diff options
author | 2001-04-09 13:42:50 +0000 | |
---|---|---|
committer | 2001-04-09 13:42:50 +0000 | |
commit | f67fb6284009a7686ee51f4e6f44d9233de8b788 (patch) | |
tree | c83a26b1ffd1a4ab532b2edb5331539d9eab523f | |
parent | e8c3bd0da575bb15fe7a31e676faecbe1d45e62c (diff) |
branchement extraction en standard (pas de Require)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1561 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | .depend.coq | 180 | ||||
-rw-r--r-- | Makefile | 23 | ||||
-rw-r--r-- | contrib/correctness/pcic.ml | 4 | ||||
-rw-r--r-- | contrib/correctness/pred.ml | 4 | ||||
-rw-r--r-- | contrib/correctness/preuves.v | 7 | ||||
-rw-r--r-- | contrib/correctness/ptactic.ml | 12 | ||||
-rw-r--r-- | contrib/extraction/Extraction.v | 20 | ||||
-rw-r--r-- | contrib/extraction/extract_env.ml | 38 | ||||
-rw-r--r-- | contrib/extraction/mlutil.ml | 52 | ||||
-rw-r--r-- | contrib/extraction/mlutil.mli | 13 | ||||
-rw-r--r-- | contrib/extraction/ocaml.ml | 5 | ||||
-rw-r--r-- | contrib/extraction/ocaml.mli | 5 | ||||
-rw-r--r-- | parsing/g_basevernac.ml4 | 2 | ||||
-rw-r--r-- | states/MakeInitial.v | 1 | ||||
-rw-r--r-- | toplevel/toplevel.ml | 16 |
15 files changed, 241 insertions, 141 deletions
diff --git a/.depend.coq b/.depend.coq index 6a766839f..bac71a85f 100644 --- a/.depend.coq +++ b/.depend.coq @@ -15,8 +15,6 @@ theories/Wellfounded/Lexicographic_Exponentiation.vo: theories/Wellfounded/Lexic theories/Wellfounded/Inverse_Image.vo: theories/Wellfounded/Inverse_Image.v theories/Wellfounded/Inclusion.vo: theories/Wellfounded/Inclusion.v theories/Relations/Relation_Definitions.vo theories/Wellfounded/Disjoint_Union.vo: theories/Wellfounded/Disjoint_Union.v theories/Relations/Relation_Operators.vo -theories/TOADD/zimmermann.vo: theories/TOADD/zimmermann.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo -theories/TOADD/cuiht.vo: theories/TOADD/cuiht.v theories/Lists/PolyList.vo theories/Bool/BoolEq.vo theories/Sets/Uniset.vo: theories/Sets/Uniset.v theories/Bool/Bool.vo theories/Sets/Permut.vo theories/Sets/Relations_3_facts.vo: theories/Sets/Relations_3_facts.v theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Relations_2.vo theories/Sets/Relations_2_facts.vo theories/Sets/Relations_3.vo theories/Sets/Relations_3.vo: theories/Sets/Relations_3.v theories/Sets/Relations_1.vo theories/Sets/Relations_2.vo @@ -61,7 +59,6 @@ theories/Num/Params.vo: theories/Num/Params.v theories/Num/OppProps.vo: theories/Num/OppProps.v theories/Num/OppAxioms.vo: theories/Num/OppAxioms.v theories/Num/NeqDef.vo: theories/Num/NeqDef.v theories/Num/Params.vo theories/Num/EqParams.vo -theories/Num/NatSyntax.vo: theories/Num/NatSyntax.v theories/Num/NSyntax.vo: theories/Num/NSyntax.v theories/Num/Params.vo theories/Num/LtProps.vo: theories/Num/LtProps.v theories/Num/Axioms.vo theories/Num/AddProps.vo theories/Num/LeProps.vo: theories/Num/LeProps.v theories/Num/LtProps.vo theories/Num/LeAxioms.vo @@ -87,7 +84,6 @@ theories/Logic/Classical_Pred_Set.vo: theories/Logic/Classical_Pred_Set.v theori theories/Logic/Classical.vo: theories/Logic/Classical.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Set.vo theories/Lists/TheoryList.vo: theories/Lists/TheoryList.v theories/Lists/PolyList.vo theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Minus.vo theories/Bool/DecBool.vo theories/Lists/Streams.vo: theories/Lists/Streams.v -theories/Lists/Program.vo: theories/Lists/Program.v tactics/Refine.vo theories/Lists/PolyListSyntax.vo: theories/Lists/PolyListSyntax.v theories/Lists/PolyList.vo theories/Lists/PolyList.vo: theories/Lists/PolyList.v theories/Arith/Le.vo theories/Lists/ListSet.vo: theories/Lists/ListSet.v theories/Lists/PolyList.vo @@ -123,7 +119,6 @@ theories/Bool/Zerob.vo: theories/Bool/Zerob.v theories/Arith/Arith.vo theories/B theories/Bool/Sumbool.vo: theories/Bool/Sumbool.v theories/Bool/IfProp.vo: theories/Bool/IfProp.v theories/Bool/Bool.vo theories/Bool/DecBool.vo: theories/Bool/DecBool.v -theories/Bool/BoolEq.vo: theories/Bool/BoolEq.v theories/Bool/Bool.vo theories/Bool/Bool.vo: theories/Bool/Bool.v theories/Arith/Wf_nat.vo: theories/Arith/Wf_nat.v theories/Arith/Lt.vo theories/Arith/Plus.vo: theories/Arith/Plus.v theories/Arith/Le.vo theories/Arith/Lt.vo @@ -179,23 +174,24 @@ contrib/omega/Zlogarithm.vo: contrib/omega/Zlogarithm.v theories/Zarith/ZArith.v contrib/omega/Zcomplements.vo: contrib/omega/Zcomplements.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo contrib/omega/OmegaSyntax.vo: contrib/omega/OmegaSyntax.v contrib/omega/Omega.vo: contrib/omega/Omega.v theories/Zarith/ZArith.vo theories/Arith/Minus.vo contrib/omega/omega.cmo contrib/omega/coq_omega.cmo contrib/omega/OmegaSyntax.vo +contrib/interface/Centaur.vo: contrib/interface/Centaur.v contrib/interface/paths.cmo contrib/interface/name_to_ast.cmo contrib/interface/xlate.cmo contrib/interface/vtp.cmo contrib/interface/translate.cmo contrib/interface/pbp.cmo contrib/interface/dad.cmo contrib/interface/debug_tac.cmo contrib/interface/history.cmo contrib/interface/centaur.cmo contrib/interface/AddDad.vo +contrib/interface/AddDad.vo: contrib/interface/AddDad.v contrib/extraction/test_extraction.vo: contrib/extraction/test_extraction.v -contrib/extraction/Extraction.vo: contrib/extraction/Extraction.v contrib/extraction/mlutil.cmo contrib/extraction/ocaml.cmo contrib/extraction/extraction.cmo contrib/extraction/extract_env.cmo -ADM/BUG/unfold.vo: ADM/BUG/unfold.v -ADM/BUG/thery.vo: ADM/BUG/thery.v theories/Bool/Bool.vo theories/Zarith/ZArith.vo theories/Lists/PolyList.vo -ADM/BUG/simpl3.vo: ADM/BUG/simpl3.v -ADM/BUG/simpl2.vo: ADM/BUG/simpl2.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/Zarith/ZArith.vo theories/Arith/Wf_nat.vo -ADM/BUG/simpl.vo: ADM/BUG/simpl.v theories/Lists/PolyList.vo -ADM/BUG/sec.vo: ADM/BUG/sec.v -ADM/BUG/record.vo: ADM/BUG/record.v theories/Arith/Arith.vo theories/Arith/EqNat.vo -ADM/BUG/local.vo: ADM/BUG/local.v -ADM/BUG/jfm.vo: ADM/BUG/jfm.v theories/Lists/PolyList.vo -ADM/BUG/fix.vo: ADM/BUG/fix.v -ADM/BUG/eauto.vo: ADM/BUG/eauto.v theories/Lists/PolyList.vo -ADM/BUG/eapp.vo: ADM/BUG/eapp.v -ADM/BUG/bugimpl.vo: ADM/BUG/bugimpl.v -ADM/BUG/bug.vo: ADM/BUG/bug.v -ADM/BUG/benjamin.vo: ADM/BUG/benjamin.v theories/Zarith/ZArith.vo theories/Lists/PolyList.vo contrib/omega/Omega.vo +contrib/extraction/Extraction.vo: contrib/extraction/Extraction.v +contrib/correctness/preuves.vo: contrib/correctness/preuves.v contrib/correctness/Correctness.vo contrib/omega/Omega.vo +contrib/correctness/Tuples.vo: contrib/correctness/Tuples.v +contrib/correctness/Sorted.vo: contrib/correctness/Sorted.v contrib/correctness/Arrays.vo contrib/correctness/ArrayPermut.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo +contrib/correctness/Programs_stuff.vo: contrib/correctness/Programs_stuff.v contrib/correctness/Arrays_stuff.vo +contrib/correctness/ProgramsExtraction.vo: contrib/correctness/ProgramsExtraction.v contrib/extraction/Extraction.vo contrib/correctness/Correctness.vo contrib/correctness/pextract.cmo +contrib/correctness/ProgWf.vo: contrib/correctness/ProgWf.v theories/Zarith/ZArith.vo theories/Arith/Wf_nat.vo +contrib/correctness/ProgInt.vo: contrib/correctness/ProgInt.v theories/Zarith/ZArith.vo theories/Zarith/ZArith_dec.vo +contrib/correctness/ProgBool.vo: contrib/correctness/ProgBool.v theories/Arith/Compare_dec.vo theories/Arith/Peano_dec.vo theories/Zarith/ZArith.vo theories/Bool/Sumbool.vo +contrib/correctness/MakeProgramsState.vo: contrib/correctness/MakeProgramsState.v +contrib/correctness/Exchange.vo: contrib/correctness/Exchange.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo +contrib/correctness/Correctness.vo: contrib/correctness/Correctness.v tactics/Refine.vo contrib/correctness/Tuples.vo contrib/correctness/ProgInt.vo contrib/correctness/ProgBool.vo contrib/correctness/ProgWf.vo contrib/correctness/Arrays.vo contrib/correctness/pmisc.cmo contrib/correctness/peffect.cmo contrib/correctness/prename.cmo contrib/correctness/perror.cmo contrib/correctness/penv.cmo contrib/correctness/putil.cmo contrib/correctness/pdb.cmo contrib/correctness/pcic.cmo contrib/correctness/pmonad.cmo contrib/correctness/pcicenv.cmo contrib/correctness/pred.cmo contrib/correctness/ptyping.cmo contrib/correctness/pwp.cmo contrib/correctness/pmlize.cmo contrib/correctness/ptactic.cmo contrib/correctness/psyntax.cmo +contrib/correctness/Arrays_stuff.vo: contrib/correctness/Arrays_stuff.v contrib/correctness/Exchange.vo contrib/correctness/ArrayPermut.vo contrib/correctness/Sorted.vo +contrib/correctness/Arrays.vo: contrib/correctness/Arrays.v contrib/correctness/ProgInt.vo +contrib/correctness/ArrayPermut.vo: contrib/correctness/ArrayPermut.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo contrib/correctness/Exchange.vo contrib/omega/Omega.vo tactics/Tauto.vo: tactics/Tauto.v tactics/Refine.vo: tactics/Refine.v tactics/Inv.vo: tactics/Inv.v tactics/Equality.vo @@ -207,77 +203,95 @@ syntax/PPTactic.vo: syntax/PPTactic.v syntax/PPConstr.vo: syntax/PPConstr.v syntax/PPCases.vo: syntax/PPCases.v syntax/MakeBare.vo: syntax/MakeBare.v -states/MakeInitial.vo: states/MakeInitial.v theories/Init/Prelude.vo theories/Init/Logic_Type.vo theories/Init/Logic_TypeSyntax.vo tactics/Equality.vo test-suite/success/Tauto.vo tactics/Inv.vo tactics/EAuto.vo tactics/AutoRewrite.vo tactics/Refine.vo tactics/EqDecide.vo -ADM/toto.vo: ADM/toto.v theories/Reals/Reals.vo theories/Arith/Peano_dec.vo -ADM/ind.vo: ADM/ind.v theories/Sets/Ensembles.vo theories/Sets/Relations_1.vo -ADM/bug3.vo: ADM/bug3.v ADM/bug2.vo -ADM/bug2.vo: ADM/bug2.v -ADM/bug1.vo: ADM/bug1.v -ADM/bug.vo: ADM/bug.v theories/Lists/PolyList.vo +states/MakeInitial.vo: states/MakeInitial.v theories/Init/Prelude.vo theories/Init/Logic_Type.vo theories/Init/Logic_TypeSyntax.vo tactics/Equality.vo test-suite/success/Tauto.vo tactics/Inv.vo tactics/EAuto.vo tactics/AutoRewrite.vo tactics/Refine.vo tactics/EqDecide.vo contrib/extraction/Extraction.vo +contrib/interface/Centaur.vo: contrib/interface/Centaur.v contrib/interface/paths.cmo contrib/interface/name_to_ast.cmo contrib/interface/xlate.cmo contrib/interface/vtp.cmo contrib/interface/translate.cmo contrib/interface/pbp.cmo contrib/interface/dad.cmo contrib/interface/debug_tac.cmo contrib/interface/history.cmo contrib/interface/centaur.cmo contrib/interface/AddDad.vo +contrib/interface/AddDad.vo: contrib/interface/AddDad.v +contrib/correctness/ArrayPermut.vo: contrib/correctness/ArrayPermut.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo contrib/correctness/Exchange.vo contrib/omega/Omega.vo +contrib/correctness/Correctness.vo: contrib/correctness/Correctness.v tactics/Refine.vo contrib/correctness/Tuples.vo contrib/correctness/ProgInt.vo contrib/correctness/ProgBool.vo contrib/correctness/ProgWf.vo contrib/correctness/Arrays.vo contrib/correctness/pmisc.cmo contrib/correctness/peffect.cmo contrib/correctness/prename.cmo contrib/correctness/perror.cmo contrib/correctness/penv.cmo contrib/correctness/putil.cmo contrib/correctness/pdb.cmo contrib/correctness/pcic.cmo contrib/correctness/pmonad.cmo contrib/correctness/pcicenv.cmo contrib/correctness/pred.cmo contrib/correctness/ptyping.cmo contrib/correctness/pwp.cmo contrib/correctness/pmlize.cmo contrib/correctness/ptactic.cmo contrib/correctness/psyntax.cmo +contrib/correctness/ProgWf.vo: contrib/correctness/ProgWf.v theories/Zarith/ZArith.vo theories/Arith/Wf_nat.vo +contrib/correctness/Programs_stuff.vo: contrib/correctness/Programs_stuff.v contrib/correctness/Arrays_stuff.vo +contrib/correctness/ProgramsExtraction.vo: contrib/correctness/ProgramsExtraction.v contrib/extraction/Extraction.vo contrib/correctness/Correctness.vo contrib/correctness/pextract.cmo +contrib/correctness/ProgInt.vo: contrib/correctness/ProgInt.v theories/Zarith/ZArith.vo theories/Zarith/ZArith_dec.vo +contrib/correctness/ProgBool.vo: contrib/correctness/ProgBool.v theories/Arith/Compare_dec.vo theories/Arith/Peano_dec.vo theories/Zarith/ZArith.vo theories/Bool/Sumbool.vo +contrib/correctness/preuves.vo: contrib/correctness/preuves.v contrib/correctness/Correctness.vo contrib/omega/Omega.vo +contrib/correctness/examples/make_extr.vo: contrib/correctness/examples/make_extr.v contrib/correctness/ProgramsExtraction.vo contrib/correctness/examples/exp.vo contrib/correctness/examples/exp_int.vo contrib/correctness/examples/fact.vo contrib/correctness/examples/fact_int.vo contrib/correctness/examples/Handbook.vo +contrib/correctness/examples/Handbook.vo: contrib/correctness/examples/Handbook.v theories/Bool/Sumbool.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo contrib/omega/Zpower.vo +contrib/correctness/examples/fact.vo: contrib/correctness/examples/fact.v contrib/omega/Omega.vo theories/Arith/Arith.vo +contrib/correctness/examples/fact_int.vo: contrib/correctness/examples/fact_int.v contrib/omega/Omega.vo contrib/ring/ZArithRing.vo +contrib/correctness/examples/exp.vo: contrib/correctness/examples/exp.v theories/Arith/Even.vo theories/Arith/Div2.vo contrib/correctness/Correctness.vo contrib/ring/ArithRing.vo contrib/ring/ZArithRing.vo +contrib/correctness/examples/exp_int.vo: contrib/correctness/examples/exp_int.v contrib/omega/Zpower.vo contrib/omega/Zcomplements.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo +contrib/correctness/MakeProgramsState.vo: contrib/correctness/MakeProgramsState.v +contrib/correctness/Exchange.vo: contrib/correctness/Exchange.v contrib/correctness/ProgInt.vo contrib/correctness/Arrays.vo +contrib/correctness/Arrays.vo: contrib/correctness/Arrays.v contrib/correctness/ProgInt.vo +contrib/correctness/Arrays_stuff.vo: contrib/correctness/Arrays_stuff.v contrib/correctness/Exchange.vo contrib/correctness/ArrayPermut.vo contrib/correctness/Sorted.vo +contrib/correctness/Tuples.vo: contrib/correctness/Tuples.v +contrib/correctness/Sorted.vo: contrib/correctness/Sorted.v contrib/correctness/Arrays.vo contrib/correctness/ArrayPermut.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo +contrib/extraction/test/bench.vo: contrib/extraction/test/bench.v theories/Lists/PolyList.vo theories/Zarith/ZArith.vo theories/Arith/Even.vo contrib/extraction/test_extraction.vo: contrib/extraction/test_extraction.v -contrib/extraction/Extraction.vo: contrib/extraction/Extraction.v contrib/extraction/mlutil.cmo contrib/extraction/ocaml.cmo contrib/extraction/extraction.cmo contrib/extraction/extract_env.cmo +contrib/extraction/Extraction.vo: contrib/extraction/Extraction.v contrib/xml/Xml.vo: contrib/xml/Xml.v contrib/xml/xml.cmo contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo -contrib/ring/ArithRing.vo: contrib/ring/ArithRing.v contrib/ring/Ring.vo theories/Arith/Arith.vo theories/Logic/Eqdep_dec.vo contrib/ring/ZArithRing.vo: contrib/ring/ZArithRing.v contrib/ring/ArithRing.vo theories/Zarith/ZArith.vo theories/Logic/Eqdep_dec.vo contrib/ring/Ring_theory.vo: contrib/ring/Ring_theory.v theories/Bool/Bool.vo contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_abstract.vo: contrib/ring/Ring_abstract.v contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo contrib/ring/Ring.vo: contrib/ring/Ring.v theories/Bool/Bool.vo contrib/ring/Ring_theory.vo contrib/ring/Quote.vo contrib/ring/Ring_normalize.vo contrib/ring/Ring_abstract.vo contrib/ring/ring.cmo contrib/ring/Quote.vo: contrib/ring/Quote.v contrib/ring/quote.cmo +contrib/ring/ArithRing.vo: contrib/ring/ArithRing.v contrib/ring/Ring.vo theories/Arith/Arith.vo theories/Logic/Eqdep_dec.vo contrib/omega/Zpower.vo: contrib/omega/Zpower.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo contrib/omega/Zcomplements.vo: contrib/omega/Zcomplements.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo contrib/omega/OmegaSyntax.vo: contrib/omega/OmegaSyntax.v contrib/omega/Omega.vo: contrib/omega/Omega.v theories/Zarith/ZArith.vo theories/Arith/Minus.vo contrib/omega/omega.cmo contrib/omega/coq_omega.cmo contrib/omega/OmegaSyntax.vo contrib/omega/Zlogarithm.vo: contrib/omega/Zlogarithm.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo contrib/omega/Zpower.vo -theories/IntMap/Graphs/Zcgraph.vo: theories/IntMap/Graphs/Zcgraph.v theories/IntMap/Graphs/Cgraph.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Addec.vo -theories/IntMap/Graphs/Cgraph.vo: theories/IntMap/Graphs/Cgraph.v theories/Arith/Arith.vo theories/Zarith/ZArith.vo theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Lists/PolyList.vo theories/Arith/Wf_nat.vo theories/IntMap/Allmaps.vo -theories/IntMap/Mapcanon.vo: theories/IntMap/Mapcanon.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo -theories/IntMap/Mapaxioms.vo: theories/IntMap/Mapaxioms.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo -theories/IntMap/Fset.vo: theories/IntMap/Fset.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo -theories/IntMap/Map.vo: theories/IntMap/Map.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo -theories/IntMap/Addec.vo: theories/IntMap/Addec.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo -theories/IntMap/Adalloc.vo: theories/IntMap/Adalloc.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Zarith/ZArith.vo theories/Arith/Arith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo -theories/IntMap/Allmaps.vo: theories/IntMap/Allmaps.v theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapsubset.vo theories/IntMap/Lsort.vo theories/IntMap/Mapfold.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo theories/IntMap/Mapc.vo theories/IntMap/Maplists.vo theories/IntMap/Adalloc.vo -theories/IntMap/Maplists.vo: theories/IntMap/Maplists.v theories/IntMap/Addr.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo theories/IntMap/Mapc.vo theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Lists/PolyList.vo theories/Arith/Arith.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapfold.vo -theories/IntMap/Lsort.vo: theories/IntMap/Lsort.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/Lists/PolyList.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapsubset.vo: theories/IntMap/Mapsubset.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo +theories/IntMap/Maplists.vo: theories/IntMap/Maplists.v theories/IntMap/Addr.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo theories/IntMap/Mapc.vo theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Lists/PolyList.vo theories/Arith/Arith.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapfold.vo theories/IntMap/Mapiter.vo: theories/IntMap/Mapiter.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Fset.vo theories/Lists/PolyList.vo theories/IntMap/Mapfold.vo: theories/IntMap/Mapfold.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/Lists/PolyList.vo theories/IntMap/Mapcard.vo: theories/IntMap/Mapcard.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/IntMap/Mapsubset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/Arith/Peano_dec.vo theories/IntMap/Mapc.vo: theories/IntMap/Mapc.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Fset.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapsubset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo +theories/IntMap/Mapcanon.vo: theories/IntMap/Mapcanon.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/Lists/PolyList.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapcard.vo +theories/IntMap/Map.vo: theories/IntMap/Map.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo +theories/IntMap/Lsort.vo: theories/IntMap/Lsort.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/Lists/PolyList.vo theories/IntMap/Mapiter.vo +theories/IntMap/Fset.vo: theories/IntMap/Fset.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo +theories/IntMap/Mapaxioms.vo: theories/IntMap/Mapaxioms.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Adist.vo: theories/IntMap/Adist.v theories/Bool/Bool.vo theories/Zarith/ZArith.vo theories/Arith/Arith.vo theories/Arith/Min.vo theories/IntMap/Addr.vo theories/IntMap/Addr.vo: theories/IntMap/Addr.v theories/Bool/Bool.vo theories/Zarith/ZArith.vo -theories/TOADD/cuiht.vo: theories/TOADD/cuiht.v theories/Lists/PolyList.vo theories/Bool/BoolEq.vo -theories/TOADD/zimmermann.vo: theories/TOADD/zimmermann.v theories/Zarith/ZArith.vo contrib/omega/Omega.vo -theories/Num/Definitions.vo: theories/Num/Definitions.v -theories/Num/NatSyntax.vo: theories/Num/NatSyntax.v +theories/IntMap/Addec.vo: theories/IntMap/Addec.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Zarith/ZArith.vo theories/IntMap/Addr.vo +theories/IntMap/Allmaps.vo: theories/IntMap/Allmaps.v theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Mapiter.vo theories/IntMap/Mapsubset.vo theories/IntMap/Lsort.vo theories/IntMap/Mapfold.vo theories/IntMap/Mapcard.vo theories/IntMap/Mapcanon.vo theories/IntMap/Mapc.vo theories/IntMap/Maplists.vo theories/IntMap/Adalloc.vo +theories/IntMap/Adalloc.vo: theories/IntMap/Adalloc.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Zarith/ZArith.vo theories/Arith/Arith.vo theories/IntMap/Addr.vo theories/IntMap/Adist.vo theories/IntMap/Addec.vo theories/IntMap/Map.vo theories/IntMap/Fset.vo +theories/Num/Nat/NeqDef.vo: theories/Num/Nat/NeqDef.v theories/Num/Params.vo +theories/Num/Nat/NSyntax.vo: theories/Num/Nat/NSyntax.v +theories/Num/Nat/Axioms.vo: theories/Num/Nat/Axioms.v theories/Num/Params.vo theories/Num/EqAxioms.vo theories/Num/NSyntax.vo +theories/Num/Params.vo: theories/Num/Params.v +theories/Num/NeqDef.vo: theories/Num/NeqDef.v theories/Num/Params.vo theories/Num/EqParams.vo +theories/Num/EqParams.vo: theories/Num/EqParams.v theories/Num/Params.vo +theories/Num/EqAxioms.vo: theories/Num/EqAxioms.v theories/Num/Params.vo theories/Num/EqParams.vo theories/Num/NeqDef.vo theories/Num/NSyntax.vo theories/Num/SubProps.vo: theories/Num/SubProps.v theories/Num/OppProps.vo: theories/Num/OppProps.v theories/Num/OppAxioms.vo: theories/Num/OppAxioms.v -theories/Num/GeProps.vo: theories/Num/GeProps.v -theories/Num/GtProps.vo: theories/Num/GtProps.v -theories/Num/LeProps.vo: theories/Num/LeProps.v theories/Num/LtProps.vo theories/Num/LeAxioms.vo -theories/Num/DiscrAxioms.vo: theories/Num/DiscrAxioms.v theories/Num/Params.vo theories/Num/NSyntax.vo -theories/Num/DiscrProps.vo: theories/Num/DiscrProps.v theories/Num/DiscrAxioms.vo theories/Num/LtProps.vo -theories/Num/LtProps.vo: theories/Num/LtProps.v theories/Num/Axioms.vo theories/Num/AddProps.vo theories/Num/NSyntax.vo: theories/Num/NSyntax.v theories/Num/Params.vo -theories/Num/EqParams.vo: theories/Num/EqParams.v theories/Num/Params.vo +theories/Num/LtProps.vo: theories/Num/LtProps.v theories/Num/Axioms.vo theories/Num/AddProps.vo +theories/Num/LeProps.vo: theories/Num/LeProps.v theories/Num/LtProps.vo theories/Num/LeAxioms.vo +theories/Num/LeAxioms.vo: theories/Num/LeAxioms.v theories/Num/Axioms.vo theories/Num/LtProps.vo +theories/Num/GtProps.vo: theories/Num/GtProps.v +theories/Num/GtAxioms.vo: theories/Num/GtAxioms.v theories/Num/Axioms.vo theories/Num/LeProps.vo +theories/Num/GeProps.vo: theories/Num/GeProps.v theories/Num/GeAxioms.vo: theories/Num/GeAxioms.v theories/Num/Axioms.vo theories/Num/LtProps.vo -theories/Num/Leibniz/NSyntax.vo: theories/Num/Leibniz/NSyntax.v theories/Num/Params.vo +theories/Num/DiscrProps.vo: theories/Num/DiscrProps.v theories/Num/DiscrAxioms.vo theories/Num/LtProps.vo theories/Num/Leibniz/Params.vo: theories/Num/Leibniz/Params.v +theories/Num/Leibniz/NSyntax.vo: theories/Num/Leibniz/NSyntax.v theories/Num/Params.vo theories/Num/Leibniz/EqAxioms.vo: theories/Num/Leibniz/EqAxioms.v theories/Num/NSyntax.vo -theories/Num/GtAxioms.vo: theories/Num/GtAxioms.v theories/Num/Axioms.vo theories/Num/LeProps.vo -theories/Num/EqAxioms.vo: theories/Num/EqAxioms.v theories/Num/Params.vo theories/Num/EqParams.vo theories/Num/NeqDef.vo theories/Num/NSyntax.vo -theories/Num/AddProps.vo: theories/Num/AddProps.v theories/Num/Axioms.vo theories/Num/EqAxioms.vo -theories/Num/LeAxioms.vo: theories/Num/LeAxioms.v theories/Num/Axioms.vo theories/Num/LtProps.vo +theories/Num/DiscrAxioms.vo: theories/Num/DiscrAxioms.v theories/Num/Params.vo theories/Num/NSyntax.vo theories/Num/Axioms.vo: theories/Num/Axioms.v theories/Num/Params.vo theories/Num/EqParams.vo theories/Num/NeqDef.vo theories/Num/NSyntax.vo -theories/Num/Params.vo: theories/Num/Params.v -theories/Num/Nat/Params.vo: theories/Num/Nat/Params.v -theories/Num/Nat/EqAxioms.vo: theories/Num/Nat/EqAxioms.v theories/Num/NSyntax.vo -theories/Num/Nat/NeqDef.vo: theories/Num/Nat/NeqDef.v theories/Num/Params.vo -theories/Num/Nat/NSyntax.vo: theories/Num/Nat/NSyntax.v -theories/Num/Nat/Axioms.vo: theories/Num/Nat/Axioms.v theories/Num/Params.vo theories/Num/EqAxioms.vo theories/Num/NSyntax.vo -theories/Num/NeqDef.vo: theories/Num/NeqDef.v theories/Num/Params.vo theories/Num/EqParams.vo +theories/Num/AddProps.vo: theories/Num/AddProps.v theories/Num/Axioms.vo theories/Num/EqAxioms.vo +theories/Num/Definitions.vo: theories/Num/Definitions.v +theories/Zarith/zarith_aux.vo: theories/Zarith/zarith_aux.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo +theories/Zarith/fast_integer.vo: theories/Zarith/fast_integer.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Minus.vo +theories/Zarith/auxiliary.vo: theories/Zarith/auxiliary.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Logic/Decidable.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo +theories/Zarith/Zsyntax.vo: theories/Zarith/Zsyntax.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo +theories/Zarith/Zmisc.vo: theories/Zarith/Zmisc.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Bool/Bool.vo +theories/Zarith/ZArith_dec.vo: theories/Zarith/ZArith_dec.v theories/Bool/Sumbool.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo +theories/Zarith/Wf_Z.vo: theories/Zarith/Wf_Z.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo +theories/Zarith/ZArith.vo: theories/Zarith/ZArith.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Zarith/ZArith_dec.vo theories/Zarith/Zmisc.vo theories/Zarith/Wf_Z.vo theories/Wellfounded/Wellfounded.vo: theories/Wellfounded/Wellfounded.v theories/Wellfounded/Disjoint_Union.vo theories/Wellfounded/Inclusion.vo theories/Wellfounded/Inverse_Image.vo theories/Wellfounded/Lexicographic_Exponentiation.vo theories/Wellfounded/Lexicographic_Product.vo theories/Wellfounded/Transitive_Closure.vo theories/Wellfounded/Union.vo theories/Wellfounded/Well_Ordering.vo theories/Wellfounded/Well_Ordering.vo: theories/Wellfounded/Well_Ordering.v theories/Logic/Eqdep.vo theories/Wellfounded/Union.vo: theories/Wellfounded/Union.v theories/Relations/Relation_Operators.vo theories/Relations/Relation_Definitions.vo theories/Wellfounded/Transitive_Closure.vo @@ -287,14 +301,6 @@ theories/Wellfounded/Lexicographic_Exponentiation.vo: theories/Wellfounded/Lexic theories/Wellfounded/Inverse_Image.vo: theories/Wellfounded/Inverse_Image.v theories/Wellfounded/Inclusion.vo: theories/Wellfounded/Inclusion.v theories/Relations/Relation_Definitions.vo theories/Wellfounded/Disjoint_Union.vo: theories/Wellfounded/Disjoint_Union.v theories/Relations/Relation_Operators.vo -theories/Zarith/fast_integer.vo: theories/Zarith/fast_integer.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Minus.vo -theories/Zarith/zarith_aux.vo: theories/Zarith/zarith_aux.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo -theories/Zarith/auxiliary.vo: theories/Zarith/auxiliary.v theories/Arith/Arith.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Logic/Decidable.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo -theories/Zarith/Zsyntax.vo: theories/Zarith/Zsyntax.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo -theories/Zarith/Zmisc.vo: theories/Zarith/Zmisc.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Bool/Bool.vo -theories/Zarith/ZArith_dec.vo: theories/Zarith/ZArith_dec.v theories/Bool/Sumbool.vo theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo -theories/Zarith/Wf_Z.vo: theories/Zarith/Wf_Z.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo -theories/Zarith/ZArith.vo: theories/Zarith/ZArith.v theories/Zarith/fast_integer.vo theories/Zarith/zarith_aux.vo theories/Zarith/auxiliary.vo theories/Zarith/Zsyntax.vo theories/Zarith/ZArith_dec.vo theories/Zarith/Zmisc.vo theories/Zarith/Wf_Z.vo theories/Sets/Uniset.vo: theories/Sets/Uniset.v theories/Bool/Bool.vo theories/Sets/Permut.vo theories/Sets/Relations_3_facts.vo: theories/Sets/Relations_3_facts.v theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Relations_2.vo theories/Sets/Relations_2_facts.vo theories/Sets/Relations_3.vo theories/Sets/Relations_3.vo: theories/Sets/Relations_3.v theories/Sets/Relations_1.vo theories/Sets/Relations_2.vo @@ -323,13 +329,13 @@ theories/Relations/Relation_Operators.vo: theories/Relations/Relation_Operators. theories/Relations/Relation_Definitions.vo: theories/Relations/Relation_Definitions.v theories/Relations/Operators_Properties.vo: theories/Relations/Operators_Properties.v theories/Relations/Relation_Definitions.vo theories/Relations/Relation_Operators.vo theories/Relations/Newman.vo: theories/Relations/Newman.v theories/Relations/Rstar.vo -theories/Reals/Rsyntax.vo: theories/Reals/Rsyntax.v theories/Reals/Rdefinitions.vo -theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/Zarith/ZArith.vo theories/Reals/TypeSyntax.vo theories/Reals/TypeSyntax.vo: theories/Reals/TypeSyntax.v +theories/Reals/Rsyntax.vo: theories/Reals/Rsyntax.v theories/Reals/Rdefinitions.vo theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbasic_fun.vo theories/Logic/Classical_Prop.vo theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rlimit.vo theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/Rlimit.vo theories/Reals/Rfunctions.vo theories/Reals/Rderiv.vo theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rfunctions.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo +theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/Zarith/ZArith.vo theories/Reals/TypeSyntax.vo theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/R_Ifp.vo theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo @@ -342,14 +348,23 @@ theories/Logic/Classical_Prop.vo: theories/Logic/Classical_Prop.v theories/Logic/Classical_Pred_Type.vo: theories/Logic/Classical_Pred_Type.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Set.vo: theories/Logic/Classical_Pred_Set.v theories/Logic/Classical_Prop.vo theories/Logic/Classical.vo: theories/Logic/Classical.v theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Set.vo -theories/Lists/PolyListSyntax.vo: theories/Lists/PolyListSyntax.v theories/Lists/PolyList.vo -theories/Lists/Program.vo: theories/Lists/Program.v tactics/Refine.vo theories/Lists/TheoryList.vo: theories/Lists/TheoryList.v theories/Lists/PolyList.vo theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Minus.vo theories/Bool/DecBool.vo theories/Lists/Streams.vo: theories/Lists/Streams.v +theories/Lists/PolyListSyntax.vo: theories/Lists/PolyListSyntax.v theories/Lists/PolyList.vo theories/Lists/PolyList.vo: theories/Lists/PolyList.v theories/Arith/Le.vo theories/Lists/List.vo: theories/Lists/List.v theories/Arith/Le.vo theories/Lists/ListSet.vo: theories/Lists/ListSet.v theories/Lists/PolyList.vo -theories/Bool/BoolEq.vo: theories/Bool/BoolEq.v theories/Bool/Bool.vo +theories/Init/Wf.vo: theories/Init/Wf.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo +theories/Init/SpecifSyntax.vo: theories/Init/SpecifSyntax.v theories/Init/LogicSyntax.vo theories/Init/Specif.vo +theories/Init/Specif.vo: theories/Init/Specif.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Datatypes.vo +theories/Init/Prelude.vo: theories/Init/Prelude.v theories/Init/Datatypes.vo theories/Init/DatatypesSyntax.vo theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Specif.vo theories/Init/SpecifSyntax.vo theories/Init/Peano.vo theories/Init/Wf.vo +theories/Init/Peano.vo: theories/Init/Peano.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Datatypes.vo +theories/Init/Logic_TypeSyntax.vo: theories/Init/Logic_TypeSyntax.v theories/Init/Logic_Type.vo +theories/Init/Logic_Type.vo: theories/Init/Logic_Type.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo +theories/Init/LogicSyntax.vo: theories/Init/LogicSyntax.v theories/Init/Logic.vo +theories/Init/Logic.vo: theories/Init/Logic.v theories/Init/Datatypes.vo +theories/Init/DatatypesSyntax.vo: theories/Init/DatatypesSyntax.v theories/Init/Datatypes.vo +theories/Init/Datatypes.vo: theories/Init/Datatypes.v theories/Bool/Zerob.vo: theories/Bool/Zerob.v theories/Arith/Arith.vo theories/Bool/Bool.vo theories/Bool/Sumbool.vo: theories/Bool/Sumbool.v theories/Bool/IfProp.vo: theories/Bool/IfProp.v theories/Bool/Bool.vo @@ -374,14 +389,3 @@ theories/Arith/Compare_dec.vo: theories/Arith/Compare_dec.v theories/Arith/Le.vo theories/Arith/Compare.vo: theories/Arith/Compare.v theories/Arith/Arith.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo theories/Arith/Min.vo theories/Arith/Arith.vo: theories/Arith/Arith.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo theories/Arith/Between.vo: theories/Arith/Between.v theories/Arith/Le.vo theories/Arith/Lt.vo -theories/Init/Wf.vo: theories/Init/Wf.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo -theories/Init/SpecifSyntax.vo: theories/Init/SpecifSyntax.v theories/Init/LogicSyntax.vo theories/Init/Specif.vo -theories/Init/Specif.vo: theories/Init/Specif.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Datatypes.vo -theories/Init/Prelude.vo: theories/Init/Prelude.v theories/Init/Datatypes.vo theories/Init/DatatypesSyntax.vo theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Specif.vo theories/Init/SpecifSyntax.vo theories/Init/Peano.vo theories/Init/Wf.vo -theories/Init/Peano.vo: theories/Init/Peano.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Datatypes.vo -theories/Init/Logic_TypeSyntax.vo: theories/Init/Logic_TypeSyntax.v theories/Init/Logic_Type.vo -theories/Init/Logic_Type.vo: theories/Init/Logic_Type.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo -theories/Init/LogicSyntax.vo: theories/Init/LogicSyntax.v theories/Init/Logic.vo -theories/Init/Logic.vo: theories/Init/Logic.v theories/Init/Datatypes.vo -theories/Init/DatatypesSyntax.vo: theories/Init/DatatypesSyntax.v theories/Init/Datatypes.vo -theories/Init/Datatypes.vo: theories/Init/Datatypes.v @@ -200,8 +200,8 @@ ML4FILES += contrib/correctness/psyntax.ml4 CONTRIB=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \ contrib/ring/quote.cmo contrib/ring/ring.cmo \ contrib/xml/xml.cmo \ - contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo -# $(CORRECTNESSCMO) + contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo \ + $(EXTRACTIONCMO) CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) @@ -279,9 +279,6 @@ toplevel: $(TOPLEVEL) # special binaries for debugging -bin/coq-extraction: $(COQMKTOP) $(CMO) $(USERTACCMO) $(EXTRACTIONCMO) - $(COQMKTOP) -top $(INCLUDES) $(CAMLDEBUG) -o $@ $(EXTRACTIONCMO) - bin/coq-interface: $(COQMKTOP) $(CMO) $(USERTACCMO) $(INTERFACE) $(COQMKTOP) -top $(INCLUDES) $(CAMLDEBUG) -o $@ $(INTERFACE) @@ -322,13 +319,18 @@ theories/Init/%.vo: theories/Init/%.v states/barestate.coq $(COQC) init: $(INITVO) +EXTRACTIONVO=contrib/extraction/Extraction.vo + TACTICSVO=tactics/Equality.vo tactics/Tauto.vo tactics/Inv.vo \ tactics/EAuto.vo tactics/AutoRewrite.vo tactics/Refine.vo \ - tactics/EqDecide.vo + tactics/EqDecide.vo $(EXTRACTIONVO) tactics/%.vo: tactics/%.v states/barestate.coq $(COQC) $(COQC) -$(BEST) -bindir bin -q -I tactics -is states/barestate.coq $< +contrib/extraction/%.vo: contrib/extraction/%.v states/barestate.coq $(COQC) + $(COQC) -$(BEST) -bindir bin -q -I tactics -is states/barestate.coq $< + states/initial.coq: states/barestate.coq states/MakeInitial.v $(INITVO) $(TACTICSVO) $(BESTCOQTOP) $(BESTCOQTOP) -q -batch -silent -is states/barestate.coq -I tactics -R theories Coq -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq @@ -436,10 +438,6 @@ clean:: # contribs ########################################################################### -EXTRACTIONVO=contrib/extraction/Extraction.vo -contrib/extraction/%.vo: contrib/extraction/%.v - $(COQC) -q -byte -bindir bin $(COQINCLUDES) $< - CORRECTNESSVO=contrib/correctness/Arrays.vo \ contrib/correctness/Correctness.vo \ contrib/correctness/Exchange.vo \ @@ -470,7 +468,7 @@ contrib/interface/Centaur.vo: contrib/interface/Centaur.v $(INTERFACE) contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) $(COQC) -q -byte -bindir bin $(COQINCLUDES) $< -CONTRIBVO = $(OMEGAVO) $(RINGVO) $(XMLVO) $(EXTRACTIONVO) +CONTRIBVO = $(OMEGAVO) $(RINGVO) $(XMLVO) $(CONTRIBVO): states/initial.coq @@ -570,8 +568,7 @@ install-binaries: $(MKDIR) $(FULLBINDIR) cp $(COQDEP) $(GALLINA) $(COQMAKEFILE) $(COQTEX) $(FULLBINDIR) -LIBFILES=$(INITVO) $(TACTICSVO) $(THEORIESVO) $(CONTRIBVO) \ - $(EXTRACTIONCMO) +LIBFILES=$(INITVO) $(TACTICSVO) $(THEORIESVO) $(CONTRIBVO) install-library: $(MKDIR) $(FULLCOQLIB) diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml index 170a56b28..cf233a988 100644 --- a/contrib/correctness/pcic.ml +++ b/contrib/correctness/pcic.ml @@ -89,8 +89,8 @@ let sig_n n = mind_entry_consnames = [ cname ]; mind_entry_lc = [ lc ] } ] } -let pair = ConstructRef ((coq_constant ["Init"; "Datatypes"] "pair",0),1) -let exist = ConstructRef ((coq_constant ["Init"; "Specif"] "exist",0),1) +let pair = ConstructRef ((coq_constant ["Init"; "Datatypes"] "prod",0),1) +let exist = ConstructRef ((coq_constant ["Init"; "Specif"] "sig",0),1) let tuple_ref dep n = if n = 2 & not dep then diff --git a/contrib/correctness/pred.ml b/contrib/correctness/pred.ml index d6f9e0e72..c71c91f93 100644 --- a/contrib/correctness/pred.ml +++ b/contrib/correctness/pred.ml @@ -29,9 +29,9 @@ let is_eta_redex bl al = Invalid_argument("List.for_all2") -> false let rec red = function - CC_letin (dep, ty, bl, e1, e2) -> + | CC_letin (dep, ty, bl, e1, e2) -> begin match red e2 with - CC_tuple (false,tl,al) -> + | CC_tuple (false,tl,al) -> if is_eta_redex bl al then red e1 else diff --git a/contrib/correctness/preuves.v b/contrib/correctness/preuves.v index 22eccbdba..730a25fd4 100644 --- a/contrib/correctness/preuves.v +++ b/contrib/correctness/preuves.v @@ -28,10 +28,15 @@ Save. Global Variable i : Z ref. Debug on. -Correctness assign1 { `0 <= i` } begin i := !i + 1 end { `0 < i` }. +Correctness assign1 { `0 <= i` } (i := !i + 1) { `0 < i` }. +Omega. +Save. (**********************************************************************) +Global Variable i : Z ref. +Debug on. +Correctness if0 { `0 <= i` } (if !i>0 then i:=!i-1 else tt) { `0 <= i` }. (**********************************************************************) Correctness echange diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml index b8ac08531..45ab72c38 100644 --- a/contrib/correctness/ptactic.ml +++ b/contrib/correctness/ptactic.ml @@ -105,16 +105,16 @@ let eq = IndRef (coq_constant ["Init";"Logic"] "eq", 0) (* ["(well_founded nat lt)"] *) let wf_nat_pattern = PApp (PRef well_founded, [| PRef nat; PRef lt |]) -(* ["((well_founded Z (Zwf ?))"] *) +(* ["((well_founded Z (Zwf ?1))"] *) let wf_z_pattern = let zwf = ConstRef (coq_constant ["correctness";"Zwf"] "Zwf") in - PApp (PRef well_founded, [| PRef z; PApp (PRef zwf, [| PMeta None |]) |]) -(* ["(and ? ?)"] *) + PApp (PRef well_founded, [| PRef z; PApp (PRef zwf, [| PMeta (Some 1) |]) |]) +(* ["(and ?1 ?2)"] *) let and_pattern = - PApp (PRef and_, [| PMeta None; PMeta None |]) -(* ["(eq ? ? ?)"] *) + PApp (PRef and_, [| PMeta (Some 1); PMeta (Some 2) |]) +(* ["(eq ?1 ?2 ?3)"] *) let eq_pattern = - PApp (PRef eq, [| PMeta None; PMeta None; PMeta None |]) + PApp (PRef eq, [| PMeta (Some 1); PMeta (Some 2); PMeta (Some 3) |]) (* loop_ids: remove loop<i> hypotheses from the context, and rewrite * using Variant<i> hypotheses when needed. *) diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v index 472cee1af..c4c62b3cb 100644 --- a/contrib/extraction/Extraction.v +++ b/contrib/extraction/Extraction.v @@ -6,17 +6,17 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -Declare ML Module "mlutil" "ocaml" "extraction" "extract_env". - Grammar vernac vernac : ast := extr_constr [ "Extraction" constrarg($c) "." ] -> [ (Extraction $c) ] | extr_list [ "Recursive" "Extraction" ne_qualidarg_list($l) "." ] -> [ (ExtractionRec ($LIST $l)) ] -| extr_list [ "Extraction" stringarg($f) ne_qualidarg_list($l) "." ] -> - [ (ExtractionFile $f ($LIST $l)) ] -| extr_module [ "Extraction" "Module" identarg($m) "." ] -> - [ (ExtractionModule $m) ] +| extr_list + [ "Extraction" options($o) stringarg($f) ne_qualidarg_list($l) "." ] + -> [ (ExtractionFile $o $f ($LIST $l)) ] +| extr_module + [ "Extraction" options($o) "Module" identarg($m) "." ] + -> [ (ExtractionModule $o $m) ] | extract_constant [ "Extract" "Constant" qualidarg($x) "=>" idorstring($y) "." ] @@ -36,4 +36,10 @@ with idorstring_list: List := with idorstring : ast := ids_ident [ identarg($id) ] -> [ $id ] -| ids_string [ stringarg($s) ] -> [ $s ]. +| ids_string [ stringarg($s) ] -> [ $s ] + +with options : ast := +| ext_opt_noopt [ "noopt" ] -> [ (VERNACARGLIST "noopt") ] +| ext_op_expand [ "expand" "[" ne_qualidarg_list($l) "]" ] -> + [ (VERNACARGLIST "expand" ($LIST $l)) ] +| ext_opt_none [ ] -> [ (VERNACARGLIST "nooption") ]. diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 9e87cc9ac..b0bb1ad3a 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -144,16 +144,35 @@ let reference_of_varg = function (try Nametab.locate q with Not_found -> no_such_reference q) | _ -> assert false -let decl_of_vargl vl = - let rl = List.map reference_of_varg vl in - List.map extract_declaration (extract_env rl) +let refs_of_vargl = List.map reference_of_varg + +let refs_set_of_list l = List.fold_right Refset.add l Refset.empty + +let decl_of_refs refs = + List.map extract_declaration (extract_env refs) let _ = vinterp_add "ExtractionRec" (fun vl () -> - let rl' = decl_of_vargl vl in + let rl' = decl_of_refs (refs_of_vargl vl) in List.iter (fun d -> mSGNL (Pp.pp_decl d)) rl') +(*s Extraction parameters. *) + +let interp_options keep modular = function + | [VARG_STRING "noopt"] -> + { no_opt = true; modular = modular; + to_keep = refs_set_of_list keep; to_expand = Refset.empty } + | [VARG_STRING "nooption"] -> + { no_opt = false; modular = modular; + to_keep = refs_set_of_list keep; to_expand = Refset.empty } + | VARG_STRING "expand" :: l -> + { no_opt = false; modular = modular; + to_keep = refs_set_of_list keep; + to_expand = refs_set_of_list (refs_of_vargl l) } + | _ -> + assert false + (*s Extraction to a file (necessarily recursive). The vernacular command is \verb!Extraction "file"! [qualid1] ... [qualidn]. We just call [extract_to_file] on the saturated environment. *) @@ -161,8 +180,10 @@ let _ = let _ = vinterp_add "ExtractionFile" (function - | VARG_STRING f :: vl -> - (fun () -> Ocaml.extract_to_file f false (decl_of_vargl vl)) + | VARG_VARGLIST o :: VARG_STRING f :: vl -> + let refs = refs_of_vargl vl in + let prm = interp_options refs false o in + (fun () -> Ocaml.extract_to_file f prm (decl_of_refs refs)) | _ -> assert false) (*s Extraction of a module. The vernacular command is \verb!Extraction Module! @@ -190,10 +211,11 @@ let extract_module m = let _ = vinterp_add "ExtractionModule" (function - | [VARG_IDENTIFIER m] -> + | [VARG_VARGLIST o; VARG_IDENTIFIER m] -> (fun () -> let m = Names.string_of_id m in Ocaml.current_module := m; let f = (String.uncapitalize m) ^ ".ml" in - Ocaml.extract_to_file f true (extract_module m)) + let prm = interp_options [] true o in + Ocaml.extract_to_file f prm (extract_module m)) | _ -> assert false) diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index de77687fb..4b04c4dec 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -195,11 +195,61 @@ let uncurrify_decl = function | d -> d -(*s Table for direct ML extractions. *) +(*s Optimization. *) module Refset = Set.Make(struct type t = global_reference let compare = compare end) +type extraction_params = { + modular : bool; (* modular extraction *) + no_opt : bool; (* no optimization at all *) + to_keep : Refset.t; (* globals to keep *) + to_expand : Refset.t; (* globals to expand *) +} + +let ml_subst_glob r m = + let rec substrec = function + | MLglob r' as t -> if r = r' then m else t + | t -> ast_map substrec t + in + substrec + +let expand r m = function + | Dglob(r',t') -> Dglob(r', ml_subst_glob r m t') + | d -> d + +let normalize = betared_ast + +let keep prm r t' = true + (* prm.no_opt || Refset.mem r prm.to_keep *) + +let warning_expansion r = + wARN (hOV 0 [< 'sTR "The constant"; 'sPC; + Printer.pr_global r; 'sPC; 'sTR "is expanded." >]) + +let rec optimize prm = function + | [] -> + [] + | (Dtype _ | Dabbrev _) as d :: l -> + d :: (optimize prm l) + (*i + | Dglob(id,(MLexn _ as t)) as d :: l -> + let l' = List.map (expand (id,t)) l in optimize prm l' + i*) + | [ Dglob(r,t) ] -> + let t' = normalize t in [ Dglob(r,t') ] + | Dglob(r,t) as d :: l -> + let t' = normalize t in + if keep prm r t' then + (Dglob(r,t')) :: (optimize prm l) + else begin + warning_expansion r; + let l' = List.map (expand r t') l in + optimize prm l' + end + +(*s Table for direct ML extractions. *) + module Refmap = Map.Make(struct type t = global_reference let compare = compare end) diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli index b68d4a954..af931b648 100644 --- a/contrib/extraction/mlutil.mli +++ b/contrib/extraction/mlutil.mli @@ -39,10 +39,21 @@ val betared_decl : ml_decl -> ml_decl val uncurrify_ast : ml_ast -> ml_ast val uncurrify_decl : ml_decl -> ml_decl -(*s Table for direct extractions to ML values. *) +(*s Optimization. *) module Refset : Set.S with type elt = global_reference +type extraction_params = { + modular : bool; (* modular extraction *) + no_opt : bool; (* no optimization at all *) + to_keep : Refset.t; (* globals to keep *) + to_expand : Refset.t; (* globals to expand *) +} + +val optimize : extraction_params -> ml_decl list -> ml_decl list + +(*s Table for direct extractions to ML values. *) + val is_ml_extraction : global_reference -> bool val find_ml_extraction : global_reference -> string diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index a7b96d8e9..2d0518d92 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -438,8 +438,9 @@ let ocaml_preamble () = 'sTR "type arity = unit"; 'fNL; 'sTR "let arity = ()"; 'fNL; 'fNL >] -let extract_to_file f modular decls = - let pp_decl = if modular then ModularPp.pp_decl else MonoPp.pp_decl in +let extract_to_file f prm decls = + let decls = optimize prm decls in + let pp_decl = if prm.modular then ModularPp.pp_decl else MonoPp.pp_decl in let cout = open_out f in let ft = Pp_control.with_output_to cout in pP_with ft (hV 0 (ocaml_preamble ())); diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli index 1a0cfec0c..74d751051 100644 --- a/contrib/extraction/ocaml.mli +++ b/contrib/extraction/ocaml.mli @@ -13,12 +13,11 @@ declarations to a file. *) open Miniml +open Mlutil module Make : functor(P : Mlpp_param) -> Mlpp -(* The boolean indicates if the extraction is modular. *) - val current_module : string ref -val extract_to_file : string -> bool -> ml_decl list -> unit +val extract_to_file : string -> extraction_params -> ml_decl list -> unit diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 1f4767704..e42223f4b 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -100,7 +100,7 @@ GEXTEND Gram <:ast< (PrintHintGoal) >> | IDENT "Print"; IDENT "HintDb"; s = identarg -> <:ast< (PrintHintDb $s) >> - | IDENT "Print"; IDENT "Section"; s = identarg -> + | IDENT "Print"; IDENT "Section"; s = qualidarg -> <:ast< (PrintSec $s) >> | IDENT "Print"; IDENT "States" -> <:ast< (PrintStates) >> (* This should be in "syntax" section but is here for factorization *) diff --git a/states/MakeInitial.v b/states/MakeInitial.v index 55b824e54..3997ae321 100644 --- a/states/MakeInitial.v +++ b/states/MakeInitial.v @@ -15,3 +15,4 @@ Require Export EAuto. Require Export AutoRewrite. Require Export Refine. Require Export EqDecide. +Require Export Extraction. diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 52f3a7935..124f9e9f1 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -165,15 +165,19 @@ let valid_loc dloc (b,e) = let valid_buffer_loc ib dloc (b,e) = valid_loc dloc (b,e) & b-ib.start >= 0 & e-ib.start < ib.len & b<=e - + +(*s The Coq prompt is the name of the focused proof, if any, and "Coq" + otherwise. We trap all exceptions to prevent the error message printing + from cycling. *) +let make_prompt () = + try + (Names.string_of_id (Pfedit.get_current_proof_name ())) ^ " < " + with _ -> + "Coq < " + (* A buffer to store the current command read on stdin. It is * initialized when a vernac command is immediately followed by "\n", * or after a Drop. *) -let make_prompt () = - if Pfedit.refining () then - (Names.string_of_id (Pfedit.get_current_proof_name ()))^" < " - else "Coq < " - let top_buffer = let pr() = (make_prompt())^(emacs_str (String.make 1 (Char.chr 249))) in |