pgiarrusso@SilenceOfTheLambdas:~/git/Coq/needle/knot-esop-2017-case-study/casestudy/needle$ make -k
/Library/Developer/CommandLineTools/usr/bin/make -C fexistsprod
/Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
COQC FExistsProd.v
File "./FExistsProd.v", line 2310, characters 0-1107:
Warning: Not a fully mutually defined fixpoint
(PTyping_wf_1 and PTyping_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./FExistsProd.v", line 2322, characters 0-2664:
Warning: Not a fully mutually defined fixpoint
(Typing_wf_1 and Typing_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
COQC DeclarationEvaluation.v
COQC MetaTheory.v
/Library/Developer/CommandLineTools/usr/bin/make -C lomega
/Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
COQC LambdaOmega.v
File "./LambdaOmega.v", line 2043, characters 0-2410:
Warning: Not a fully mutually defined fixpoint
(e.g., TRed_wf_1 and TRed_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./LambdaOmega.v", line 2070, characters 0-1157:
Warning: Not a fully mutually defined fixpoint
(Kinding_wf_1 and Kinding_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./LambdaOmega.v", line 2086, characters 0-1056:
Warning: Not a fully mutually defined fixpoint
(e.g., TRedStar_wf_1 and TRedStar_wf_0 are not mutually
dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./LambdaOmega.v", line 2104, characters 0-2740:
Warning: Not a fully mutually defined fixpoint
(TyEq_wf_2 and TyEq_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./LambdaOmega.v", line 2137, characters 0-1148:
Warning: Not a fully mutually defined fixpoint
(Typing_wf_1 and Typing_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./LambdaOmega.v", line 2181, characters 0-61:
Warning: obligation_Env_reg_TRed is declared as a local axiom
[local-declaration,scope]
COQC DeclarationEvaluation.v
COQC MetaTheory.v
File "./MetaTheory.v", line 278, characters 4-56:
Error: Unable to find an instance for the variables S1, S2.
make[2]: *** [MetaTheory.vo] Error 1
make[2]: Target `all' not remade because of errors.
make[1]: *** [coq] Error 2
make: *** [lomega] Error 2
/Library/Developer/CommandLineTools/usr/bin/make -C fomega
/Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
COQC FOmega.v
File "./FOmega.v", line 2227, characters 0-2708:
Warning: Not a fully mutually defined fixpoint
(e.g., TRed_wf_1 and TRed_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./FOmega.v", line 2257, characters 0-1327:
Warning: Not a fully mutually defined fixpoint
(Kinding_wf_1 and Kinding_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./FOmega.v", line 2275, characters 0-1067:
Warning: Not a fully mutually defined fixpoint
(e.g., TRedStar_wf_1 and TRedStar_wf_0 are not mutually
dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./FOmega.v", line 2293, characters 0-3034:
Warning: Not a fully mutually defined fixpoint
(TyEq_wf_2 and TyEq_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./FOmega.v", line 2329, characters 0-1698:
Warning: Not a fully mutually defined fixpoint
(Typing_wf_1 and Typing_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./FOmega.v", line 2377, characters 0-61:
Warning: obligation_Env_reg_TRed is declared as a local axiom
[local-declaration,scope]
COQC DeclarationEvaluation.v
COQC MetaTheory.v
File "./MetaTheory.v", line 281, characters 39-41:
Ltac call to "exists (ne_bindings_list)" failed.
Error: The reference T0 was not found in the current environment.
make[2]: *** [MetaTheory.vo] Error 1
make[2]: Target `all' not remade because of errors.
make[1]: *** [coq] Error 2
make: *** [fomega] Error 2
/Library/Developer/CommandLineTools/usr/bin/make -C fsub
/Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
COQC FSub.v
File "./FSub.v", line 1829, characters 0-1623:
Warning: Not a fully mutually defined fixpoint
(Typing_wf_1 and Typing_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./FSub.v", line 1856, characters 0-57:
Warning: obligation_Env_var_ty is declared as a local axiom
[local-declaration,scope]
File "./FSub.v", line 1870, characters 0-59:
Warning: obligation_Env_reg_Sub is declared as a local axiom
[local-declaration,scope]
COQC DeclarationEvaluation.v
COQC MetaTheory.v
File "./MetaTheory.v", line 72, characters 4-5:
Error: Wrong bullet + : Current bullet + is not finished.
make[2]: *** [MetaTheory.vo] Error 1
make[2]: Target `all' not remade because of errors.
make[1]: *** [coq] Error 2
make: *** [fsub] Error 2
/Library/Developer/CommandLineTools/usr/bin/make -C stlc
/Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
COQC Stlc.v
File "./Stlc.v", line 884, characters 0-1027:
Warning: Not a fully mutually defined fixpoint
(Typing_wf_1 and Typing_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
COQC DeclarationEvaluation.v
COQC MetaTheory.v
/Library/Developer/CommandLineTools/usr/bin/make -C fsubprod
/Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
COQC FSubProd.v
File "./FSubProd.v", line 2324, characters 0-1110:
Warning: Not a fully mutually defined fixpoint
(PTyping_wf_1 and PTyping_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./FSubProd.v", line 2336, characters 0-2448:
Warning: Not a fully mutually defined fixpoint
(Typing_wf_1 and Typing_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./FSubProd.v", line 2370, characters 0-57:
Warning: obligation_Env_var_ty is declared as a local axiom
[local-declaration,scope]
File "./FSubProd.v", line 2384, characters 0-59:
Warning: obligation_Env_reg_Sub is declared as a local axiom
[local-declaration,scope]
COQC DeclarationEvaluation.v
COQC MetaTheory.v
File "./MetaTheory.v", line 100, characters 4-5:
Error: Wrong bullet + : Current bullet + is not finished.
make[2]: *** [MetaTheory.vo] Error 1
make[2]: Target `all' not remade because of errors.
make[1]: *** [coq] Error 2
make: *** [fsubprod] Error 2
/Library/Developer/CommandLineTools/usr/bin/make -C f
/Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
COQC F.v
File "./F.v", line 1670, characters 0-1402:
Warning: Not a fully mutually defined fixpoint
(Typing_wf_1 and Typing_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
COQC DeclarationEvaluation.v
COQC MetaTheory.v
/Library/Developer/CommandLineTools/usr/bin/make -C fexists
/Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
COQC Fexists.v
File "./Fexists.v", line 1827, characters 0-1847:
Warning: Not a fully mutually defined fixpoint
(Typing_wf_1 and Typing_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
COQC DeclarationEvaluation.v
COQC MetaTheory.v
/Library/Developer/CommandLineTools/usr/bin/make -C stlcprod
/Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
COQC StlcProd.v
File "./StlcProd.v", line 1185, characters 0-1107:
Warning: Not a fully mutually defined fixpoint
(PTyping_wf_1 and PTyping_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./StlcProd.v", line 1197, characters 0-1816:
Warning: Not a fully mutually defined fixpoint
(Typing_wf_1 and Typing_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./StlcProd.v", line 1224, characters 0-57:
Warning: obligation_Env_var_tm is declared as a local axiom
[local-declaration,scope]
File "./StlcProd.v", line 1232, characters 0-65:
Warning: obligation_Env_reg_Typing is declared as a local axiom
[local-declaration,scope]
COQC DeclarationEvaluation.v
COQC MetaTheory.v
/Library/Developer/CommandLineTools/usr/bin/make -C fprod
/Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
COQC FProd.v
File "./FProd.v", line 2154, characters 0-1107:
Warning: Not a fully mutually defined fixpoint
(PTyping_wf_1 and PTyping_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./FProd.v", line 2166, characters 0-2204:
Warning: Not a fully mutually defined fixpoint
(Typing_wf_1 and Typing_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
COQC DeclarationEvaluation.v
COQC MetaTheory.v
/Library/Developer/CommandLineTools/usr/bin/make -C fseqlet
/Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
COQC FSeqLet.v
File "./FSeqLet.v", line 2241, characters 0-2270:
Warning: Not a fully mutually defined fixpoint
(Typing_wf_1 and DTyping_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
COQC DeclarationEvaluation.v
COQC MetaTheory.v
make: Target `default' not remade because of errors.