diff options
Diffstat (limited to 'contrib/extraction/test')
36 files changed, 1424 insertions, 0 deletions
diff --git a/contrib/extraction/test/.depend b/contrib/extraction/test/.depend new file mode 100644 index 00000000..641b50a7 --- /dev/null +++ b/contrib/extraction/test/.depend @@ -0,0 +1,713 @@ +theories/Arith/arith.cmo: theories/Arith/arith.cmi +theories/Arith/arith.cmx: theories/Arith/arith.cmi +theories/Arith/between.cmo: theories/Arith/between.cmi +theories/Arith/between.cmx: theories/Arith/between.cmi +theories/Arith/bool_nat.cmo: theories/Arith/compare_dec.cmi \ + theories/Init/datatypes.cmi theories/Arith/peano_dec.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi \ + theories/Arith/bool_nat.cmi +theories/Arith/bool_nat.cmx: theories/Arith/compare_dec.cmx \ + theories/Init/datatypes.cmx theories/Arith/peano_dec.cmx \ + theories/Init/specif.cmx theories/Bool/sumbool.cmx \ + theories/Arith/bool_nat.cmi +theories/Arith/compare_dec.cmo: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/Arith/compare_dec.cmi +theories/Arith/compare_dec.cmx: theories/Init/datatypes.cmx \ + theories/Init/specif.cmx theories/Arith/compare_dec.cmi +theories/Arith/compare.cmo: theories/Arith/compare_dec.cmi \ + theories/Init/datatypes.cmi theories/Init/specif.cmi \ + theories/Arith/compare.cmi +theories/Arith/compare.cmx: theories/Arith/compare_dec.cmx \ + theories/Init/datatypes.cmx theories/Init/specif.cmx \ + theories/Arith/compare.cmi +theories/Arith/div2.cmo: theories/Init/datatypes.cmi theories/Init/peano.cmi \ + theories/Init/specif.cmi theories/Arith/div2.cmi +theories/Arith/div2.cmx: theories/Init/datatypes.cmx theories/Init/peano.cmx \ + theories/Init/specif.cmx theories/Arith/div2.cmi +theories/Arith/eqNat.cmo: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/Arith/eqNat.cmi +theories/Arith/eqNat.cmx: theories/Init/datatypes.cmx \ + theories/Init/specif.cmx theories/Arith/eqNat.cmi +theories/Arith/euclid.cmo: theories/Arith/compare_dec.cmi \ + theories/Init/datatypes.cmi theories/Init/specif.cmi \ + theories/Arith/euclid.cmi +theories/Arith/euclid.cmx: theories/Arith/compare_dec.cmx \ + theories/Init/datatypes.cmx theories/Init/specif.cmx \ + theories/Arith/euclid.cmi +theories/Arith/even.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \ + theories/Arith/even.cmi +theories/Arith/even.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \ + theories/Arith/even.cmi +theories/Arith/factorial.cmo: theories/Init/datatypes.cmi \ + theories/Init/peano.cmi theories/Arith/factorial.cmi +theories/Arith/factorial.cmx: theories/Init/datatypes.cmx \ + theories/Init/peano.cmx theories/Arith/factorial.cmi +theories/Arith/gt.cmo: theories/Arith/gt.cmi +theories/Arith/gt.cmx: theories/Arith/gt.cmi +theories/Arith/le.cmo: theories/Arith/le.cmi +theories/Arith/le.cmx: theories/Arith/le.cmi +theories/Arith/lt.cmo: theories/Arith/lt.cmi +theories/Arith/lt.cmx: theories/Arith/lt.cmi +theories/Arith/max.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \ + theories/Arith/max.cmi +theories/Arith/max.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \ + theories/Arith/max.cmi +theories/Arith/min.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \ + theories/Arith/min.cmi +theories/Arith/min.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \ + theories/Arith/min.cmi +theories/Arith/minus.cmo: theories/Arith/minus.cmi +theories/Arith/minus.cmx: theories/Arith/minus.cmi +theories/Arith/mult.cmo: theories/Init/datatypes.cmi theories/Arith/plus.cmi \ + theories/Arith/mult.cmi +theories/Arith/mult.cmx: theories/Init/datatypes.cmx theories/Arith/plus.cmx \ + theories/Arith/mult.cmi +theories/Arith/peano_dec.cmo: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/Arith/peano_dec.cmi +theories/Arith/peano_dec.cmx: theories/Init/datatypes.cmx \ + theories/Init/specif.cmx theories/Arith/peano_dec.cmi +theories/Arith/plus.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \ + theories/Arith/plus.cmi +theories/Arith/plus.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \ + theories/Arith/plus.cmi +theories/Arith/wf_nat.cmo: theories/Init/datatypes.cmi \ + theories/Arith/wf_nat.cmi +theories/Arith/wf_nat.cmx: theories/Init/datatypes.cmx \ + theories/Arith/wf_nat.cmi +theories/Bool/boolEq.cmo: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/Bool/boolEq.cmi +theories/Bool/boolEq.cmx: theories/Init/datatypes.cmx \ + theories/Init/specif.cmx theories/Bool/boolEq.cmi +theories/Bool/bool.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \ + theories/Bool/bool.cmi +theories/Bool/bool.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \ + theories/Bool/bool.cmi +theories/Bool/bvector.cmo: theories/Bool/bool.cmi theories/Init/datatypes.cmi \ + theories/Init/peano.cmi theories/Bool/bvector.cmi +theories/Bool/bvector.cmx: theories/Bool/bool.cmx theories/Init/datatypes.cmx \ + theories/Init/peano.cmx theories/Bool/bvector.cmi +theories/Bool/decBool.cmo: theories/Init/specif.cmi theories/Bool/decBool.cmi +theories/Bool/decBool.cmx: theories/Init/specif.cmx theories/Bool/decBool.cmi +theories/Bool/ifProp.cmo: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/Bool/ifProp.cmi +theories/Bool/ifProp.cmx: theories/Init/datatypes.cmx \ + theories/Init/specif.cmx theories/Bool/ifProp.cmi +theories/Bool/sumbool.cmo: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi +theories/Bool/sumbool.cmx: theories/Init/datatypes.cmx \ + theories/Init/specif.cmx theories/Bool/sumbool.cmi +theories/Bool/zerob.cmo: theories/Init/datatypes.cmi theories/Bool/zerob.cmi +theories/Bool/zerob.cmx: theories/Init/datatypes.cmx theories/Bool/zerob.cmi +theories/Init/datatypes.cmo: theories/Init/datatypes.cmi +theories/Init/datatypes.cmx: theories/Init/datatypes.cmi +theories/Init/logic.cmo: theories/Init/logic.cmi +theories/Init/logic.cmx: theories/Init/logic.cmi +theories/Init/logic_Type.cmo: theories/Init/datatypes.cmi \ + theories/Init/logic_Type.cmi +theories/Init/logic_Type.cmx: theories/Init/datatypes.cmx \ + theories/Init/logic_Type.cmi +theories/Init/notations.cmo: theories/Init/notations.cmi +theories/Init/notations.cmx: theories/Init/notations.cmi +theories/Init/peano.cmo: theories/Init/datatypes.cmi theories/Init/peano.cmi +theories/Init/peano.cmx: theories/Init/datatypes.cmx theories/Init/peano.cmi +theories/Init/prelude.cmo: theories/Init/prelude.cmi +theories/Init/prelude.cmx: theories/Init/prelude.cmi +theories/Init/specif.cmo: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi +theories/Init/specif.cmx: theories/Init/datatypes.cmx \ + theories/Init/specif.cmi +theories/Init/wf.cmo: theories/Init/wf.cmi +theories/Init/wf.cmx: theories/Init/wf.cmi +theories/IntMap/adalloc.cmo: theories/IntMap/addec.cmi \ + theories/IntMap/addr.cmi theories/NArith/binPos.cmi \ + theories/Init/datatypes.cmi theories/IntMap/map.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi \ + theories/IntMap/adalloc.cmi +theories/IntMap/adalloc.cmx: theories/IntMap/addec.cmx \ + theories/IntMap/addr.cmx theories/NArith/binPos.cmx \ + theories/Init/datatypes.cmx theories/IntMap/map.cmx \ + theories/Init/specif.cmx theories/Bool/sumbool.cmx \ + theories/IntMap/adalloc.cmi +theories/IntMap/addec.cmo: theories/IntMap/addr.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi \ + theories/IntMap/addec.cmi +theories/IntMap/addec.cmx: theories/IntMap/addr.cmx \ + theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ + theories/Init/specif.cmx theories/Bool/sumbool.cmx \ + theories/IntMap/addec.cmi +theories/IntMap/addr.cmo: theories/NArith/binPos.cmi theories/Bool/bool.cmi \ + theories/Init/datatypes.cmi theories/Init/specif.cmi \ + theories/IntMap/addr.cmi +theories/IntMap/addr.cmx: theories/NArith/binPos.cmx theories/Bool/bool.cmx \ + theories/Init/datatypes.cmx theories/Init/specif.cmx \ + theories/IntMap/addr.cmi +theories/IntMap/adist.cmo: theories/IntMap/addr.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ + theories/IntMap/adist.cmi +theories/IntMap/adist.cmx: theories/IntMap/addr.cmx \ + theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ + theories/IntMap/adist.cmi +theories/IntMap/allmaps.cmo: theories/IntMap/allmaps.cmi +theories/IntMap/allmaps.cmx: theories/IntMap/allmaps.cmi +theories/IntMap/fset.cmo: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ + theories/Init/datatypes.cmi theories/IntMap/map.cmi \ + theories/Init/specif.cmi theories/IntMap/fset.cmi +theories/IntMap/fset.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \ + theories/Init/datatypes.cmx theories/IntMap/map.cmx \ + theories/Init/specif.cmx theories/IntMap/fset.cmi +theories/IntMap/lsort.cmo: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ + theories/NArith/binPos.cmi theories/Bool/bool.cmi \ + theories/Init/datatypes.cmi theories/Lists/list.cmi \ + theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi \ + theories/IntMap/lsort.cmi +theories/IntMap/lsort.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \ + theories/NArith/binPos.cmx theories/Bool/bool.cmx \ + theories/Init/datatypes.cmx theories/Lists/list.cmx \ + theories/IntMap/map.cmx theories/IntMap/mapiter.cmx \ + theories/Init/specif.cmx theories/Bool/sumbool.cmx \ + theories/IntMap/lsort.cmi +theories/IntMap/mapaxioms.cmo: theories/IntMap/mapaxioms.cmi +theories/IntMap/mapaxioms.cmx: theories/IntMap/mapaxioms.cmi +theories/IntMap/mapcanon.cmo: theories/IntMap/map.cmi \ + theories/Init/specif.cmi theories/IntMap/mapcanon.cmi +theories/IntMap/mapcanon.cmx: theories/IntMap/map.cmx \ + theories/Init/specif.cmx theories/IntMap/mapcanon.cmi +theories/IntMap/mapcard.cmo: theories/IntMap/addec.cmi \ + theories/IntMap/addr.cmi theories/Init/datatypes.cmi \ + theories/IntMap/map.cmi theories/Init/peano.cmi \ + theories/Arith/peano_dec.cmi theories/Arith/plus.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi \ + theories/IntMap/mapcard.cmi +theories/IntMap/mapcard.cmx: theories/IntMap/addec.cmx \ + theories/IntMap/addr.cmx theories/Init/datatypes.cmx \ + theories/IntMap/map.cmx theories/Init/peano.cmx \ + theories/Arith/peano_dec.cmx theories/Arith/plus.cmx \ + theories/Init/specif.cmx theories/Bool/sumbool.cmx \ + theories/IntMap/mapcard.cmi +theories/IntMap/mapc.cmo: theories/IntMap/mapc.cmi +theories/IntMap/mapc.cmx: theories/IntMap/mapc.cmi +theories/IntMap/mapfold.cmo: theories/IntMap/addr.cmi \ + theories/Init/datatypes.cmi theories/IntMap/fset.cmi \ + theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \ + theories/Init/specif.cmi theories/IntMap/mapfold.cmi +theories/IntMap/mapfold.cmx: theories/IntMap/addr.cmx \ + theories/Init/datatypes.cmx theories/IntMap/fset.cmx \ + theories/IntMap/map.cmx theories/IntMap/mapiter.cmx \ + theories/Init/specif.cmx theories/IntMap/mapfold.cmi +theories/IntMap/mapiter.cmo: theories/IntMap/addec.cmi \ + theories/IntMap/addr.cmi theories/Init/datatypes.cmi \ + theories/Lists/list.cmi theories/IntMap/map.cmi theories/Init/specif.cmi \ + theories/Bool/sumbool.cmi theories/IntMap/mapiter.cmi +theories/IntMap/mapiter.cmx: theories/IntMap/addec.cmx \ + theories/IntMap/addr.cmx theories/Init/datatypes.cmx \ + theories/Lists/list.cmx theories/IntMap/map.cmx theories/Init/specif.cmx \ + theories/Bool/sumbool.cmx theories/IntMap/mapiter.cmi +theories/IntMap/maplists.cmo: theories/IntMap/addec.cmi \ + theories/IntMap/addr.cmi theories/Init/datatypes.cmi \ + theories/IntMap/fset.cmi theories/Lists/list.cmi theories/IntMap/map.cmi \ + theories/IntMap/mapiter.cmi theories/Init/specif.cmi \ + theories/Bool/sumbool.cmi theories/IntMap/maplists.cmi +theories/IntMap/maplists.cmx: theories/IntMap/addec.cmx \ + theories/IntMap/addr.cmx theories/Init/datatypes.cmx \ + theories/IntMap/fset.cmx theories/Lists/list.cmx theories/IntMap/map.cmx \ + theories/IntMap/mapiter.cmx theories/Init/specif.cmx \ + theories/Bool/sumbool.cmx theories/IntMap/maplists.cmi +theories/IntMap/map.cmo: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ + theories/Init/peano.cmi theories/Init/specif.cmi theories/IntMap/map.cmi +theories/IntMap/map.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \ + theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ + theories/Init/peano.cmx theories/Init/specif.cmx theories/IntMap/map.cmi +theories/IntMap/mapsubset.cmo: theories/Bool/bool.cmi \ + theories/Init/datatypes.cmi theories/IntMap/fset.cmi \ + theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \ + theories/IntMap/mapsubset.cmi +theories/IntMap/mapsubset.cmx: theories/Bool/bool.cmx \ + theories/Init/datatypes.cmx theories/IntMap/fset.cmx \ + theories/IntMap/map.cmx theories/IntMap/mapiter.cmx \ + theories/IntMap/mapsubset.cmi +theories/Lists/list.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \ + theories/Lists/list.cmi +theories/Lists/list.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \ + theories/Lists/list.cmi +theories/Lists/listSet.cmo: theories/Init/datatypes.cmi \ + theories/Lists/list.cmi theories/Init/specif.cmi \ + theories/Lists/listSet.cmi +theories/Lists/listSet.cmx: theories/Init/datatypes.cmx \ + theories/Lists/list.cmx theories/Init/specif.cmx \ + theories/Lists/listSet.cmi +theories/Lists/monoList.cmo: theories/Init/datatypes.cmi \ + theories/Lists/monoList.cmi +theories/Lists/monoList.cmx: theories/Init/datatypes.cmx \ + theories/Lists/monoList.cmi +theories/Lists/streams.cmo: theories/Init/datatypes.cmi \ + theories/Lists/streams.cmi +theories/Lists/streams.cmx: theories/Init/datatypes.cmx \ + theories/Lists/streams.cmi +theories/Lists/theoryList.cmo: theories/Init/datatypes.cmi \ + theories/Lists/list.cmi theories/Init/specif.cmi \ + theories/Lists/theoryList.cmi +theories/Lists/theoryList.cmx: theories/Init/datatypes.cmx \ + theories/Lists/list.cmx theories/Init/specif.cmx \ + theories/Lists/theoryList.cmi +theories/Logic/berardi.cmo: theories/Logic/berardi.cmi +theories/Logic/berardi.cmx: theories/Logic/berardi.cmi +theories/Logic/choiceFacts.cmo: theories/Logic/choiceFacts.cmi +theories/Logic/choiceFacts.cmx: theories/Logic/choiceFacts.cmi +theories/Logic/classicalChoice.cmo: theories/Logic/classicalChoice.cmi +theories/Logic/classicalChoice.cmx: theories/Logic/classicalChoice.cmi +theories/Logic/classicalDescription.cmo: \ + theories/Logic/classicalDescription.cmi +theories/Logic/classicalDescription.cmx: \ + theories/Logic/classicalDescription.cmi +theories/Logic/classicalFacts.cmo: theories/Logic/classicalFacts.cmi +theories/Logic/classicalFacts.cmx: theories/Logic/classicalFacts.cmi +theories/Logic/classical.cmo: theories/Logic/classical.cmi +theories/Logic/classical.cmx: theories/Logic/classical.cmi +theories/Logic/classical_Pred_Set.cmo: theories/Logic/classical_Pred_Set.cmi +theories/Logic/classical_Pred_Set.cmx: theories/Logic/classical_Pred_Set.cmi +theories/Logic/classical_Pred_Type.cmo: \ + theories/Logic/classical_Pred_Type.cmi +theories/Logic/classical_Pred_Type.cmx: \ + theories/Logic/classical_Pred_Type.cmi +theories/Logic/classical_Prop.cmo: theories/Logic/classical_Prop.cmi +theories/Logic/classical_Prop.cmx: theories/Logic/classical_Prop.cmi +theories/Logic/classical_Type.cmo: theories/Logic/classical_Type.cmi +theories/Logic/classical_Type.cmx: theories/Logic/classical_Type.cmi +theories/Logic/decidable.cmo: theories/Logic/decidable.cmi +theories/Logic/decidable.cmx: theories/Logic/decidable.cmi +theories/Logic/diaconescu.cmo: theories/Logic/diaconescu.cmi +theories/Logic/diaconescu.cmx: theories/Logic/diaconescu.cmi +theories/Logic/eqdep_dec.cmo: theories/Logic/eqdep_dec.cmi +theories/Logic/eqdep_dec.cmx: theories/Logic/eqdep_dec.cmi +theories/Logic/eqdep.cmo: theories/Logic/eqdep.cmi +theories/Logic/eqdep.cmx: theories/Logic/eqdep.cmi +theories/Logic/hurkens.cmo: theories/Logic/hurkens.cmi +theories/Logic/hurkens.cmx: theories/Logic/hurkens.cmi +theories/Logic/jMeq.cmo: theories/Logic/jMeq.cmi +theories/Logic/jMeq.cmx: theories/Logic/jMeq.cmi +theories/Logic/proofIrrelevance.cmo: theories/Logic/proofIrrelevance.cmi +theories/Logic/proofIrrelevance.cmx: theories/Logic/proofIrrelevance.cmi +theories/Logic/relationalChoice.cmo: theories/Logic/relationalChoice.cmi +theories/Logic/relationalChoice.cmx: theories/Logic/relationalChoice.cmi +theories/NArith/binNat.cmo: theories/NArith/binPos.cmi \ + theories/Init/datatypes.cmi theories/NArith/binNat.cmi +theories/NArith/binNat.cmx: theories/NArith/binPos.cmx \ + theories/Init/datatypes.cmx theories/NArith/binNat.cmi +theories/NArith/binPos.cmo: theories/Init/datatypes.cmi \ + theories/Init/peano.cmi theories/NArith/binPos.cmi +theories/NArith/binPos.cmx: theories/Init/datatypes.cmx \ + theories/Init/peano.cmx theories/NArith/binPos.cmi +theories/NArith/nArith.cmo: theories/NArith/nArith.cmi +theories/NArith/nArith.cmx: theories/NArith/nArith.cmi +theories/NArith/pnat.cmo: theories/NArith/pnat.cmi +theories/NArith/pnat.cmx: theories/NArith/pnat.cmi +theories/Relations/newman.cmo: theories/Relations/newman.cmi +theories/Relations/newman.cmx: theories/Relations/newman.cmi +theories/Relations/operators_Properties.cmo: \ + theories/Relations/operators_Properties.cmi +theories/Relations/operators_Properties.cmx: \ + theories/Relations/operators_Properties.cmi +theories/Relations/relation_Definitions.cmo: \ + theories/Relations/relation_Definitions.cmi +theories/Relations/relation_Definitions.cmx: \ + theories/Relations/relation_Definitions.cmi +theories/Relations/relation_Operators.cmo: theories/Lists/list.cmi \ + theories/Init/specif.cmi theories/Relations/relation_Operators.cmi +theories/Relations/relation_Operators.cmx: theories/Lists/list.cmx \ + theories/Init/specif.cmx theories/Relations/relation_Operators.cmi +theories/Relations/relations.cmo: theories/Relations/relations.cmi +theories/Relations/relations.cmx: theories/Relations/relations.cmi +theories/Relations/rstar.cmo: theories/Relations/rstar.cmi +theories/Relations/rstar.cmx: theories/Relations/rstar.cmi +theories/Setoids/setoid.cmo: theories/Setoids/setoid.cmi +theories/Setoids/setoid.cmx: theories/Setoids/setoid.cmi +theories/Sets/classical_sets.cmo: theories/Sets/classical_sets.cmi +theories/Sets/classical_sets.cmx: theories/Sets/classical_sets.cmi +theories/Sets/constructive_sets.cmo: theories/Sets/constructive_sets.cmi +theories/Sets/constructive_sets.cmx: theories/Sets/constructive_sets.cmi +theories/Sets/cpo.cmo: theories/Sets/partial_Order.cmi theories/Sets/cpo.cmi +theories/Sets/cpo.cmx: theories/Sets/partial_Order.cmx theories/Sets/cpo.cmi +theories/Sets/ensembles.cmo: theories/Sets/ensembles.cmi +theories/Sets/ensembles.cmx: theories/Sets/ensembles.cmi +theories/Sets/finite_sets_facts.cmo: theories/Sets/finite_sets_facts.cmi +theories/Sets/finite_sets_facts.cmx: theories/Sets/finite_sets_facts.cmi +theories/Sets/finite_sets.cmo: theories/Sets/finite_sets.cmi +theories/Sets/finite_sets.cmx: theories/Sets/finite_sets.cmi +theories/Sets/image.cmo: theories/Sets/image.cmi +theories/Sets/image.cmx: theories/Sets/image.cmi +theories/Sets/infinite_sets.cmo: theories/Sets/infinite_sets.cmi +theories/Sets/infinite_sets.cmx: theories/Sets/infinite_sets.cmi +theories/Sets/integers.cmo: theories/Init/datatypes.cmi \ + theories/Sets/partial_Order.cmi theories/Sets/integers.cmi +theories/Sets/integers.cmx: theories/Init/datatypes.cmx \ + theories/Sets/partial_Order.cmx theories/Sets/integers.cmi +theories/Sets/multiset.cmo: theories/Init/datatypes.cmi \ + theories/Init/peano.cmi theories/Init/specif.cmi \ + theories/Sets/multiset.cmi +theories/Sets/multiset.cmx: theories/Init/datatypes.cmx \ + theories/Init/peano.cmx theories/Init/specif.cmx \ + theories/Sets/multiset.cmi +theories/Sets/partial_Order.cmo: theories/Sets/ensembles.cmi \ + theories/Sets/relations_1.cmi theories/Sets/partial_Order.cmi +theories/Sets/partial_Order.cmx: theories/Sets/ensembles.cmx \ + theories/Sets/relations_1.cmx theories/Sets/partial_Order.cmi +theories/Sets/permut.cmo: theories/Sets/permut.cmi +theories/Sets/permut.cmx: theories/Sets/permut.cmi +theories/Sets/powerset_Classical_facts.cmo: \ + theories/Sets/powerset_Classical_facts.cmi +theories/Sets/powerset_Classical_facts.cmx: \ + theories/Sets/powerset_Classical_facts.cmi +theories/Sets/powerset_facts.cmo: theories/Sets/powerset_facts.cmi +theories/Sets/powerset_facts.cmx: theories/Sets/powerset_facts.cmi +theories/Sets/powerset.cmo: theories/Sets/ensembles.cmi \ + theories/Sets/partial_Order.cmi theories/Sets/powerset.cmi +theories/Sets/powerset.cmx: theories/Sets/ensembles.cmx \ + theories/Sets/partial_Order.cmx theories/Sets/powerset.cmi +theories/Sets/relations_1_facts.cmo: theories/Sets/relations_1_facts.cmi +theories/Sets/relations_1_facts.cmx: theories/Sets/relations_1_facts.cmi +theories/Sets/relations_1.cmo: theories/Sets/relations_1.cmi +theories/Sets/relations_1.cmx: theories/Sets/relations_1.cmi +theories/Sets/relations_2_facts.cmo: theories/Sets/relations_2_facts.cmi +theories/Sets/relations_2_facts.cmx: theories/Sets/relations_2_facts.cmi +theories/Sets/relations_2.cmo: theories/Sets/relations_2.cmi +theories/Sets/relations_2.cmx: theories/Sets/relations_2.cmi +theories/Sets/relations_3_facts.cmo: theories/Sets/relations_3_facts.cmi +theories/Sets/relations_3_facts.cmx: theories/Sets/relations_3_facts.cmi +theories/Sets/relations_3.cmo: theories/Sets/relations_3.cmi +theories/Sets/relations_3.cmx: theories/Sets/relations_3.cmi +theories/Sets/uniset.cmo: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/Sets/uniset.cmi +theories/Sets/uniset.cmx: theories/Init/datatypes.cmx \ + theories/Init/specif.cmx theories/Sets/uniset.cmi +theories/Sorting/heap.cmo: theories/Init/datatypes.cmi \ + theories/Lists/list.cmi theories/Sets/multiset.cmi \ + theories/Init/peano.cmi theories/Sorting/sorting.cmi \ + theories/Init/specif.cmi theories/Sorting/heap.cmi +theories/Sorting/heap.cmx: theories/Init/datatypes.cmx \ + theories/Lists/list.cmx theories/Sets/multiset.cmx \ + theories/Init/peano.cmx theories/Sorting/sorting.cmx \ + theories/Init/specif.cmx theories/Sorting/heap.cmi +theories/Sorting/permutation.cmo: theories/Init/datatypes.cmi \ + theories/Lists/list.cmi theories/Sets/multiset.cmi \ + theories/Init/peano.cmi theories/Init/specif.cmi \ + theories/Sorting/permutation.cmi +theories/Sorting/permutation.cmx: theories/Init/datatypes.cmx \ + theories/Lists/list.cmx theories/Sets/multiset.cmx \ + theories/Init/peano.cmx theories/Init/specif.cmx \ + theories/Sorting/permutation.cmi +theories/Sorting/sorting.cmo: theories/Lists/list.cmi \ + theories/Init/specif.cmi theories/Sorting/sorting.cmi +theories/Sorting/sorting.cmx: theories/Lists/list.cmx \ + theories/Init/specif.cmx theories/Sorting/sorting.cmi +theories/Wellfounded/disjoint_Union.cmo: \ + theories/Wellfounded/disjoint_Union.cmi +theories/Wellfounded/disjoint_Union.cmx: \ + theories/Wellfounded/disjoint_Union.cmi +theories/Wellfounded/inclusion.cmo: theories/Wellfounded/inclusion.cmi +theories/Wellfounded/inclusion.cmx: theories/Wellfounded/inclusion.cmi +theories/Wellfounded/inverse_Image.cmo: \ + theories/Wellfounded/inverse_Image.cmi +theories/Wellfounded/inverse_Image.cmx: \ + theories/Wellfounded/inverse_Image.cmi +theories/Wellfounded/lexicographic_Exponentiation.cmo: \ + theories/Wellfounded/lexicographic_Exponentiation.cmi +theories/Wellfounded/lexicographic_Exponentiation.cmx: \ + theories/Wellfounded/lexicographic_Exponentiation.cmi +theories/Wellfounded/lexicographic_Product.cmo: \ + theories/Wellfounded/lexicographic_Product.cmi +theories/Wellfounded/lexicographic_Product.cmx: \ + theories/Wellfounded/lexicographic_Product.cmi +theories/Wellfounded/transitive_Closure.cmo: \ + theories/Wellfounded/transitive_Closure.cmi +theories/Wellfounded/transitive_Closure.cmx: \ + theories/Wellfounded/transitive_Closure.cmi +theories/Wellfounded/union.cmo: theories/Wellfounded/union.cmi +theories/Wellfounded/union.cmx: theories/Wellfounded/union.cmi +theories/Wellfounded/wellfounded.cmo: theories/Wellfounded/wellfounded.cmi +theories/Wellfounded/wellfounded.cmx: theories/Wellfounded/wellfounded.cmi +theories/Wellfounded/well_Ordering.cmo: theories/Init/specif.cmi \ + theories/Wellfounded/well_Ordering.cmi +theories/Wellfounded/well_Ordering.cmx: theories/Init/specif.cmx \ + theories/Wellfounded/well_Ordering.cmi +theories/ZArith/auxiliary.cmo: theories/ZArith/auxiliary.cmi +theories/ZArith/auxiliary.cmx: theories/ZArith/auxiliary.cmi +theories/ZArith/binInt.cmo: theories/NArith/binNat.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ + theories/ZArith/binInt.cmi +theories/ZArith/binInt.cmx: theories/NArith/binNat.cmx \ + theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ + theories/ZArith/binInt.cmi +theories/ZArith/wf_Z.cmo: theories/ZArith/binInt.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ + theories/Init/peano.cmi theories/Init/specif.cmi theories/ZArith/wf_Z.cmi +theories/ZArith/wf_Z.cmx: theories/ZArith/binInt.cmx \ + theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ + theories/Init/peano.cmx theories/Init/specif.cmx theories/ZArith/wf_Z.cmi +theories/ZArith/zabs.cmo: theories/ZArith/binInt.cmi theories/Init/specif.cmi \ + theories/Bool/sumbool.cmi theories/ZArith/zabs.cmi +theories/ZArith/zabs.cmx: theories/ZArith/binInt.cmx theories/Init/specif.cmx \ + theories/Bool/sumbool.cmx theories/ZArith/zabs.cmi +theories/ZArith/zArith_base.cmo: theories/ZArith/zArith_base.cmi +theories/ZArith/zArith_base.cmx: theories/ZArith/zArith_base.cmi +theories/ZArith/zArith_dec.cmo: theories/ZArith/binInt.cmi \ + theories/Init/datatypes.cmi theories/Init/specif.cmi \ + theories/Bool/sumbool.cmi theories/ZArith/zArith_dec.cmi +theories/ZArith/zArith_dec.cmx: theories/ZArith/binInt.cmx \ + theories/Init/datatypes.cmx theories/Init/specif.cmx \ + theories/Bool/sumbool.cmx theories/ZArith/zArith_dec.cmi +theories/ZArith/zArith.cmo: theories/ZArith/zArith.cmi +theories/ZArith/zArith.cmx: theories/ZArith/zArith.cmi +theories/ZArith/zbinary.cmo: theories/ZArith/binInt.cmi \ + theories/NArith/binPos.cmi theories/Bool/bvector.cmi \ + theories/Init/datatypes.cmi theories/ZArith/zeven.cmi \ + theories/ZArith/zbinary.cmi +theories/ZArith/zbinary.cmx: theories/ZArith/binInt.cmx \ + theories/NArith/binPos.cmx theories/Bool/bvector.cmx \ + theories/Init/datatypes.cmx theories/ZArith/zeven.cmx \ + theories/ZArith/zbinary.cmi +theories/ZArith/zbool.cmo: theories/ZArith/binInt.cmi \ + theories/Init/datatypes.cmi theories/Init/specif.cmi \ + theories/Bool/sumbool.cmi theories/ZArith/zArith_dec.cmi \ + theories/ZArith/zeven.cmi theories/ZArith/zbool.cmi +theories/ZArith/zbool.cmx: theories/ZArith/binInt.cmx \ + theories/Init/datatypes.cmx theories/Init/specif.cmx \ + theories/Bool/sumbool.cmx theories/ZArith/zArith_dec.cmx \ + theories/ZArith/zeven.cmx theories/ZArith/zbool.cmi +theories/ZArith/zcompare.cmo: theories/ZArith/zcompare.cmi +theories/ZArith/zcompare.cmx: theories/ZArith/zcompare.cmi +theories/ZArith/zcomplements.cmo: theories/ZArith/binInt.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ + theories/Lists/list.cmi theories/Init/specif.cmi theories/ZArith/wf_Z.cmi \ + theories/ZArith/zabs.cmi theories/ZArith/zcomplements.cmi +theories/ZArith/zcomplements.cmx: theories/ZArith/binInt.cmx \ + theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ + theories/Lists/list.cmx theories/Init/specif.cmx theories/ZArith/wf_Z.cmx \ + theories/ZArith/zabs.cmx theories/ZArith/zcomplements.cmi +theories/ZArith/zdiv.cmo: theories/ZArith/binInt.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/ZArith/zArith_dec.cmi \ + theories/ZArith/zbool.cmi theories/ZArith/zdiv.cmi +theories/ZArith/zdiv.cmx: theories/ZArith/binInt.cmx \ + theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ + theories/Init/specif.cmx theories/ZArith/zArith_dec.cmx \ + theories/ZArith/zbool.cmx theories/ZArith/zdiv.cmi +theories/ZArith/zeven.cmo: theories/ZArith/binInt.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/ZArith/zeven.cmi +theories/ZArith/zeven.cmx: theories/ZArith/binInt.cmx \ + theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ + theories/Init/specif.cmx theories/ZArith/zeven.cmi +theories/ZArith/zhints.cmo: theories/ZArith/zhints.cmi +theories/ZArith/zhints.cmx: theories/ZArith/zhints.cmi +theories/ZArith/zlogarithm.cmo: theories/ZArith/binInt.cmi \ + theories/NArith/binPos.cmi theories/ZArith/zlogarithm.cmi +theories/ZArith/zlogarithm.cmx: theories/ZArith/binInt.cmx \ + theories/NArith/binPos.cmx theories/ZArith/zlogarithm.cmi +theories/ZArith/zmin.cmo: theories/ZArith/binInt.cmi \ + theories/Init/datatypes.cmi theories/ZArith/zmin.cmi +theories/ZArith/zmin.cmx: theories/ZArith/binInt.cmx \ + theories/Init/datatypes.cmx theories/ZArith/zmin.cmi +theories/ZArith/zmisc.cmo: theories/ZArith/binInt.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ + theories/ZArith/zmisc.cmi +theories/ZArith/zmisc.cmx: theories/ZArith/binInt.cmx \ + theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ + theories/ZArith/zmisc.cmi +theories/ZArith/znat.cmo: theories/ZArith/znat.cmi +theories/ZArith/znat.cmx: theories/ZArith/znat.cmi +theories/ZArith/znumtheory.cmo: theories/ZArith/binInt.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/ZArith/wf_Z.cmi \ + theories/ZArith/zArith_dec.cmi theories/ZArith/zdiv.cmi \ + theories/ZArith/zorder.cmi theories/ZArith/znumtheory.cmi +theories/ZArith/znumtheory.cmx: theories/ZArith/binInt.cmx \ + theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ + theories/Init/specif.cmx theories/ZArith/wf_Z.cmx \ + theories/ZArith/zArith_dec.cmx theories/ZArith/zdiv.cmx \ + theories/ZArith/zorder.cmx theories/ZArith/znumtheory.cmi +theories/ZArith/zorder.cmo: theories/ZArith/binInt.cmi \ + theories/Init/datatypes.cmi theories/Init/specif.cmi \ + theories/ZArith/zorder.cmi +theories/ZArith/zorder.cmx: theories/ZArith/binInt.cmx \ + theories/Init/datatypes.cmx theories/Init/specif.cmx \ + theories/ZArith/zorder.cmi +theories/ZArith/zpower.cmo: theories/ZArith/binInt.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ + theories/ZArith/zmisc.cmi theories/ZArith/zpower.cmi +theories/ZArith/zpower.cmx: theories/ZArith/binInt.cmx \ + theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ + theories/ZArith/zmisc.cmx theories/ZArith/zpower.cmi +theories/ZArith/zsqrt.cmo: theories/ZArith/binInt.cmi \ + theories/NArith/binPos.cmi theories/Init/specif.cmi \ + theories/ZArith/zArith_dec.cmi theories/ZArith/zsqrt.cmi +theories/ZArith/zsqrt.cmx: theories/ZArith/binInt.cmx \ + theories/NArith/binPos.cmx theories/Init/specif.cmx \ + theories/ZArith/zArith_dec.cmx theories/ZArith/zsqrt.cmi +theories/ZArith/zwf.cmo: theories/ZArith/zwf.cmi +theories/ZArith/zwf.cmx: theories/ZArith/zwf.cmi +theories/Arith/bool_nat.cmi: theories/Arith/compare_dec.cmi \ + theories/Init/datatypes.cmi theories/Arith/peano_dec.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi +theories/Arith/compare_dec.cmi: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi +theories/Arith/compare.cmi: theories/Arith/compare_dec.cmi \ + theories/Init/datatypes.cmi theories/Init/specif.cmi +theories/Arith/div2.cmi: theories/Init/datatypes.cmi theories/Init/peano.cmi \ + theories/Init/specif.cmi +theories/Arith/eqNat.cmi: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi +theories/Arith/euclid.cmi: theories/Arith/compare_dec.cmi \ + theories/Init/datatypes.cmi theories/Init/specif.cmi +theories/Arith/even.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi +theories/Arith/factorial.cmi: theories/Init/datatypes.cmi \ + theories/Init/peano.cmi +theories/Arith/max.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi +theories/Arith/min.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi +theories/Arith/mult.cmi: theories/Init/datatypes.cmi theories/Arith/plus.cmi +theories/Arith/peano_dec.cmi: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi +theories/Arith/plus.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi +theories/Arith/wf_nat.cmi: theories/Init/datatypes.cmi +theories/Bool/boolEq.cmi: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi +theories/Bool/bool.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi +theories/Bool/bvector.cmi: theories/Bool/bool.cmi theories/Init/datatypes.cmi \ + theories/Init/peano.cmi +theories/Bool/decBool.cmi: theories/Init/specif.cmi +theories/Bool/ifProp.cmi: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi +theories/Bool/sumbool.cmi: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi +theories/Bool/zerob.cmi: theories/Init/datatypes.cmi +theories/Init/logic_Type.cmi: theories/Init/datatypes.cmi +theories/Init/peano.cmi: theories/Init/datatypes.cmi +theories/Init/specif.cmi: theories/Init/datatypes.cmi +theories/IntMap/adalloc.cmi: theories/IntMap/addec.cmi \ + theories/IntMap/addr.cmi theories/NArith/binPos.cmi \ + theories/Init/datatypes.cmi theories/IntMap/map.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi +theories/IntMap/addec.cmi: theories/IntMap/addr.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi +theories/IntMap/addr.cmi: theories/NArith/binPos.cmi theories/Bool/bool.cmi \ + theories/Init/datatypes.cmi theories/Init/specif.cmi +theories/IntMap/adist.cmi: theories/IntMap/addr.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi +theories/IntMap/fset.cmi: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ + theories/Init/datatypes.cmi theories/IntMap/map.cmi \ + theories/Init/specif.cmi +theories/IntMap/lsort.cmi: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ + theories/NArith/binPos.cmi theories/Bool/bool.cmi \ + theories/Init/datatypes.cmi theories/Lists/list.cmi \ + theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi +theories/IntMap/mapcanon.cmi: theories/IntMap/map.cmi \ + theories/Init/specif.cmi +theories/IntMap/mapcard.cmi: theories/IntMap/addec.cmi \ + theories/IntMap/addr.cmi theories/Init/datatypes.cmi \ + theories/IntMap/map.cmi theories/Init/peano.cmi \ + theories/Arith/peano_dec.cmi theories/Arith/plus.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi +theories/IntMap/mapfold.cmi: theories/IntMap/addr.cmi \ + theories/Init/datatypes.cmi theories/IntMap/fset.cmi \ + theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \ + theories/Init/specif.cmi +theories/IntMap/mapiter.cmi: theories/IntMap/addec.cmi \ + theories/IntMap/addr.cmi theories/Init/datatypes.cmi \ + theories/Lists/list.cmi theories/IntMap/map.cmi theories/Init/specif.cmi \ + theories/Bool/sumbool.cmi +theories/IntMap/maplists.cmi: theories/IntMap/addec.cmi \ + theories/IntMap/addr.cmi theories/Init/datatypes.cmi \ + theories/IntMap/fset.cmi theories/Lists/list.cmi theories/IntMap/map.cmi \ + theories/IntMap/mapiter.cmi theories/Init/specif.cmi \ + theories/Bool/sumbool.cmi +theories/IntMap/map.cmi: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ + theories/Init/peano.cmi theories/Init/specif.cmi +theories/IntMap/mapsubset.cmi: theories/Bool/bool.cmi \ + theories/Init/datatypes.cmi theories/IntMap/fset.cmi \ + theories/IntMap/map.cmi theories/IntMap/mapiter.cmi +theories/Lists/list.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi +theories/Lists/listSet.cmi: theories/Init/datatypes.cmi \ + theories/Lists/list.cmi theories/Init/specif.cmi +theories/Lists/monoList.cmi: theories/Init/datatypes.cmi +theories/Lists/streams.cmi: theories/Init/datatypes.cmi +theories/Lists/theoryList.cmi: theories/Init/datatypes.cmi \ + theories/Lists/list.cmi theories/Init/specif.cmi +theories/NArith/binNat.cmi: theories/NArith/binPos.cmi \ + theories/Init/datatypes.cmi +theories/NArith/binPos.cmi: theories/Init/datatypes.cmi \ + theories/Init/peano.cmi +theories/Relations/relation_Operators.cmi: theories/Lists/list.cmi \ + theories/Init/specif.cmi +theories/Sets/cpo.cmi: theories/Sets/partial_Order.cmi +theories/Sets/integers.cmi: theories/Init/datatypes.cmi \ + theories/Sets/partial_Order.cmi +theories/Sets/multiset.cmi: theories/Init/datatypes.cmi \ + theories/Init/peano.cmi theories/Init/specif.cmi +theories/Sets/partial_Order.cmi: theories/Sets/ensembles.cmi \ + theories/Sets/relations_1.cmi +theories/Sets/powerset.cmi: theories/Sets/ensembles.cmi \ + theories/Sets/partial_Order.cmi +theories/Sets/uniset.cmi: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi +theories/Sorting/heap.cmi: theories/Init/datatypes.cmi \ + theories/Lists/list.cmi theories/Sets/multiset.cmi \ + theories/Init/peano.cmi theories/Sorting/sorting.cmi \ + theories/Init/specif.cmi +theories/Sorting/permutation.cmi: theories/Init/datatypes.cmi \ + theories/Lists/list.cmi theories/Sets/multiset.cmi \ + theories/Init/peano.cmi theories/Init/specif.cmi +theories/Sorting/sorting.cmi: theories/Lists/list.cmi \ + theories/Init/specif.cmi +theories/Wellfounded/well_Ordering.cmi: theories/Init/specif.cmi +theories/ZArith/binInt.cmi: theories/NArith/binNat.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi +theories/ZArith/wf_Z.cmi: theories/ZArith/binInt.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ + theories/Init/peano.cmi theories/Init/specif.cmi +theories/ZArith/zabs.cmi: theories/ZArith/binInt.cmi theories/Init/specif.cmi \ + theories/Bool/sumbool.cmi +theories/ZArith/zArith_dec.cmi: theories/ZArith/binInt.cmi \ + theories/Init/datatypes.cmi theories/Init/specif.cmi \ + theories/Bool/sumbool.cmi +theories/ZArith/zbinary.cmi: theories/ZArith/binInt.cmi \ + theories/NArith/binPos.cmi theories/Bool/bvector.cmi \ + theories/Init/datatypes.cmi theories/ZArith/zeven.cmi +theories/ZArith/zbool.cmi: theories/ZArith/binInt.cmi \ + theories/Init/datatypes.cmi theories/Init/specif.cmi \ + theories/Bool/sumbool.cmi theories/ZArith/zArith_dec.cmi \ + theories/ZArith/zeven.cmi +theories/ZArith/zcomplements.cmi: theories/ZArith/binInt.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ + theories/Lists/list.cmi theories/Init/specif.cmi theories/ZArith/wf_Z.cmi \ + theories/ZArith/zabs.cmi +theories/ZArith/zdiv.cmi: theories/ZArith/binInt.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/ZArith/zArith_dec.cmi \ + theories/ZArith/zbool.cmi +theories/ZArith/zeven.cmi: theories/ZArith/binInt.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ + theories/Init/specif.cmi +theories/ZArith/zlogarithm.cmi: theories/ZArith/binInt.cmi \ + theories/NArith/binPos.cmi +theories/ZArith/zmin.cmi: theories/ZArith/binInt.cmi \ + theories/Init/datatypes.cmi +theories/ZArith/zmisc.cmi: theories/ZArith/binInt.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi +theories/ZArith/znumtheory.cmi: theories/ZArith/binInt.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/ZArith/wf_Z.cmi \ + theories/ZArith/zArith_dec.cmi theories/ZArith/zdiv.cmi \ + theories/ZArith/zorder.cmi +theories/ZArith/zorder.cmi: theories/ZArith/binInt.cmi \ + theories/Init/datatypes.cmi theories/Init/specif.cmi +theories/ZArith/zpower.cmi: theories/ZArith/binInt.cmi \ + theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ + theories/ZArith/zmisc.cmi +theories/ZArith/zsqrt.cmi: theories/ZArith/binInt.cmi \ + theories/NArith/binPos.cmi theories/Init/specif.cmi \ + theories/ZArith/zArith_dec.cmi diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile new file mode 100644 index 00000000..c9bb5623 --- /dev/null +++ b/contrib/extraction/test/Makefile @@ -0,0 +1,109 @@ +# +# General variables +# + +TOPDIR=../../.. + +# Files with axioms to be realized: can't be extracted directly + +AXIOMSVO:= \ +theories/Reals/% \ +theories/Num/% + +DIRS:= $(shell (cd $(TOPDIR);find theories -type d ! -name CVS)) + +INCL:= $(patsubst %,-I %,$(DIRS)) + +VO:= $(shell (cd $(TOPDIR);find theories -name \*.vo)) + +VO:= $(filter-out $(AXIOMSVO),$(VO)) + +ML:= $(shell test -x v2ml && ./v2ml $(VO)) + +MLI:= $(patsubst %.ml,%.mli,$(ML)) + +CMO:= $(patsubst %.ml,%.cmo,$(ML)) + +OSTDLIB:=$(shell (ocamlc -where)) + +# +# General rules +# + +all: v2ml ml $(MLI) $(CMO) + +ml: $(ML) + +depend: $(ML) + rm -f .depend; ocamldep $(INCL) theories/*/*.ml theories/*/*.mli > .depend + +tree: + mkdir -p $(DIRS) + cp $(OSTDLIB)/pervasives.cmi $(OSTDLIB)/obj.cmi $(OSTDLIB)/lazy.cmi theories + +#%.mli:%.ml +# ./make_mli $< > $@ + +%.cmi:%.mli + ocamlc -c $(INCL) -nostdlib $< + +%.cmo:%.ml + ocamlc -c $(INCL) -nostdlib $< + +$(ML): ml2v + ./extract $@ + +clean: + rm -f theories/*/*.ml* theories/*/*.cm* + + +# +# Utilities +# + +open: + find theories -name "*".ml -exec ./qualify2open \{\} \; + +undo_open: + find theories -name "*".ml -exec mv \{\}.orig \{\} \; + +ml2v: ml2v.ml + ocamlopt -o $@ $< + +v2ml: v2ml.ml + ocamlopt -o $@ $< + $(MAKE) + +# +# Extraction of Reals +# + + +REALSAXIOMSVO:=theories/Reals/Rsyntax.vo + +REALSALLVO:=$(shell cd $(TOPDIR); ls -tr theories/Reals/*.vo) +REALSVO:=$(filter-out $(REALSAXIOMSVO),$(REALSALLVO)) +REALSML:=$(shell test -x v2ml && ./v2ml $(REALSVO)) +REALSCMO:= $(patsubst %.ml,%.cmo,$(REALSML)) + +reals: all realsml theories/Reals/addReals.cmo $(REALSCMO) + +realsml: $(REALSML) + +theories/Reals/addReals.ml: + cp -f addReals theories/Reals/addReals.ml + +$(REALSML): + ./extract $@ + + +# +# The End +# + +.PHONY: all tree clean reals realsml depend + +include .depend + + + diff --git a/contrib/extraction/test/Makefile.haskell b/contrib/extraction/test/Makefile.haskell new file mode 100644 index 00000000..6e1e15d1 --- /dev/null +++ b/contrib/extraction/test/Makefile.haskell @@ -0,0 +1,416 @@ +# +# General variables +# + +TOPDIR=../../.. + +# Files with axioms to be realized: can't be extracted directly + +AXIOMSVO:= \ +theories/Init/Prelude.vo \ +theories/Reals/% \ +theories/Num/% + +DIRS:= $(shell (cd $(TOPDIR);find theories -type d ! -name CVS)) + +INCL:= $(patsubst %,-i%,$(DIRS)) + +VO:= $(shell (cd $(TOPDIR);find theories -name \*.vo)) + +VO:= $(filter-out $(AXIOMSVO),$(VO)) + +HS:= $(shell test -x v2hs && ./v2hs $(VO)) + +O:= $(patsubst %.hs,%.o,$(HS)) + +# +# General rules +# + +all: v2hs hs $(O) + +hs: $(HS) + +tree: + mkdir -p $(DIRS) + +%.o:%.hs + ghc $(INCL) -c $< + +$(HS): hs2v + ./extract.haskell $@ + +clean: + rm -f theories/*/*.h* theories/*/*.o + + +# +# Utilities +# + +hs2v: hs2v.ml + ocamlc -o $@ $< + +v2hs: v2hs.ml + ocamlc -o $@ $< + $(MAKE) -f Makefile.haskell + + +# +# The End +# + +.PHONY: all tree clean depend + +# DO NOT DELETE: Beginning of Haskell dependencies +theories/Arith/Between.o : theories/Arith/Between.hs +theories/Arith/Bool_nat.o : theories/Arith/Bool_nat.hs +theories/Arith/Bool_nat.o : theories/Bool/Sumbool.o +theories/Arith/Bool_nat.o : theories/Init/Specif.o +theories/Arith/Bool_nat.o : theories/Arith/Peano_dec.o +theories/Arith/Bool_nat.o : theories/Init/Datatypes.o +theories/Arith/Bool_nat.o : theories/Arith/Compare_dec.o +theories/Arith/Compare_dec.o : theories/Arith/Compare_dec.hs +theories/Arith/Compare_dec.o : theories/Init/Specif.o +theories/Arith/Compare_dec.o : theories/Init/Logic.o +theories/Arith/Compare_dec.o : theories/Init/Datatypes.o +theories/Arith/Compare.o : theories/Arith/Compare.hs +theories/Arith/Compare.o : theories/Init/Specif.o +theories/Arith/Compare.o : theories/Init/Datatypes.o +theories/Arith/Compare.o : theories/Arith/Compare_dec.o +theories/Arith/Div2.o : theories/Arith/Div2.hs +theories/Arith/Div2.o : theories/Init/Specif.o +theories/Arith/Div2.o : theories/Init/Peano.o +theories/Arith/Div2.o : theories/Init/Datatypes.o +theories/Arith/EqNat.o : theories/Arith/EqNat.hs +theories/Arith/EqNat.o : theories/Init/Specif.o +theories/Arith/EqNat.o : theories/Init/Datatypes.o +theories/Arith/Euclid.o : theories/Arith/Euclid.hs +theories/Arith/Euclid.o : theories/Arith/Wf_nat.o +theories/Arith/Euclid.o : theories/Init/Specif.o +theories/Arith/Euclid.o : theories/Arith/Minus.o +theories/Arith/Euclid.o : theories/Init/Datatypes.o +theories/Arith/Euclid.o : theories/Arith/Compare_dec.o +theories/Arith/Even.o : theories/Arith/Even.hs +theories/Arith/Even.o : theories/Init/Specif.o +theories/Arith/Even.o : theories/Init/Datatypes.o +theories/Arith/Gt.o : theories/Arith/Gt.hs +theories/Arith/Le.o : theories/Arith/Le.hs +theories/Arith/Lt.o : theories/Arith/Lt.hs +theories/Arith/Max.o : theories/Arith/Max.hs +theories/Arith/Max.o : theories/Init/Specif.o +theories/Arith/Max.o : theories/Init/Logic.o +theories/Arith/Max.o : theories/Init/Datatypes.o +theories/Arith/Min.o : theories/Arith/Min.hs +theories/Arith/Min.o : theories/Init/Specif.o +theories/Arith/Min.o : theories/Init/Logic.o +theories/Arith/Min.o : theories/Init/Datatypes.o +theories/Arith/Minus.o : theories/Arith/Minus.hs +theories/Arith/Minus.o : theories/Init/Datatypes.o +theories/Arith/Mult.o : theories/Arith/Mult.hs +theories/Arith/Mult.o : theories/Arith/Plus.o +theories/Arith/Mult.o : theories/Init/Datatypes.o +theories/Arith/Peano_dec.o : theories/Arith/Peano_dec.hs +theories/Arith/Peano_dec.o : theories/Init/Specif.o +theories/Arith/Peano_dec.o : theories/Init/Datatypes.o +theories/Arith/Plus.o : theories/Arith/Plus.hs +theories/Arith/Plus.o : theories/Init/Specif.o +theories/Arith/Plus.o : theories/Init/Logic.o +theories/Arith/Plus.o : theories/Init/Datatypes.o +theories/Arith/Wf_nat.o : theories/Arith/Wf_nat.hs +theories/Arith/Wf_nat.o : theories/Init/Wf.o +theories/Arith/Wf_nat.o : theories/Init/Logic.o +theories/Arith/Wf_nat.o : theories/Init/Datatypes.o +theories/Bool/BoolEq.o : theories/Bool/BoolEq.hs +theories/Bool/BoolEq.o : theories/Init/Specif.o +theories/Bool/BoolEq.o : theories/Init/Datatypes.o +theories/Bool/Bool.o : theories/Bool/Bool.hs +theories/Bool/Bool.o : theories/Init/Specif.o +theories/Bool/Bool.o : theories/Init/Datatypes.o +theories/Bool/DecBool.o : theories/Bool/DecBool.hs +theories/Bool/DecBool.o : theories/Init/Specif.o +theories/Bool/IfProp.o : theories/Bool/IfProp.hs +theories/Bool/IfProp.o : theories/Init/Specif.o +theories/Bool/IfProp.o : theories/Init/Datatypes.o +theories/Bool/Sumbool.o : theories/Bool/Sumbool.hs +theories/Bool/Sumbool.o : theories/Init/Specif.o +theories/Bool/Sumbool.o : theories/Init/Datatypes.o +theories/Bool/Zerob.o : theories/Bool/Zerob.hs +theories/Bool/Zerob.o : theories/Init/Datatypes.o +theories/Init/Datatypes.o : theories/Init/Datatypes.hs +theories/Init/DatatypesSyntax.o : theories/Init/DatatypesSyntax.hs +theories/Init/Logic.o : theories/Init/Logic.hs +theories/Init/LogicSyntax.o : theories/Init/LogicSyntax.hs +theories/Init/Logic_Type.o : theories/Init/Logic_Type.hs +theories/Init/Logic_TypeSyntax.o : theories/Init/Logic_TypeSyntax.hs +theories/Init/Peano.o : theories/Init/Peano.hs +theories/Init/Peano.o : theories/Init/Datatypes.o +theories/Init/Specif.o : theories/Init/Specif.hs +theories/Init/Specif.o : theories/Init/Logic.o +theories/Init/Specif.o : theories/Init/Datatypes.o +theories/Init/SpecifSyntax.o : theories/Init/SpecifSyntax.hs +theories/Init/Wf.o : theories/Init/Wf.hs +theories/IntMap/Adalloc.o : theories/IntMap/Adalloc.hs +theories/IntMap/Adalloc.o : theories/ZArith/Fast_integer.o +theories/IntMap/Adalloc.o : theories/Bool/Sumbool.o +theories/IntMap/Adalloc.o : theories/Init/Specif.o +theories/IntMap/Adalloc.o : theories/IntMap/Map.o +theories/IntMap/Adalloc.o : theories/Init/Logic.o +theories/IntMap/Adalloc.o : theories/Init/Datatypes.o +theories/IntMap/Adalloc.o : theories/IntMap/Addr.o +theories/IntMap/Adalloc.o : theories/IntMap/Addec.o +theories/IntMap/Addec.o : theories/IntMap/Addec.hs +theories/IntMap/Addec.o : theories/ZArith/Fast_integer.o +theories/IntMap/Addec.o : theories/Bool/Sumbool.o +theories/IntMap/Addec.o : theories/Init/Specif.o +theories/IntMap/Addec.o : theories/Init/Datatypes.o +theories/IntMap/Addec.o : theories/IntMap/Addr.o +theories/IntMap/Addr.o : theories/IntMap/Addr.hs +theories/IntMap/Addr.o : theories/ZArith/Fast_integer.o +theories/IntMap/Addr.o : theories/Init/Specif.o +theories/IntMap/Addr.o : theories/Init/Datatypes.o +theories/IntMap/Addr.o : theories/Bool/Bool.o +theories/IntMap/Adist.o : theories/IntMap/Adist.hs +theories/IntMap/Adist.o : theories/ZArith/Fast_integer.o +theories/IntMap/Adist.o : theories/Arith/Min.o +theories/IntMap/Adist.o : theories/Init/Datatypes.o +theories/IntMap/Adist.o : theories/IntMap/Addr.o +theories/IntMap/Allmaps.o : theories/IntMap/Allmaps.hs +theories/IntMap/Fset.o : theories/IntMap/Fset.hs +theories/IntMap/Fset.o : theories/Init/Specif.o +theories/IntMap/Fset.o : theories/IntMap/Map.o +theories/IntMap/Fset.o : theories/Init/Logic.o +theories/IntMap/Fset.o : theories/Init/Datatypes.o +theories/IntMap/Fset.o : theories/IntMap/Addr.o +theories/IntMap/Fset.o : theories/IntMap/Addec.o +theories/IntMap/Lsort.o : theories/IntMap/Lsort.hs +theories/IntMap/Lsort.o : theories/ZArith/Fast_integer.o +theories/IntMap/Lsort.o : theories/Bool/Sumbool.o +theories/IntMap/Lsort.o : theories/Init/Specif.o +theories/IntMap/Lsort.o : theories/Lists/PolyList.o +theories/IntMap/Lsort.o : theories/IntMap/Mapiter.o +theories/IntMap/Lsort.o : theories/IntMap/Map.o +theories/IntMap/Lsort.o : theories/Init/Logic.o +theories/IntMap/Lsort.o : theories/Init/Datatypes.o +theories/IntMap/Lsort.o : theories/Bool/Bool.o +theories/IntMap/Lsort.o : theories/IntMap/Addr.o +theories/IntMap/Lsort.o : theories/IntMap/Addec.o +theories/IntMap/Mapaxioms.o : theories/IntMap/Mapaxioms.hs +theories/IntMap/Mapcanon.o : theories/IntMap/Mapcanon.hs +theories/IntMap/Mapcanon.o : theories/Init/Specif.o +theories/IntMap/Mapcanon.o : theories/IntMap/Map.o +theories/IntMap/Mapcard.o : theories/IntMap/Mapcard.hs +theories/IntMap/Mapcard.o : theories/Bool/Sumbool.o +theories/IntMap/Mapcard.o : theories/Init/Specif.o +theories/IntMap/Mapcard.o : theories/Arith/Plus.o +theories/IntMap/Mapcard.o : theories/Arith/Peano_dec.o +theories/IntMap/Mapcard.o : theories/Init/Peano.o +theories/IntMap/Mapcard.o : theories/IntMap/Map.o +theories/IntMap/Mapcard.o : theories/Init/Logic.o +theories/IntMap/Mapcard.o : theories/Init/Datatypes.o +theories/IntMap/Mapcard.o : theories/IntMap/Addr.o +theories/IntMap/Mapcard.o : theories/IntMap/Addec.o +theories/IntMap/Mapc.o : theories/IntMap/Mapc.hs +theories/IntMap/Mapfold.o : theories/IntMap/Mapfold.hs +theories/IntMap/Mapfold.o : theories/Init/Specif.o +theories/IntMap/Mapfold.o : theories/IntMap/Mapiter.o +theories/IntMap/Mapfold.o : theories/IntMap/Map.o +theories/IntMap/Mapfold.o : theories/Init/Logic.o +theories/IntMap/Mapfold.o : theories/IntMap/Fset.o +theories/IntMap/Mapfold.o : theories/Init/Datatypes.o +theories/IntMap/Mapfold.o : theories/IntMap/Addr.o +theories/IntMap/Map.o : theories/IntMap/Map.hs +theories/IntMap/Map.o : theories/ZArith/Fast_integer.o +theories/IntMap/Map.o : theories/Init/Specif.o +theories/IntMap/Map.o : theories/Init/Peano.o +theories/IntMap/Map.o : theories/Init/Datatypes.o +theories/IntMap/Map.o : theories/IntMap/Addr.o +theories/IntMap/Map.o : theories/IntMap/Addec.o +theories/IntMap/Mapiter.o : theories/IntMap/Mapiter.hs +theories/IntMap/Mapiter.o : theories/Bool/Sumbool.o +theories/IntMap/Mapiter.o : theories/Init/Specif.o +theories/IntMap/Mapiter.o : theories/Lists/PolyList.o +theories/IntMap/Mapiter.o : theories/IntMap/Map.o +theories/IntMap/Mapiter.o : theories/Init/Logic.o +theories/IntMap/Mapiter.o : theories/Init/Datatypes.o +theories/IntMap/Mapiter.o : theories/IntMap/Addr.o +theories/IntMap/Mapiter.o : theories/IntMap/Addec.o +theories/IntMap/Maplists.o : theories/IntMap/Maplists.hs +theories/IntMap/Maplists.o : theories/Bool/Sumbool.o +theories/IntMap/Maplists.o : theories/Init/Specif.o +theories/IntMap/Maplists.o : theories/Lists/PolyList.o +theories/IntMap/Maplists.o : theories/IntMap/Mapiter.o +theories/IntMap/Maplists.o : theories/IntMap/Map.o +theories/IntMap/Maplists.o : theories/Init/Logic.o +theories/IntMap/Maplists.o : theories/IntMap/Fset.o +theories/IntMap/Maplists.o : theories/Init/Datatypes.o +theories/IntMap/Maplists.o : theories/Bool/Bool.o +theories/IntMap/Maplists.o : theories/IntMap/Addr.o +theories/IntMap/Maplists.o : theories/IntMap/Addec.o +theories/IntMap/Mapsubset.o : theories/IntMap/Mapsubset.hs +theories/IntMap/Mapsubset.o : theories/IntMap/Mapiter.o +theories/IntMap/Mapsubset.o : theories/IntMap/Map.o +theories/IntMap/Mapsubset.o : theories/IntMap/Fset.o +theories/IntMap/Mapsubset.o : theories/Init/Datatypes.o +theories/IntMap/Mapsubset.o : theories/Bool/Bool.o +theories/Lists/ListSet.o : theories/Lists/ListSet.hs +theories/Lists/ListSet.o : theories/Init/Specif.o +theories/Lists/ListSet.o : theories/Lists/PolyList.o +theories/Lists/ListSet.o : theories/Init/Logic.o +theories/Lists/ListSet.o : theories/Init/Datatypes.o +theories/Lists/PolyList.o : theories/Lists/PolyList.hs +theories/Lists/PolyList.o : theories/Init/Specif.o +theories/Lists/PolyList.o : theories/Init/Datatypes.o +theories/Lists/PolyListSyntax.o : theories/Lists/PolyListSyntax.hs +theories/Lists/Streams.o : theories/Lists/Streams.hs +theories/Lists/Streams.o : theories/Init/Datatypes.o +theories/Lists/TheoryList.o : theories/Lists/TheoryList.hs +theories/Lists/TheoryList.o : theories/Init/Specif.o +theories/Lists/TheoryList.o : theories/Lists/PolyList.o +theories/Lists/TheoryList.o : theories/Bool/DecBool.o +theories/Lists/TheoryList.o : theories/Init/Datatypes.o +theories/Logic/Berardi.o : theories/Logic/Berardi.hs +theories/Logic/ClassicalFacts.o : theories/Logic/ClassicalFacts.hs +theories/Logic/Classical.o : theories/Logic/Classical.hs +theories/Logic/Classical_Pred_Set.o : theories/Logic/Classical_Pred_Set.hs +theories/Logic/Classical_Pred_Type.o : theories/Logic/Classical_Pred_Type.hs +theories/Logic/Classical_Prop.o : theories/Logic/Classical_Prop.hs +theories/Logic/Classical_Type.o : theories/Logic/Classical_Type.hs +theories/Logic/Decidable.o : theories/Logic/Decidable.hs +theories/Logic/Eqdep_dec.o : theories/Logic/Eqdep_dec.hs +theories/Logic/Eqdep.o : theories/Logic/Eqdep.hs +theories/Logic/Hurkens.o : theories/Logic/Hurkens.hs +theories/Logic/JMeq.o : theories/Logic/JMeq.hs +theories/Logic/ProofIrrelevance.o : theories/Logic/ProofIrrelevance.hs +theories/Relations/Newman.o : theories/Relations/Newman.hs +theories/Relations/Operators_Properties.o : theories/Relations/Operators_Properties.hs +theories/Relations/Relation_Definitions.o : theories/Relations/Relation_Definitions.hs +theories/Relations/Relation_Operators.o : theories/Relations/Relation_Operators.hs +theories/Relations/Relation_Operators.o : theories/Init/Specif.o +theories/Relations/Relation_Operators.o : theories/Lists/PolyList.o +theories/Relations/Relations.o : theories/Relations/Relations.hs +theories/Relations/Rstar.o : theories/Relations/Rstar.hs +theories/Setoids/Setoid.o : theories/Setoids/Setoid.hs +theories/Sets/Classical_sets.o : theories/Sets/Classical_sets.hs +theories/Sets/Constructive_sets.o : theories/Sets/Constructive_sets.hs +theories/Sets/Cpo.o : theories/Sets/Cpo.hs +theories/Sets/Cpo.o : theories/Sets/Partial_Order.o +theories/Sets/Ensembles.o : theories/Sets/Ensembles.hs +theories/Sets/Finite_sets_facts.o : theories/Sets/Finite_sets_facts.hs +theories/Sets/Finite_sets.o : theories/Sets/Finite_sets.hs +theories/Sets/Image.o : theories/Sets/Image.hs +theories/Sets/Infinite_sets.o : theories/Sets/Infinite_sets.hs +theories/Sets/Integers.o : theories/Sets/Integers.hs +theories/Sets/Integers.o : theories/Sets/Partial_Order.o +theories/Sets/Integers.o : theories/Init/Datatypes.o +theories/Sets/Multiset.o : theories/Sets/Multiset.hs +theories/Sets/Multiset.o : theories/Init/Specif.o +theories/Sets/Multiset.o : theories/Init/Peano.o +theories/Sets/Multiset.o : theories/Init/Datatypes.o +theories/Sets/Partial_Order.o : theories/Sets/Partial_Order.hs +theories/Sets/Permut.o : theories/Sets/Permut.hs +theories/Sets/Powerset_Classical_facts.o : theories/Sets/Powerset_Classical_facts.hs +theories/Sets/Powerset_facts.o : theories/Sets/Powerset_facts.hs +theories/Sets/Powerset.o : theories/Sets/Powerset.hs +theories/Sets/Powerset.o : theories/Sets/Partial_Order.o +theories/Sets/Relations_1_facts.o : theories/Sets/Relations_1_facts.hs +theories/Sets/Relations_1.o : theories/Sets/Relations_1.hs +theories/Sets/Relations_2_facts.o : theories/Sets/Relations_2_facts.hs +theories/Sets/Relations_2.o : theories/Sets/Relations_2.hs +theories/Sets/Relations_3_facts.o : theories/Sets/Relations_3_facts.hs +theories/Sets/Relations_3.o : theories/Sets/Relations_3.hs +theories/Sets/Uniset.o : theories/Sets/Uniset.hs +theories/Sets/Uniset.o : theories/Init/Specif.o +theories/Sets/Uniset.o : theories/Init/Datatypes.o +theories/Sets/Uniset.o : theories/Bool/Bool.o +theories/Sorting/Heap.o : theories/Sorting/Heap.hs +theories/Sorting/Heap.o : theories/Init/Specif.o +theories/Sorting/Heap.o : theories/Sorting/Sorting.o +theories/Sorting/Heap.o : theories/Lists/PolyList.o +theories/Sorting/Heap.o : theories/Sets/Multiset.o +theories/Sorting/Heap.o : theories/Init/Logic.o +theories/Sorting/Permutation.o : theories/Sorting/Permutation.hs +theories/Sorting/Permutation.o : theories/Init/Specif.o +theories/Sorting/Permutation.o : theories/Lists/PolyList.o +theories/Sorting/Permutation.o : theories/Sets/Multiset.o +theories/Sorting/Sorting.o : theories/Sorting/Sorting.hs +theories/Sorting/Sorting.o : theories/Init/Specif.o +theories/Sorting/Sorting.o : theories/Lists/PolyList.o +theories/Sorting/Sorting.o : theories/Init/Logic.o +theories/Wellfounded/Disjoint_Union.o : theories/Wellfounded/Disjoint_Union.hs +theories/Wellfounded/Inclusion.o : theories/Wellfounded/Inclusion.hs +theories/Wellfounded/Inverse_Image.o : theories/Wellfounded/Inverse_Image.hs +theories/Wellfounded/Lexicographic_Exponentiation.o : theories/Wellfounded/Lexicographic_Exponentiation.hs +theories/Wellfounded/Lexicographic_Product.o : theories/Wellfounded/Lexicographic_Product.hs +theories/Wellfounded/Transitive_Closure.o : theories/Wellfounded/Transitive_Closure.hs +theories/Wellfounded/Union.o : theories/Wellfounded/Union.hs +theories/Wellfounded/Wellfounded.o : theories/Wellfounded/Wellfounded.hs +theories/Wellfounded/Well_Ordering.o : theories/Wellfounded/Well_Ordering.hs +theories/Wellfounded/Well_Ordering.o : theories/Init/Wf.o +theories/Wellfounded/Well_Ordering.o : theories/Init/Specif.o +theories/ZArith/Auxiliary.o : theories/ZArith/Auxiliary.hs +theories/ZArith/Fast_integer.o : theories/ZArith/Fast_integer.hs +theories/ZArith/Fast_integer.o : theories/Init/Peano.o +theories/ZArith/Fast_integer.o : theories/Init/Datatypes.o +theories/ZArith/Wf_Z.o : theories/ZArith/Wf_Z.hs +theories/ZArith/Wf_Z.o : theories/ZArith/Zarith_aux.o +theories/ZArith/Wf_Z.o : theories/ZArith/Fast_integer.o +theories/ZArith/Wf_Z.o : theories/Init/Specif.o +theories/ZArith/Wf_Z.o : theories/Init/Peano.o +theories/ZArith/Wf_Z.o : theories/Init/Logic.o +theories/ZArith/Wf_Z.o : theories/Init/Datatypes.o +theories/ZArith/Zarith_aux.o : theories/ZArith/Zarith_aux.hs +theories/ZArith/Zarith_aux.o : theories/ZArith/Fast_integer.o +theories/ZArith/Zarith_aux.o : theories/Init/Specif.o +theories/ZArith/Zarith_aux.o : theories/Init/Datatypes.o +theories/ZArith/ZArith_base.o : theories/ZArith/ZArith_base.hs +theories/ZArith/ZArith_dec.o : theories/ZArith/ZArith_dec.hs +theories/ZArith/ZArith_dec.o : theories/ZArith/Fast_integer.o +theories/ZArith/ZArith_dec.o : theories/Bool/Sumbool.o +theories/ZArith/ZArith_dec.o : theories/Init/Specif.o +theories/ZArith/ZArith_dec.o : theories/Init/Logic.o +theories/ZArith/ZArith.o : theories/ZArith/ZArith.hs +theories/ZArith/Zbool.o : theories/ZArith/Zbool.hs +theories/ZArith/Zbool.o : theories/ZArith/Fast_integer.o +theories/ZArith/Zbool.o : theories/ZArith/Zmisc.o +theories/ZArith/Zbool.o : theories/ZArith/ZArith_dec.o +theories/ZArith/Zbool.o : theories/Bool/Sumbool.o +theories/ZArith/Zbool.o : theories/Init/Specif.o +theories/ZArith/Zbool.o : theories/Init/Datatypes.o +theories/ZArith/Zcomplements.o : theories/ZArith/Zcomplements.hs +theories/ZArith/Zcomplements.o : theories/ZArith/Zarith_aux.o +theories/ZArith/Zcomplements.o : theories/ZArith/Fast_integer.o +theories/ZArith/Zcomplements.o : theories/ZArith/Wf_Z.o +theories/ZArith/Zcomplements.o : theories/Init/Specif.o +theories/ZArith/Zcomplements.o : theories/Init/Logic.o +theories/ZArith/Zcomplements.o : theories/Init/Datatypes.o +theories/ZArith/Zdiv.o : theories/ZArith/Zdiv.hs +theories/ZArith/Zdiv.o : theories/ZArith/Zarith_aux.o +theories/ZArith/Zdiv.o : theories/ZArith/Fast_integer.o +theories/ZArith/Zdiv.o : theories/ZArith/Zmisc.o +theories/ZArith/Zdiv.o : theories/ZArith/ZArith_dec.o +theories/ZArith/Zdiv.o : theories/Init/Specif.o +theories/ZArith/Zdiv.o : theories/Init/Logic.o +theories/ZArith/Zdiv.o : theories/Init/Datatypes.o +theories/ZArith/Zhints.o : theories/ZArith/Zhints.hs +theories/ZArith/Zlogarithm.o : theories/ZArith/Zlogarithm.hs +theories/ZArith/Zlogarithm.o : theories/ZArith/Zarith_aux.o +theories/ZArith/Zlogarithm.o : theories/ZArith/Fast_integer.o +theories/ZArith/Zmisc.o : theories/ZArith/Zmisc.hs +theories/ZArith/Zmisc.o : theories/ZArith/Fast_integer.o +theories/ZArith/Zmisc.o : theories/Init/Specif.o +theories/ZArith/Zmisc.o : theories/Init/Datatypes.o +theories/ZArith/Zpower.o : theories/ZArith/Zpower.hs +theories/ZArith/Zpower.o : theories/ZArith/Zarith_aux.o +theories/ZArith/Zpower.o : theories/ZArith/Fast_integer.o +theories/ZArith/Zpower.o : theories/ZArith/Zmisc.o +theories/ZArith/Zpower.o : theories/Init/Logic.o +theories/ZArith/Zpower.o : theories/Init/Datatypes.o +theories/ZArith/Zsqrt.o : theories/ZArith/Zsqrt.hs +theories/ZArith/Zsqrt.o : theories/ZArith/Zarith_aux.o +theories/ZArith/Zsqrt.o : theories/ZArith/Fast_integer.o +theories/ZArith/Zsqrt.o : theories/ZArith/ZArith_dec.o +theories/ZArith/Zsqrt.o : theories/Init/Specif.o +theories/ZArith/Zsqrt.o : theories/Init/Logic.o +theories/ZArith/Zwf.o : theories/ZArith/Zwf.hs +# DO NOT DELETE: End of Haskell dependencies diff --git a/contrib/extraction/test/addReals b/contrib/extraction/test/addReals new file mode 100644 index 00000000..fb73d47b --- /dev/null +++ b/contrib/extraction/test/addReals @@ -0,0 +1,21 @@ +open TypeSyntax +open Fast_integer + + +let total_order_T x y = +if x = y then InleftT RightT +else if x < y then InleftT LeftT +else InrightT + +let rec int_to_positive i = + if i = 1 then XH + else + if (i mod 2) = 0 then XO (int_to_positive (i/2)) + else XI (int_to_positive (i/2)) + +let rec int_to_Z i = + if i = 0 then ZERO + else if i > 0 then POS (int_to_positive i) + else NEG (int_to_positive (-i)) + +let my_ceil x = int_to_Z (succ (int_of_float (floor x))) diff --git a/contrib/extraction/test/custom/Adalloc b/contrib/extraction/test/custom/Adalloc new file mode 100644 index 00000000..0fb556aa --- /dev/null +++ b/contrib/extraction/test/custom/Adalloc @@ -0,0 +1,2 @@ +Require Import Addr. +Extraction NoInline ad_double ad_double_plus_un. diff --git a/contrib/extraction/test/custom/Euclid b/contrib/extraction/test/custom/Euclid new file mode 100644 index 00000000..a58e3940 --- /dev/null +++ b/contrib/extraction/test/custom/Euclid @@ -0,0 +1 @@ +Extraction Inline Wf_nat.gt_wf_rec Wf_nat.lt_wf_rec. diff --git a/contrib/extraction/test/custom/List b/contrib/extraction/test/custom/List new file mode 100644 index 00000000..ffee7dc9 --- /dev/null +++ b/contrib/extraction/test/custom/List @@ -0,0 +1 @@ +Extraction NoInline map. diff --git a/contrib/extraction/test/custom/ListSet b/contrib/extraction/test/custom/ListSet new file mode 100644 index 00000000..c9bea52a --- /dev/null +++ b/contrib/extraction/test/custom/ListSet @@ -0,0 +1 @@ +Extraction NoInline set_add set_mem. diff --git a/contrib/extraction/test/custom/Lsort b/contrib/extraction/test/custom/Lsort new file mode 100644 index 00000000..6a185683 --- /dev/null +++ b/contrib/extraction/test/custom/Lsort @@ -0,0 +1,2 @@ +Require Import Addr. +Extraction NoInline ad_double ad_double_plus_un. diff --git a/contrib/extraction/test/custom/Map b/contrib/extraction/test/custom/Map new file mode 100644 index 00000000..3e464e39 --- /dev/null +++ b/contrib/extraction/test/custom/Map @@ -0,0 +1,3 @@ +Require Import Addr. +Extraction NoInline ad_double ad_double_plus_un. + diff --git a/contrib/extraction/test/custom/Mapcard b/contrib/extraction/test/custom/Mapcard new file mode 100644 index 00000000..ca555aa3 --- /dev/null +++ b/contrib/extraction/test/custom/Mapcard @@ -0,0 +1,4 @@ +Require Import Plus. +Extraction NoInline plus_is_one. +Require Import Addr. +Extraction NoInline ad_double ad_double_plus_un. diff --git a/contrib/extraction/test/custom/Mapiter b/contrib/extraction/test/custom/Mapiter new file mode 100644 index 00000000..6a185683 --- /dev/null +++ b/contrib/extraction/test/custom/Mapiter @@ -0,0 +1,2 @@ +Require Import Addr. +Extraction NoInline ad_double ad_double_plus_un. diff --git a/contrib/extraction/test/custom/R_Ifp b/contrib/extraction/test/custom/R_Ifp new file mode 100644 index 00000000..d8f1b3e7 --- /dev/null +++ b/contrib/extraction/test/custom/R_Ifp @@ -0,0 +1,2 @@ +Load "custom/Reals". + diff --git a/contrib/extraction/test/custom/R_sqr b/contrib/extraction/test/custom/R_sqr new file mode 100644 index 00000000..d8f1b3e7 --- /dev/null +++ b/contrib/extraction/test/custom/R_sqr @@ -0,0 +1,2 @@ +Load "custom/Reals". + diff --git a/contrib/extraction/test/custom/Ranalysis b/contrib/extraction/test/custom/Ranalysis new file mode 100644 index 00000000..d8f1b3e7 --- /dev/null +++ b/contrib/extraction/test/custom/Ranalysis @@ -0,0 +1,2 @@ +Load "custom/Reals". + diff --git a/contrib/extraction/test/custom/Raxioms b/contrib/extraction/test/custom/Raxioms new file mode 100644 index 00000000..d8f1b3e7 --- /dev/null +++ b/contrib/extraction/test/custom/Raxioms @@ -0,0 +1,2 @@ +Load "custom/Reals". + diff --git a/contrib/extraction/test/custom/Rbase b/contrib/extraction/test/custom/Rbase new file mode 100644 index 00000000..d8f1b3e7 --- /dev/null +++ b/contrib/extraction/test/custom/Rbase @@ -0,0 +1,2 @@ +Load "custom/Reals". + diff --git a/contrib/extraction/test/custom/Rbasic_fun b/contrib/extraction/test/custom/Rbasic_fun new file mode 100644 index 00000000..d8f1b3e7 --- /dev/null +++ b/contrib/extraction/test/custom/Rbasic_fun @@ -0,0 +1,2 @@ +Load "custom/Reals". + diff --git a/contrib/extraction/test/custom/Rdefinitions b/contrib/extraction/test/custom/Rdefinitions new file mode 100644 index 00000000..d8f1b3e7 --- /dev/null +++ b/contrib/extraction/test/custom/Rdefinitions @@ -0,0 +1,2 @@ +Load "custom/Reals". + diff --git a/contrib/extraction/test/custom/Reals.v b/contrib/extraction/test/custom/Reals.v new file mode 100644 index 00000000..45d0a224 --- /dev/null +++ b/contrib/extraction/test/custom/Reals.v @@ -0,0 +1,17 @@ +Require Import Reals. +Extract Inlined Constant R => float. +Extract Inlined Constant R0 => "0.0". +Extract Inlined Constant R1 => "1.0". +Extract Inlined Constant Rplus => "(+.)". +Extract Inlined Constant Rmult => "( *.)". +Extract Inlined Constant Ropp => "(~-.)". +Extract Inlined Constant Rinv => "(fun x -> 1.0 /. x)". +Extract Inlined Constant Rlt => "(<)". +Extract Inlined Constant up => "AddReals.my_ceil". +Extract Inlined Constant total_order_T => "AddReals.total_order_T". +Extract Inlined Constant sqrt => "sqrt". +Extract Inlined Constant sigma => "(fun l h -> sigma_aux l h (Minus.minus h l))". +Extract Inlined Constant PI => "3.141593". +Extract Inlined Constant cos => cos. +Extract Inlined Constant sin => sin. +Extract Inlined Constant derive_pt => "(fun f x -> ((f (x+.1E-5))-.(f x))*.1E5)". diff --git a/contrib/extraction/test/custom/Rfunctions b/contrib/extraction/test/custom/Rfunctions new file mode 100644 index 00000000..d8f1b3e7 --- /dev/null +++ b/contrib/extraction/test/custom/Rfunctions @@ -0,0 +1,2 @@ +Load "custom/Reals". + diff --git a/contrib/extraction/test/custom/Rgeom b/contrib/extraction/test/custom/Rgeom new file mode 100644 index 00000000..d8f1b3e7 --- /dev/null +++ b/contrib/extraction/test/custom/Rgeom @@ -0,0 +1,2 @@ +Load "custom/Reals". + diff --git a/contrib/extraction/test/custom/Rlimit b/contrib/extraction/test/custom/Rlimit new file mode 100644 index 00000000..d8f1b3e7 --- /dev/null +++ b/contrib/extraction/test/custom/Rlimit @@ -0,0 +1,2 @@ +Load "custom/Reals". + diff --git a/contrib/extraction/test/custom/Rseries b/contrib/extraction/test/custom/Rseries new file mode 100644 index 00000000..d8f1b3e7 --- /dev/null +++ b/contrib/extraction/test/custom/Rseries @@ -0,0 +1,2 @@ +Load "custom/Reals". + diff --git a/contrib/extraction/test/custom/Rsigma b/contrib/extraction/test/custom/Rsigma new file mode 100644 index 00000000..d8f1b3e7 --- /dev/null +++ b/contrib/extraction/test/custom/Rsigma @@ -0,0 +1,2 @@ +Load "custom/Reals". + diff --git a/contrib/extraction/test/custom/Rtrigo b/contrib/extraction/test/custom/Rtrigo new file mode 100644 index 00000000..d8f1b3e7 --- /dev/null +++ b/contrib/extraction/test/custom/Rtrigo @@ -0,0 +1,2 @@ +Load "custom/Reals". + diff --git a/contrib/extraction/test/custom/ZArith_dec b/contrib/extraction/test/custom/ZArith_dec new file mode 100644 index 00000000..2201419e --- /dev/null +++ b/contrib/extraction/test/custom/ZArith_dec @@ -0,0 +1 @@ +Extraction Inline Dcompare_inf Zcompare_rec. diff --git a/contrib/extraction/test/custom/fast_integer b/contrib/extraction/test/custom/fast_integer new file mode 100644 index 00000000..e2b24953 --- /dev/null +++ b/contrib/extraction/test/custom/fast_integer @@ -0,0 +1 @@ +Extraction NoInline Zero_suivi_de Un_suivi_de. diff --git a/contrib/extraction/test/e b/contrib/extraction/test/e new file mode 100644 index 00000000..88b6c90b --- /dev/null +++ b/contrib/extraction/test/e @@ -0,0 +1,17 @@ + +(* To trace Extraction, you can use this file via: *) +(* Drop. #use "e";; *) +(* *) + +#use "include";; +open Extraction;; +open Miniml;; +#trace extract_declaration;; +go();; + + + + + + + diff --git a/contrib/extraction/test/extract b/contrib/extraction/test/extract new file mode 100755 index 00000000..83444be3 --- /dev/null +++ b/contrib/extraction/test/extract @@ -0,0 +1,12 @@ +#!/bin/sh +rm -f /tmp/extr$$.v +vfile=`./ml2v $1` +d=`dirname $vfile` +n=`basename $vfile .v` +if [ -e custom/$n ]; then cat custom/$n > /tmp/extr$$.v; fi +echo "Cd \"$d\". Extraction Library $n. " >> /tmp/extr$$.v +../../../bin/coqtop.opt -silent -batch -require $n -load-vernac-source /tmp/extr$$.v +out=$? +rm -f /tmp/extr$$.v +exit $out + diff --git a/contrib/extraction/test/extract.haskell b/contrib/extraction/test/extract.haskell new file mode 100755 index 00000000..d11bc706 --- /dev/null +++ b/contrib/extraction/test/extract.haskell @@ -0,0 +1,12 @@ +#!/bin/sh +rm -f /tmp/extr$$.v +vfile=`./hs2v $1` +d=`dirname $vfile` +n=`basename $vfile .v` +if [ -e custom/$n ]; then cat custom/$n > /tmp/extr$$.v; fi +echo "Cd \"$d\". Extraction Language Haskell. Extraction Library $n. " >> /tmp/extr$$.v +../../../bin/coqtop.opt -silent -batch -require $n -load-vernac-source /tmp/extr$$.v +out=$? +rm -f /tmp/extr$$.v +exit $out + diff --git a/contrib/extraction/test/hs2v.ml b/contrib/extraction/test/hs2v.ml new file mode 100644 index 00000000..fd8b9b26 --- /dev/null +++ b/contrib/extraction/test/hs2v.ml @@ -0,0 +1,14 @@ +let _ = + for j = 1 to ((Array.length Sys.argv)-1) do + let fml = Sys.argv.(j) in + let f = Filename.chop_extension fml in + let fv = f ^ ".v" in + if Sys.file_exists ("../../../" ^ fv) then + print_string (fv^" ") + else + let d = Filename.dirname f in + let b = String.uncapitalize (Filename.basename f) in + let fv = Filename.concat d (b ^ ".v ") in + print_string fv + done; + print_newline() diff --git a/contrib/extraction/test/make_mli b/contrib/extraction/test/make_mli new file mode 100755 index 00000000..40ee496e --- /dev/null +++ b/contrib/extraction/test/make_mli @@ -0,0 +1,17 @@ +#!/usr/bin/awk -We $0 + +{ match($0,"^open") + if (RLENGTH>0) state=1 + match($0,"^type") + if (RLENGTH>0) state=1 + match($0,"^\(\*\* ") + if (RLENGTH>0) state=2 + match($0,"^let") + if (RLENGTH>0) state=0 + match($0,"^and") + if ((RLENGTH>0) && (state==2)) state=0 + if ((RLENGTH>0) && (state==1)) state=1 + gsub("\(\*\* ","") + gsub("\*\*\)","") + if (state>0) print +} diff --git a/contrib/extraction/test/ml2v.ml b/contrib/extraction/test/ml2v.ml new file mode 100644 index 00000000..363ea642 --- /dev/null +++ b/contrib/extraction/test/ml2v.ml @@ -0,0 +1,14 @@ +let _ = + for j = 1 to ((Array.length Sys.argv)-1) do + let fml = Sys.argv.(j) in + let f = Filename.chop_extension fml in + let fv = f ^ ".v" in + if Sys.file_exists ("../../../" ^ fv) then + print_string (fv^" ") + else + let d = Filename.dirname f in + let b = String.capitalize (Filename.basename f) in + let fv = Filename.concat d (b ^ ".v ") in + print_string fv + done; + print_newline() diff --git a/contrib/extraction/test/v2hs.ml b/contrib/extraction/test/v2hs.ml new file mode 100644 index 00000000..88632875 --- /dev/null +++ b/contrib/extraction/test/v2hs.ml @@ -0,0 +1,9 @@ +let _ = + for j = 1 to ((Array.length Sys.argv) -1) do + let s = Sys.argv.(j) in + let b = Filename.chop_extension (Filename.basename s) in + let b = String.capitalize b in + let d = Filename.dirname s in + print_string (Filename.concat d (b ^ ".hs ")) + done; + print_newline() diff --git a/contrib/extraction/test/v2ml.ml b/contrib/extraction/test/v2ml.ml new file mode 100644 index 00000000..245a1b1e --- /dev/null +++ b/contrib/extraction/test/v2ml.ml @@ -0,0 +1,9 @@ +let _ = + for j = 1 to ((Array.length Sys.argv) -1) do + let s = Sys.argv.(j) in + let b = Filename.chop_extension (Filename.basename s) in + let b = String.uncapitalize b in + let d = Filename.dirname s in + print_string (Filename.concat d (b ^ ".ml ")) + done; + print_newline() |