$ make -j4 make -C template-coq make[1]: Entering directory '/home/arthur/tmp/Template-Coq/template-coq' make -f Makefile.coq make[2]: Entering directory '/home/arthur/tmp/Template-Coq/template-coq' COQDEP VFILES COQDEP src/template_coq.mlpack CAMLDEP src/denote.ml CAMLDEP src/constr_quoter.ml CAMLDEP src/quoter.ml CAMLDEP -pp src/g_template_coq.ml4 COQC theories/utils.v COQC theories/config.v CAMLOPT -c -for-pack Template_coq src/quoter.ml COQC theories/monad_utils.v CAMLOPT -c -for-pack Template_coq src/constr_quoter.ml CAMLOPT -c -for-pack Template_coq src/denote.ml CAMLOPT -pp -c -for-pack Template_coq src/g_template_coq.ml4 CAMLOPT -pack -o src/template_coq.cmx CAMLOPT -a -o src/template_coq.cmxa CAMLOPT -shared -o src/template_coq.cmxs COQC theories/kernel/univ.v COQC theories/kernel/uGraph.v COQC theories/Ast.v COQC theories/AstUtils.v COQC theories/Induction.v COQC theories/TemplateMonad/Core.v COQC theories/LiftSubst.v COQC theories/TemplateMonad/Monad.v COQC theories/TemplateMonad.v COQC theories/Loader.v COQC theories/UnivSubst.v COQC theories/Typing.v COQC theories/MetaTheory.v COQC theories/Checker.v COQC theories/WeakSubst.v COQC theories/WcbvEval.v COQC theories/Retyping.v COQC theories/All.v COQC theories/Extraction.v File "./theories/Extraction.v", line 24, characters 0-37: Warning: The following logical axioms were encountered: Typing.conv_refl Checker.cumul_spec Typing.wf_graph_prop_set Checker.cumul_reduce_to_product Checker.leq_universe_refl Checker.cumul_convert_leq Checker.cumul_reduce_to_sort Checker.eq_ind_refl Typing.cumul_trans Typing.cumul_refl' Checker.conv_spec Checker.infer_complete Typing.congr_cumul_prod Checker.cumul_reduce_to_ind Checker.reduce_cumul. Having invalid logical axiom in the environment when extracting may lead to incorrect or non-terminating ML terms. [extraction-logical-axiom,extraction] File "./theories/Extraction.v", line 25, characters 0-38: Warning: The following logical axioms were encountered: Typing.conv_refl Checker.cumul_spec Typing.wf_graph_prop_set Checker.cumul_reduce_to_product Checker.leq_universe_refl Checker.cumul_convert_leq Checker.cumul_reduce_to_sort Checker.eq_ind_refl Typing.cumul_trans Typing.cumul_refl' Checker.conv_spec Checker.infer_complete Typing.congr_cumul_prod Checker.cumul_reduce_to_ind Checker.reduce_cumul. Having invalid logical axiom in the environment when extracting may lead to incorrect or non-terminating ML terms. [extraction-logical-axiom,extraction] make[2]: Leaving directory '/home/arthur/tmp/Template-Coq/template-coq' make[1]: Leaving directory '/home/arthur/tmp/Template-Coq/template-coq' ./movefiles.sh make -C checker make[1]: Entering directory '/home/arthur/tmp/Template-Coq/checker' make -f Makefile.coq make[2]: Entering directory '/home/arthur/tmp/Template-Coq/checker' COQDEP VFILES CAMLDEP src/retyping0.mli CAMLDEP src/liftSubst.mli CAMLDEP src/string0.mli CAMLDEP src/typing0.mli CAMLDEP src/monad_utils.mli CAMLDEP src/binInt.mli CAMLDEP src/astUtils.mli CAMLDEP src/ast0.mli CAMLDEP src/uGraph0.mli CAMLDEP src/induction.mli CAMLDEP src/orderedType0.mli CAMLDEP src/ordersTac.mli *** Warning: in file theories/Loader.v, required library Loader matches several files in path (found Loader.v in ../template-coq/theories and theories; used the latter) *** Warning: in file theories/Loader.v, required library Loader matches several files in path (found Loader.v in ../template-coq/theories and theories; used the latter) CAMLDEP src/binPosDef.mli CAMLDEP src/orders.mli CAMLDEP src/binPos.mli CAMLDEP src/binNat.mli CAMLDEP src/binNums.mli CAMLDEP src/ascii.mli CAMLDEP src/fMapWeakList.mli CAMLDEP src/decidableType.mli CAMLDEP src/fSetWeakList.mli CAMLDEP src/basics.mli CAMLDEP src/equalities.mli CAMLDEP src/specif.mli CAMLDEP src/list0.mli CAMLDEP src/mSetWeakList.mli CAMLDEP src/nat0.mli CAMLDEP src/univ0.mli CAMLDEP src/univSubst0.mli CAMLDEP src/config0.mli CAMLDEP src/utils.mli CAMLDEP src/checker0.mli CAMLDEP src/bool.mli CAMLDEP src/datatypes.mli CAMLDEP src/peanoNat.mli COQDEP src/template_coq_checker_plugin.mlpack CAMLDEP src/decimal.mli CAMLDEP src/term_quoter.ml CAMLDEP src/retyping0.ml CAMLDEP src/liftSubst.ml CAMLDEP src/string0.ml CAMLDEP src/typing0.ml CAMLDEP src/monad_utils.ml CAMLDEP src/binInt.ml CAMLDEP src/uGraph0.ml CAMLDEP src/astUtils.ml CAMLDEP src/ast0.ml CAMLDEP src/induction.ml CAMLDEP src/orderedType0.ml CAMLDEP src/ordersTac.ml CAMLDEP src/binPosDef.ml CAMLDEP src/orders.ml CAMLDEP src/binPos.ml CAMLDEP src/binNat.ml CAMLDEP src/binNums.ml CAMLDEP src/ascii.ml CAMLDEP src/fMapWeakList.ml CAMLDEP src/decidableType.ml CAMLDEP src/fSetWeakList.ml CAMLDEP src/basics.ml CAMLDEP src/equalities.ml CAMLDEP src/specif.ml CAMLDEP src/list0.ml CAMLDEP src/mSetWeakList.ml CAMLDEP src/nat0.ml CAMLDEP src/univ0.ml CAMLDEP src/univSubst0.ml CAMLDEP src/config0.ml CAMLDEP src/utils.ml CAMLDEP src/checker0.ml CAMLDEP src/bool.ml CAMLDEP src/datatypes.ml CAMLDEP src/peanoNat.ml CAMLDEP src/decimal.ml CAMLDEP -pp src/g_template_checker.ml4 CAMLC -c src/decimal.mli CAMLC -c src/bool.mli CAMLC -c src/basics.mli CAMLC -c src/datatypes.mli CAMLC -c src/binNums.mli CAMLC -c src/config0.mli CAMLOPT -c -for-pack Template_coq_checker_plugin src/decimal.ml CAMLOPT -c -for-pack Template_coq_checker_plugin src/bool.ml CAMLC -c src/peanoNat.mli CAMLC -c src/specif.mli CAMLC -c src/equalities.mli CAMLOPT -c -for-pack Template_coq_checker_plugin src/basics.ml CAMLC -c src/nat0.mli CAMLOPT -c -for-pack Template_coq_checker_plugin src/binNums.ml CAMLC -c src/binPosDef.mli CAMLC -c src/string0.mli CAMLOPT -c -for-pack Template_coq_checker_plugin src/config0.ml CAMLC -c src/monad_utils.mli File "src/binPosDef.mli", line 3, characters 0-9: Warning 33: unused open Nat0. CAMLOPT -c -for-pack Template_coq_checker_plugin src/datatypes.ml CAMLC -c src/list0.mli CAMLOPT -c -for-pack Template_coq_checker_plugin src/equalities.ml CAMLC -c src/decidableType.mli CAMLC -c src/binPos.mli CAMLC -c src/orders.mli CAMLOPT -c -for-pack Template_coq_checker_plugin src/peanoNat.ml File "src/binPos.mli", line 5, characters 0-9: Warning 33: unused open Nat0. CAMLOPT -c -for-pack Template_coq_checker_plugin src/specif.ml CAMLC -c src/mSetWeakList.mli CAMLC -c src/fMapWeakList.mli File "src/mSetWeakList.mli", line 1, characters 0-11: Warning 33: unused open Basics. File "src/mSetWeakList.mli", line 4, characters 0-10: Warning 33: unused open List0. CAMLOPT -c -for-pack Template_coq_checker_plugin src/nat0.ml CAMLC -c src/binNat.mli File "src/binNat.mli", line 1, characters 0-11: Warning 33: unused open BinPos. CAMLOPT -c -for-pack Template_coq_checker_plugin src/string0.ml File "src/fMapWeakList.mli", line 2, characters 0-10: Warning 33: unused open List0. CAMLOPT -c -for-pack Template_coq_checker_plugin src/orders.ml CAMLC -c src/ordersTac.mli CAMLOPT -c -for-pack Template_coq_checker_plugin src/monad_utils.ml CAMLOPT -c -for-pack Template_coq_checker_plugin src/list0.ml CAMLOPT -c -for-pack Template_coq_checker_plugin src/decidableType.ml CAMLC -c src/fSetWeakList.mli File "src/fSetWeakList.mli", line 2, characters 0-17: Warning 33: unused open MSetWeakList. CAMLOPT -c -for-pack Template_coq_checker_plugin src/binPosDef.ml CAMLC -c src/binInt.mli CAMLC -c src/ascii.mli File "src/ascii.mli", line 1, characters 0-11: Warning 33: unused open BinNat. File "src/binInt.mli", line 1, characters 0-11: Warning 33: unused open BinNat. File "src/binInt.mli", line 2, characters 0-11: Warning 33: unused open BinPos. CAMLOPT -c -for-pack Template_coq_checker_plugin src/ordersTac.ml CAMLC -c src/orderedType0.mli CAMLOPT -c -for-pack Template_coq_checker_plugin src/mSetWeakList.ml File "src/orderedType0.mli", line 1, characters 0-14: Warning 33: unused open OrdersTac. File "src/ordersTac.ml", line 1, characters 0-14: Warning 33: unused open Datatypes. CAMLOPT -c -for-pack Template_coq_checker_plugin src/fMapWeakList.ml CAMLC -c src/utils.mli File "src/binPosDef.ml", line 3, characters 0-9: Warning 33: unused open Nat0. CAMLOPT -c -for-pack Template_coq_checker_plugin src/orderedType0.ml CAMLC -c src/univ0.mli CAMLOPT -c -for-pack Template_coq_checker_plugin src/fSetWeakList.ml File "src/fSetWeakList.ml", line 1, characters 0-14: Warning 33: unused open Datatypes. CAMLOPT -c -for-pack Template_coq_checker_plugin src/utils.ml File "src/univ0.mli", line 1, characters 0-9: Warning 33: unused open Bool. File "src/univ0.mli", line 3, characters 0-17: Warning 33: unused open FMapWeakList. File "src/univ0.mli", line 4, characters 0-17: Warning 33: unused open FSetWeakList. File "src/univ0.mli", line 5, characters 0-10: Warning 33: unused open List0. File "src/univ0.mli", line 6, characters 0-17: Warning 33: unused open MSetWeakList. File "src/univ0.mli", line 7, characters 0-9: Warning 33: unused open Nat0. File "src/univ0.mli", line 8, characters 0-13: Warning 33: unused open PeanoNat. File "src/univ0.mli", line 9, characters 0-12: Warning 33: unused open String0. File "src/univ0.mli", line 10, characters 0-10: Warning 33: unused open Utils. CAMLC -c src/uGraph0.mli File "src/uGraph0.mli", line 1, characters 0-11: Warning 33: unused open BinInt. File "src/uGraph0.mli", line 2, characters 0-14: Warning 33: unused open Datatypes. File "src/uGraph0.mli", line 3, characters 0-10: Warning 33: unused open List0. CAMLC -c src/ast0.mli CAMLOPT -c -for-pack Template_coq_checker_plugin src/binPos.ml CAMLOPT -c -for-pack Template_coq_checker_plugin src/univ0.ml File "src/binPos.ml", line 16, characters 10-14: Warning 39: unused rec flag. CAMLC -c src/induction.mli CAMLC -c src/astUtils.mli File "src/binPos.ml", line 184, characters 10-13: Warning 39: unused rec flag. File "src/binPos.ml", line 254, characters 10-22: Warning 39: unused rec flag. File "src/induction.mli", line 2, characters 0-14: Warning 33: unused open Datatypes. CAMLC -c src/liftSubst.mli File "src/astUtils.mli", line 3, characters 0-10: Warning 33: unused open List0. File "src/astUtils.mli", line 4, characters 0-13: Warning 33: unused open PeanoNat. File "src/astUtils.mli", line 5, characters 0-12: Warning 33: unused open String0. File "src/astUtils.mli", line 6, characters 0-10: Warning 33: unused open Utils. CAMLC -c src/univSubst0.mli File "src/liftSubst.mli", line 3, characters 0-14: Warning 33: unused open Induction. File "src/liftSubst.mli", line 4, characters 0-10: Warning 33: unused open List0. File "src/liftSubst.mli", line 5, characters 0-9: Warning 33: unused open Nat0. File "src/univ0.ml", line 1, characters 0-9: Warning 33: unused open Bool. File "src/univ0.ml", line 3, characters 0-17: Warning 33: unused open FMapWeakList. File "src/univ0.ml", line 4, characters 0-17: Warning 33: unused open FSetWeakList. File "src/binPos.ml", line 5, characters 0-9: Warning 33: unused open Nat0. File "src/univSubst0.mli", line 2, characters 0-13: Warning 33: unused open AstUtils. File "src/univSubst0.mli", line 3, characters 0-14: Warning 33: unused open Induction. File "src/univSubst0.mli", line 4, characters 0-10: Warning 33: unused open List0. CAMLC -c src/typing0.mli File "src/typing0.mli", line 4, characters 0-14: Warning 33: unused open LiftSubst. File "src/typing0.mli", line 5, characters 0-10: Warning 33: unused open List0. File "src/typing0.mli", line 6, characters 0-9: Warning 33: unused open Nat0. File "src/typing0.mli", line 7, characters 0-13: Warning 33: unused open PeanoNat. File "src/typing0.mli", line 9, characters 0-12: Warning 33: unused open String0. File "src/typing0.mli", line 10, characters 0-15: Warning 33: unused open UnivSubst0. File "src/typing0.mli", line 14, characters 0-10: Warning 33: unused open Utils. CAMLC -c src/checker0.mli File "src/checker0.mli", line 2, characters 0-13: Warning 33: unused open AstUtils. File "src/checker0.mli", line 4, characters 0-14: Warning 33: unused open Induction. File "src/checker0.mli", line 5, characters 0-14: Warning 33: unused open LiftSubst. File "src/checker0.mli", line 6, characters 0-10: Warning 33: unused open List0. File "src/checker0.mli", line 7, characters 0-13: Warning 33: unused open PeanoNat. File "src/checker0.mli", line 8, characters 0-12: Warning 33: unused open String0. File "src/checker0.mli", line 10, characters 0-15: Warning 33: unused open UnivSubst0. CAMLC -c src/retyping0.mli File "src/retyping0.mli", line 3, characters 0-14: Warning 33: unused open Datatypes. File "src/retyping0.mli", line 4, characters 0-14: Warning 33: unused open LiftSubst. File "src/retyping0.mli", line 5, characters 0-10: Warning 33: unused open List0. File "src/retyping0.mli", line 6, characters 0-16: Warning 33: unused open Monad_utils. CAMLOPT -c -for-pack Template_coq_checker_plugin src/binNat.ml File "src/binNat.ml", line 78, characters 10-13: Warning 39: unused rec flag. File "src/binNat.ml", line 314, characters 10-15: Warning 39: unused rec flag. CAMLOPT -c -for-pack Template_coq_checker_plugin src/binInt.ml CAMLOPT -c -for-pack Template_coq_checker_plugin src/ascii.ml File "src/binInt.ml", line 174, characters 10-13: Warning 39: unused rec flag. CAMLOPT -c -for-pack Template_coq_checker_plugin src/uGraph0.ml CAMLOPT -c -for-pack Template_coq_checker_plugin src/ast0.ml CAMLOPT -c -for-pack Template_coq_checker_plugin src/astUtils.ml CAMLOPT -c -for-pack Template_coq_checker_plugin src/induction.ml CAMLOPT -c -for-pack Template_coq_checker_plugin src/term_quoter.ml CAMLOPT -c -for-pack Template_coq_checker_plugin src/liftSubst.ml CAMLOPT -c -for-pack Template_coq_checker_plugin src/univSubst0.ml CAMLOPT -c -for-pack Template_coq_checker_plugin src/typing0.ml File "src/typing0.ml", line 11, characters 0-12: Warning 33: unused open Config0. CAMLOPT -c -for-pack Template_coq_checker_plugin src/checker0.ml File "src/checker0.ml", line 1869, characters 53-55: Warning 20: this argument will not be used by the function. File "src/checker0.ml", line 1869, characters 56-58: Warning 20: this argument will not be used by the function. File "src/checker0.ml", line 11, characters 0-12: Warning 33: unused open Config0. CAMLOPT -c -for-pack Template_coq_checker_plugin src/retyping0.ml CAMLOPT -pp -c -for-pack Template_coq_checker_plugin src/g_template_checker.ml4 File "src/retyping0.ml", line 8, characters 0-10: Warning 33: unused open Utils. CAMLOPT -pack -o src/template_coq_checker_plugin.cmx CAMLOPT -a -o src/template_coq_checker_plugin.cmxa CAMLOPT -shared -o src/template_coq_checker_plugin.cmxs COQC theories/Loader.v make[2]: Leaving directory '/home/arthur/tmp/Template-Coq/checker' make[1]: Leaving directory '/home/arthur/tmp/Template-Coq/checker' make -C extraction make[1]: Entering directory '/home/arthur/tmp/Template-Coq/extraction' make -f Makefile.extraction make[2]: Entering directory '/home/arthur/tmp/Template-Coq/extraction' COQDEP VFILES COQC theories/Ast.v File "./theories/Ast.v", line 175, characters 0-67: Warning: Notation _ ,, _ was already used. [notation-overridden,parsing] COQC theories/Induction.v File "./theories/Induction.v", line 4, characters 0-43: Warning: Notation _ ,, _ was already used. [notation-overridden,parsing] COQC theories/LiftSubst.v File "./theories/LiftSubst.v", line 4, characters 0-53: Warning: Notation _ ,, _ was already used. [notation-overridden,parsing] COQC theories/UnivSubst.v File "./theories/UnivSubst.v", line 5, characters 0-63: Warning: Notation _ ,, _ was already used. [notation-overridden,parsing] COQC theories/Typing.v File "./theories/Typing.v", line 5, characters 0-73: Warning: Notation _ ,, _ was already used. [notation-overridden,parsing] COQC theories/WcbvEval.v File "./theories/WcbvEval.v", line 5, characters 0-80: Warning: Notation _ ,, _ was already used. [notation-overridden,parsing] COQC theories/Extract.v COQC theories/All.v COQC theories/Extraction.v File "./theories/All.v", line 1, characters 0-43: Warning: Notation _ ,, _ was already used. [notation-overridden,parsing] File "./theories/Extraction.v", line 7, characters 0-43: Warning: Notation _ ,, _ was already used. [notation-overridden,parsing] File "./theories/Extraction.v", line 34, characters 0-27: Warning: The following logical axioms were encountered: Typing.conv_refl Checker.cumul_spec Typing.wf_graph_prop_set Checker.cumul_reduce_to_product Checker.leq_universe_refl Checker.cumul_convert_leq Checker.cumul_reduce_to_sort Checker.eq_ind_refl Typing.cumul_trans Typing.cumul_refl' Checker.conv_spec Checker.infer_complete Typing.congr_cumul_prod Checker.cumul_reduce_to_ind Checker.reduce_cumul. Having invalid logical axiom in the environment when extracting may lead to incorrect or non-terminating ML terms. [extraction-logical-axiom,extraction] make[2]: Leaving directory '/home/arthur/tmp/Template-Coq/extraction' sh clean_extraction.sh Cleaning result of extraction Moving Ast1.ml to src/ast1.ml Moving Ast1.mli to src/ast1.mli Moving Extract.ml to src/extract.ml Moving Extract.mli to src/extract.mli Moving Induction0.ml to src/induction0.ml Moving Induction0.mli to src/induction0.mli Moving LiftSubst0.ml to src/liftSubst0.ml Moving LiftSubst0.mli to src/liftSubst0.mli Moving Typing1.ml to src/typing1.ml Moving Typing1.mli to src/typing1.mli Moving UnivSubst1.ml to src/univSubst1.ml Moving UnivSubst1.mli to src/univSubst1.mli make -f Makefile.plugin make[2]: Entering directory '/home/arthur/tmp/Template-Coq/extraction' CAMLDEP src/extract.mli CAMLDEP src/univSubst1.mli CAMLDEP src/typing1.mli CAMLDEP src/liftSubst0.mli CAMLDEP src/induction0.mli CAMLDEP src/ast1.mli COQDEP src/template_coq_extraction_plugin.mlpack CAMLDEP src/extract.ml CAMLDEP src/univSubst1.ml CAMLDEP src/typing1.ml CAMLDEP src/liftSubst0.ml CAMLDEP src/induction0.ml CAMLDEP src/ast1.ml CAMLC -c src/ast1.mli CAMLC -c src/induction0.mli File "command line", line 1: File "command line", line 1: Error: Unbound module Template_coq_checker_plugin.Typing0Error: Unbound module Template_coq_checker_plugin.Typing0 Makefile.plugin:588: recipe for target 'src/ast1.cmi' failed make[3]: *** [src/ast1.cmi] Error 2 make[3]: *** Waiting for unfinished jobs.... Makefile.plugin:588: recipe for target 'src/induction0.cmi' failed make[3]: *** [src/induction0.cmi] Error 2 Makefile.plugin:317: recipe for target 'all' failed make[2]: *** [all] Error 2 make[2]: Leaving directory '/home/arthur/tmp/Template-Coq/extraction' Makefile:15: recipe for target 'plugin' failed make[1]: *** [plugin] Error 2 make[1]: Leaving directory '/home/arthur/tmp/Template-Coq/extraction' Makefile:37: recipe for target 'extraction' failed make: *** [extraction] Error 2