aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorfilliatr2000-11-06 16:43:51 +0000
committerfilliatr2000-11-06 16:43:51 +0000
commit723c344d3e4cf7fdc2e4854ea7d55d140570424d (patch)
tree41ae18d8e43aa80007d361e83414d3b043f693ee
parent826913ee19c25cfe445f574080524662bdba1597 (diff)
nouveau discharge fait par le noyau; plus de recettes dans les corps des constantes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@807 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat
-rw-r--r--.depend1197
-rw-r--r--Makefile13
-rw-r--r--contrib/xml/xmlcommand.ml13
-rw-r--r--doc/kernel.dep.ps128
-rw-r--r--kernel/cooking.ml158
-rw-r--r--kernel/cooking.mli32
-rw-r--r--kernel/declarations.ml14
-rw-r--r--kernel/declarations.mli12
-rw-r--r--kernel/environ.ml10
-rw-r--r--kernel/environ.mli5
-rw-r--r--kernel/instantiate.ml9
-rw-r--r--kernel/safe_typing.ml73
-rw-r--r--kernel/safe_typing.mli16
-rw-r--r--lib/system.ml2
-rw-r--r--library/declare.ml26
-rw-r--r--library/declare.mli8
-rw-r--r--library/global.ml10
-rw-r--r--library/global.mli7
-rw-r--r--parsing/pretty.ml25
-rw-r--r--pretyping/class.ml4
-rw-r--r--proofs/pfedit.ml2
-rw-r--r--tactics/leminv.ml2
-rw-r--r--tactics/tactics.ml2
-rw-r--r--toplevel/command.ml45
-rw-r--r--toplevel/discharge.ml218
-rw-r--r--toplevel/record.ml4
-rw-r--r--toplevel/vernacentries.ml8
27 files changed, 1644 insertions, 399 deletions
diff --git a/.depend b/.depend
index e69de29bb2..df3667d677 100644
--- a/.depend
+++ b/.depend
@@ -0,0 +1,1197 @@
+kernel/closure.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
+ lib/pp.cmi kernel/term.cmi
+kernel/cooking.cmi: kernel/declarations.cmi kernel/environ.cmi \
+ kernel/names.cmi kernel/term.cmi
+kernel/declarations.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
+ kernel/univ.cmi
+kernel/environ.cmi: kernel/declarations.cmi kernel/names.cmi kernel/sign.cmi \
+ kernel/term.cmi kernel/univ.cmi
+kernel/evd.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi
+kernel/indtypes.cmi: kernel/declarations.cmi kernel/environ.cmi \
+ kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi
+kernel/inductive.cmi: kernel/declarations.cmi kernel/environ.cmi \
+ kernel/evd.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
+ kernel/univ.cmi
+kernel/instantiate.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
+ kernel/sign.cmi kernel/term.cmi
+kernel/names.cmi: lib/pp.cmi
+kernel/reduction.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \
+ kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi
+kernel/safe_typing.cmi: kernel/cooking.cmi kernel/declarations.cmi \
+ kernel/environ.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
+ kernel/sign.cmi kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi
+kernel/sign.cmi: kernel/names.cmi kernel/term.cmi
+kernel/term.cmi: kernel/names.cmi lib/pp.cmi kernel/univ.cmi lib/util.cmi
+kernel/type_errors.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
+ lib/pp.cmi kernel/sign.cmi kernel/term.cmi
+kernel/typeops.cmi: kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \
+ kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi
+kernel/univ.cmi: kernel/names.cmi lib/pp.cmi
+lib/pp.cmi: lib/pp_control.cmi
+lib/system.cmi: lib/pp.cmi
+lib/util.cmi: lib/pp.cmi
+library/declare.cmi: kernel/cooking.cmi kernel/declarations.cmi \
+ kernel/environ.cmi kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi \
+ kernel/term.cmi
+library/global.cmi: kernel/cooking.cmi kernel/declarations.cmi \
+ kernel/environ.cmi kernel/inductive.cmi kernel/names.cmi \
+ kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi
+library/goptions.cmi: kernel/names.cmi lib/pp.cmi
+library/impargs.cmi: kernel/inductive.cmi kernel/names.cmi kernel/term.cmi
+library/indrec.cmi: kernel/declarations.cmi kernel/environ.cmi kernel/evd.cmi \
+ kernel/inductive.cmi kernel/names.cmi kernel/term.cmi
+library/lib.cmi: library/libobject.cmi kernel/names.cmi library/summary.cmi
+library/libobject.cmi: kernel/names.cmi
+library/library.cmi: library/lib.cmi lib/pp.cmi
+library/nametab.cmi: kernel/names.cmi
+library/summary.cmi: kernel/names.cmi
+parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
+ parsing/pcoq.cmi lib/pp.cmi
+parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
+ kernel/names.cmi parsing/pattern.cmi pretyping/rawterm.cmi \
+ kernel/sign.cmi kernel/term.cmi
+parsing/coqast.cmi: lib/dyn.cmi
+parsing/egrammar.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
+ parsing/pcoq.cmi
+parsing/esyntax.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
+ lib/pp.cmi
+parsing/extend.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
+ lib/pp.cmi
+parsing/g_minicoq.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
+ kernel/term.cmi
+parsing/pattern.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
+ pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi
+parsing/pcoq.cmi: parsing/coqast.cmi
+parsing/pretty.cmi: kernel/declarations.cmi kernel/environ.cmi \
+ kernel/inductive.cmi library/lib.cmi kernel/names.cmi lib/pp.cmi \
+ kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi
+parsing/printer.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/names.cmi \
+ parsing/pattern.cmi lib/pp.cmi pretyping/rawterm.cmi kernel/sign.cmi \
+ kernel/term.cmi
+parsing/termast.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/names.cmi \
+ parsing/pattern.cmi pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi
+pretyping/cases.cmi: kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \
+ kernel/inductive.cmi kernel/names.cmi pretyping/rawterm.cmi \
+ kernel/term.cmi
+pretyping/class.cmi: pretyping/classops.cmi library/declare.cmi \
+ kernel/names.cmi kernel/term.cmi
+pretyping/classops.cmi: library/declare.cmi kernel/environ.cmi kernel/evd.cmi \
+ library/libobject.cmi kernel/names.cmi lib/pp.cmi pretyping/rawterm.cmi \
+ kernel/term.cmi
+pretyping/coercion.cmi: kernel/environ.cmi pretyping/evarutil.cmi \
+ kernel/evd.cmi pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi
+pretyping/detyping.cmi: kernel/environ.cmi kernel/names.cmi \
+ pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi
+pretyping/evarconv.cmi: kernel/environ.cmi pretyping/evarutil.cmi \
+ kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi
+pretyping/evarutil.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
+ pretyping/rawterm.cmi kernel/reduction.cmi kernel/sign.cmi \
+ kernel/term.cmi
+pretyping/multcase.cmi: kernel/environ.cmi pretyping/evarutil.cmi \
+ kernel/evd.cmi kernel/names.cmi pretyping/rawterm.cmi kernel/term.cmi
+pretyping/pretype_errors.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
+ pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \
+ kernel/type_errors.cmi
+pretyping/pretyping.cmi: kernel/environ.cmi pretyping/evarutil.cmi \
+ kernel/evd.cmi kernel/names.cmi pretyping/rawterm.cmi kernel/sign.cmi \
+ kernel/term.cmi
+pretyping/rawterm.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi
+pretyping/recordops.cmi: pretyping/classops.cmi library/libobject.cmi \
+ library/library.cmi kernel/names.cmi kernel/term.cmi
+pretyping/retyping.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
+ kernel/term.cmi
+pretyping/syntax_def.cmi: kernel/names.cmi pretyping/rawterm.cmi
+pretyping/tacred.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \
+ kernel/names.cmi kernel/reduction.cmi kernel/term.cmi
+pretyping/typing.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi
+proofs/clenv.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
+ lib/pp.cmi proofs/proof_type.cmi proofs/tacmach.cmi kernel/term.cmi \
+ lib/util.cmi
+proofs/evar_refiner.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
+ kernel/names.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
+ proofs/refiner.cmi kernel/sign.cmi kernel/term.cmi
+proofs/logic.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
+ lib/pp.cmi proofs/proof_type.cmi kernel/sign.cmi kernel/term.cmi
+proofs/macros.cmi: parsing/ast.cmi parsing/coqast.cmi kernel/names.cmi \
+ proofs/proof_type.cmi proofs/tacmach.cmi
+proofs/pfedit.cmi: parsing/coqast.cmi kernel/declarations.cmi \
+ library/declare.cmi kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
+ proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi
+proofs/proof_trees.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
+ kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi kernel/sign.cmi \
+ lib/stamps.cmi kernel/term.cmi lib/util.cmi
+proofs/proof_type.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
+ kernel/names.cmi lib/stamps.cmi pretyping/tacred.cmi kernel/term.cmi \
+ lib/util.cmi
+proofs/refiner.cmi: lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
+ kernel/sign.cmi kernel/term.cmi
+proofs/stock.cmi: kernel/names.cmi
+proofs/tacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/environ.cmi \
+ kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacmach.cmi \
+ proofs/tactic_debug.cmi kernel/term.cmi
+proofs/tacmach.cmi: parsing/coqast.cmi kernel/environ.cmi \
+ proofs/evar_refiner.cmi kernel/evd.cmi kernel/names.cmi lib/pp.cmi \
+ proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \
+ proofs/refiner.cmi kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi
+proofs/tactic_debug.cmi: parsing/coqast.cmi kernel/environ.cmi \
+ proofs/proof_type.cmi kernel/term.cmi
+tactics/auto.cmi: tactics/btermdn.cmi proofs/clenv.cmi parsing/coqast.cmi \
+ kernel/environ.cmi kernel/evd.cmi kernel/names.cmi parsing/pattern.cmi \
+ proofs/proof_type.cmi pretyping/rawterm.cmi kernel/sign.cmi \
+ proofs/tacmach.cmi kernel/term.cmi lib/util.cmi
+tactics/btermdn.cmi: parsing/pattern.cmi kernel/term.cmi
+tactics/dhyp.cmi: kernel/names.cmi proofs/tacmach.cmi
+tactics/elim.cmi: kernel/names.cmi proofs/proof_type.cmi proofs/tacmach.cmi \
+ tactics/tacticals.cmi kernel/term.cmi
+tactics/equality.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
+ tactics/hipattern.cmi kernel/names.cmi parsing/pattern.cmi \
+ proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi \
+ tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
+ tactics/wcclausenv.cmi
+tactics/hiddentac.cmi: kernel/names.cmi proofs/proof_type.cmi \
+ tactics/tacentries.cmi proofs/tacmach.cmi kernel/term.cmi
+tactics/hipattern.cmi: kernel/evd.cmi kernel/names.cmi parsing/pattern.cmi \
+ proofs/proof_trees.cmi kernel/sign.cmi proofs/stock.cmi kernel/term.cmi \
+ lib/util.cmi
+tactics/inv.cmi: parsing/coqast.cmi kernel/names.cmi proofs/tacmach.cmi
+tactics/nbtermdn.cmi: tactics/btermdn.cmi parsing/pattern.cmi kernel/term.cmi
+tactics/refine.cmi: proofs/tacmach.cmi kernel/term.cmi
+tactics/tacentries.cmi: proofs/proof_type.cmi proofs/tacmach.cmi
+tactics/tacticals.cmi: proofs/clenv.cmi parsing/coqast.cmi kernel/names.cmi \
+ parsing/pattern.cmi proofs/proof_type.cmi kernel/reduction.cmi \
+ kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi tactics/wcclausenv.cmi
+tactics/tactics.cmi: proofs/clenv.cmi kernel/environ.cmi kernel/evd.cmi \
+ kernel/names.cmi proofs/proof_type.cmi kernel/reduction.cmi \
+ proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \
+ kernel/term.cmi
+tactics/termdn.cmi: parsing/pattern.cmi kernel/term.cmi
+tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/environ.cmi kernel/evd.cmi \
+ kernel/names.cmi proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi \
+ kernel/term.cmi
+toplevel/command.cmi: parsing/coqast.cmi library/declare.cmi \
+ kernel/environ.cmi kernel/names.cmi proofs/proof_type.cmi \
+ pretyping/tacred.cmi kernel/term.cmi
+toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi
+toplevel/fhimsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
+ kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi
+toplevel/himsg.cmi: kernel/environ.cmi kernel/indtypes.cmi proofs/logic.cmi \
+ kernel/names.cmi lib/pp.cmi kernel/type_errors.cmi
+toplevel/metasyntax.cmi: parsing/coqast.cmi parsing/extend.cmi
+toplevel/mltop.cmi: library/libobject.cmi
+toplevel/protectedtoplevel.cmi: lib/pp.cmi
+toplevel/record.cmi: parsing/coqast.cmi kernel/names.cmi kernel/term.cmi
+toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
+ kernel/term.cmi
+toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi
+toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi
+toplevel/vernacentries.cmi: kernel/names.cmi kernel/term.cmi \
+ toplevel/vernacinterp.cmi
+toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
+ proofs/proof_type.cmi
+contrib/xml/xmlcommand.cmi: kernel/names.cmi
+config/coq_config.cmo: config/coq_config.cmi
+config/coq_config.cmx: config/coq_config.cmi
+dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi
+dev/db_printers.cmx: kernel/names.cmx lib/pp.cmx
+dev/top_printers.cmo: parsing/ast.cmi parsing/astterm.cmi proofs/clenv.cmi \
+ toplevel/command.cmi kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
+ lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi proofs/refiner.cmi \
+ kernel/sign.cmi lib/system.cmi proofs/tacmach.cmi kernel/term.cmi \
+ parsing/termast.cmi kernel/univ.cmi toplevel/vernacentries.cmi \
+ toplevel/vernacinterp.cmi
+dev/top_printers.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \
+ toplevel/command.cmx kernel/environ.cmx kernel/evd.cmx kernel/names.cmx \
+ lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx proofs/refiner.cmx \
+ kernel/sign.cmx lib/system.cmx proofs/tacmach.cmx kernel/term.cmx \
+ parsing/termast.cmx kernel/univ.cmx toplevel/vernacentries.cmx \
+ toplevel/vernacinterp.cmx
+kernel/closure.cmo: kernel/declarations.cmi kernel/environ.cmi kernel/evd.cmi \
+ kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
+ kernel/univ.cmi lib/util.cmi kernel/closure.cmi
+kernel/closure.cmx: kernel/declarations.cmx kernel/environ.cmx kernel/evd.cmx \
+ kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
+ kernel/univ.cmx lib/util.cmx kernel/closure.cmi
+kernel/cooking.cmo: kernel/declarations.cmi kernel/environ.cmi kernel/evd.cmi \
+ kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/reduction.cmi \
+ kernel/term.cmi lib/util.cmi kernel/cooking.cmi
+kernel/cooking.cmx: kernel/declarations.cmx kernel/environ.cmx kernel/evd.cmx \
+ kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx kernel/reduction.cmx \
+ kernel/term.cmx lib/util.cmx kernel/cooking.cmi
+kernel/declarations.cmo: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
+ kernel/univ.cmi kernel/declarations.cmi
+kernel/declarations.cmx: kernel/names.cmx kernel/sign.cmx kernel/term.cmx \
+ kernel/univ.cmx kernel/declarations.cmi
+kernel/environ.cmo: kernel/declarations.cmi kernel/names.cmi lib/pp.cmi \
+ kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
+ kernel/environ.cmi
+kernel/environ.cmx: kernel/declarations.cmx kernel/names.cmx lib/pp.cmx \
+ kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
+ kernel/environ.cmi
+kernel/evd.cmo: kernel/names.cmi kernel/sign.cmi kernel/term.cmi lib/util.cmi \
+ kernel/evd.cmi
+kernel/evd.cmx: kernel/names.cmx kernel/sign.cmx kernel/term.cmx lib/util.cmx \
+ kernel/evd.cmi
+kernel/indtypes.cmo: kernel/declarations.cmi kernel/environ.cmi \
+ kernel/evd.cmi kernel/inductive.cmi kernel/instantiate.cmi \
+ kernel/names.cmi kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
+ kernel/typeops.cmi lib/util.cmi kernel/indtypes.cmi
+kernel/indtypes.cmx: kernel/declarations.cmx kernel/environ.cmx \
+ kernel/evd.cmx kernel/inductive.cmx kernel/instantiate.cmx \
+ kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
+ kernel/typeops.cmx lib/util.cmx kernel/indtypes.cmi
+kernel/inductive.cmo: kernel/declarations.cmi kernel/environ.cmi \
+ kernel/instantiate.cmi kernel/names.cmi kernel/reduction.cmi \
+ kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
+ kernel/inductive.cmi
+kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \
+ kernel/instantiate.cmx kernel/names.cmx kernel/reduction.cmx \
+ kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
+ kernel/inductive.cmi
+kernel/instantiate.cmo: kernel/declarations.cmi kernel/environ.cmi \
+ kernel/evd.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \
+ kernel/term.cmi lib/util.cmi kernel/instantiate.cmi
+kernel/instantiate.cmx: kernel/declarations.cmx kernel/environ.cmx \
+ kernel/evd.cmx kernel/names.cmx lib/pp.cmx kernel/sign.cmx \
+ kernel/term.cmx lib/util.cmx kernel/instantiate.cmi
+kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/util.cmi kernel/names.cmi
+kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/util.cmx kernel/names.cmi
+kernel/reduction.cmo: kernel/closure.cmi kernel/declarations.cmi \
+ kernel/environ.cmi kernel/evd.cmi kernel/instantiate.cmi kernel/names.cmi \
+ lib/pp.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
+ kernel/reduction.cmi
+kernel/reduction.cmx: kernel/closure.cmx kernel/declarations.cmx \
+ kernel/environ.cmx kernel/evd.cmx kernel/instantiate.cmx kernel/names.cmx \
+ lib/pp.cmx kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
+ kernel/reduction.cmi
+kernel/safe_typing.cmo: kernel/cooking.cmi kernel/declarations.cmi \
+ kernel/environ.cmi kernel/evd.cmi kernel/indtypes.cmi \
+ kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/reduction.cmi \
+ kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi \
+ kernel/univ.cmi lib/util.cmi kernel/safe_typing.cmi
+kernel/safe_typing.cmx: kernel/cooking.cmx kernel/declarations.cmx \
+ kernel/environ.cmx kernel/evd.cmx kernel/indtypes.cmx \
+ kernel/inductive.cmx kernel/names.cmx lib/pp.cmx kernel/reduction.cmx \
+ kernel/sign.cmx kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx \
+ kernel/univ.cmx lib/util.cmx kernel/safe_typing.cmi
+kernel/sign.cmo: kernel/names.cmi kernel/term.cmi lib/util.cmi \
+ kernel/sign.cmi
+kernel/sign.cmx: kernel/names.cmx kernel/term.cmx lib/util.cmx \
+ kernel/sign.cmi
+kernel/term.cmo: lib/hashcons.cmi kernel/names.cmi lib/pp.cmi kernel/univ.cmi \
+ lib/util.cmi kernel/term.cmi
+kernel/term.cmx: lib/hashcons.cmx kernel/names.cmx lib/pp.cmx kernel/univ.cmx \
+ lib/util.cmx kernel/term.cmi
+kernel/type_errors.cmo: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
+ kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
+ kernel/type_errors.cmi
+kernel/type_errors.cmx: kernel/environ.cmx kernel/names.cmx lib/pp.cmx \
+ kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
+ kernel/type_errors.cmi
+kernel/typeops.cmo: kernel/declarations.cmi kernel/environ.cmi \
+ kernel/inductive.cmi kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \
+ kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
+ kernel/type_errors.cmi kernel/univ.cmi lib/util.cmi kernel/typeops.cmi
+kernel/typeops.cmx: kernel/declarations.cmx kernel/environ.cmx \
+ kernel/inductive.cmx kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \
+ kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
+ kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx kernel/typeops.cmi
+kernel/univ.cmo: lib/pp.cmi lib/util.cmi kernel/univ.cmi
+kernel/univ.cmx: lib/pp.cmx lib/util.cmx kernel/univ.cmi
+lib/bij.cmo: lib/gmap.cmi lib/bij.cmi
+lib/bij.cmx: lib/gmap.cmx lib/bij.cmi
+lib/bstack.cmo: lib/util.cmi lib/bstack.cmi
+lib/bstack.cmx: lib/util.cmx lib/bstack.cmi
+lib/dyn.cmo: lib/util.cmi lib/dyn.cmi
+lib/dyn.cmx: lib/util.cmx lib/dyn.cmi
+lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi
+lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi
+lib/gmap.cmo: lib/gmap.cmi
+lib/gmap.cmx: lib/gmap.cmi
+lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi
+lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi
+lib/gset.cmo: lib/gset.cmi
+lib/gset.cmx: lib/gset.cmi
+lib/hashcons.cmo: lib/hashcons.cmi
+lib/hashcons.cmx: lib/hashcons.cmi
+lib/options.cmo: lib/util.cmi lib/options.cmi
+lib/options.cmx: lib/util.cmx lib/options.cmi
+lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi
+lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi
+lib/pp_control.cmo: lib/pp_control.cmi
+lib/pp_control.cmx: lib/pp_control.cmi
+lib/profile.cmo: lib/system.cmi lib/profile.cmi
+lib/profile.cmx: lib/system.cmx lib/profile.cmi
+lib/stamps.cmo: lib/stamps.cmi
+lib/stamps.cmx: lib/stamps.cmi
+lib/system.cmo: lib/pp.cmi lib/util.cmi lib/system.cmi
+lib/system.cmx: lib/pp.cmx lib/util.cmx lib/system.cmi
+lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi
+lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi
+lib/util.cmo: lib/pp.cmi lib/util.cmi
+lib/util.cmx: lib/pp.cmx lib/util.cmi
+library/declare.cmo: kernel/cooking.cmi kernel/declarations.cmi \
+ kernel/environ.cmi kernel/evd.cmi library/global.cmi library/impargs.cmi \
+ library/indrec.cmi kernel/inductive.cmi library/lib.cmi \
+ library/libobject.cmi kernel/names.cmi library/nametab.cmi \
+ lib/options.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \
+ library/summary.cmi kernel/term.cmi kernel/type_errors.cmi \
+ kernel/typeops.cmi lib/util.cmi library/declare.cmi
+library/declare.cmx: kernel/cooking.cmx kernel/declarations.cmx \
+ kernel/environ.cmx kernel/evd.cmx library/global.cmx library/impargs.cmx \
+ library/indrec.cmx kernel/inductive.cmx library/lib.cmx \
+ library/libobject.cmx kernel/names.cmx library/nametab.cmx \
+ lib/options.cmx lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx \
+ library/summary.cmx kernel/term.cmx kernel/type_errors.cmx \
+ kernel/typeops.cmx lib/util.cmx library/declare.cmi
+library/global.cmo: kernel/environ.cmi kernel/inductive.cmi \
+ kernel/instantiate.cmi kernel/safe_typing.cmi kernel/sign.cmi \
+ library/summary.cmi kernel/term.cmi lib/util.cmi library/global.cmi
+library/global.cmx: kernel/environ.cmx kernel/inductive.cmx \
+ kernel/instantiate.cmx kernel/safe_typing.cmx kernel/sign.cmx \
+ library/summary.cmx kernel/term.cmx lib/util.cmx library/global.cmi
+library/goptions.cmo: library/lib.cmi library/libobject.cmi kernel/names.cmi \
+ lib/pp.cmi library/summary.cmi lib/util.cmi library/goptions.cmi
+library/goptions.cmx: library/lib.cmx library/libobject.cmx kernel/names.cmx \
+ lib/pp.cmx library/summary.cmx lib/util.cmx library/goptions.cmi
+library/impargs.cmo: kernel/declarations.cmi kernel/environ.cmi \
+ kernel/evd.cmi library/global.cmi kernel/inductive.cmi kernel/names.cmi \
+ kernel/reduction.cmi library/summary.cmi kernel/term.cmi \
+ library/impargs.cmi
+library/impargs.cmx: kernel/declarations.cmx kernel/environ.cmx \
+ kernel/evd.cmx library/global.cmx kernel/inductive.cmx kernel/names.cmx \
+ kernel/reduction.cmx library/summary.cmx kernel/term.cmx \
+ library/impargs.cmi
+library/indrec.cmo: kernel/declarations.cmi kernel/environ.cmi \
+ kernel/indtypes.cmi kernel/inductive.cmi kernel/instantiate.cmi \
+ kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \
+ kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \
+ library/indrec.cmi
+library/indrec.cmx: kernel/declarations.cmx kernel/environ.cmx \
+ kernel/indtypes.cmx kernel/inductive.cmx kernel/instantiate.cmx \
+ kernel/names.cmx lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx \
+ kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \
+ library/indrec.cmi
+library/lib.cmo: library/libobject.cmi kernel/names.cmi library/summary.cmi \
+ kernel/univ.cmi lib/util.cmi library/lib.cmi
+library/lib.cmx: library/libobject.cmx kernel/names.cmx library/summary.cmx \
+ kernel/univ.cmx lib/util.cmx library/lib.cmi
+library/libobject.cmo: lib/dyn.cmi kernel/names.cmi lib/util.cmi \
+ library/libobject.cmi
+library/libobject.cmx: lib/dyn.cmx kernel/names.cmx lib/util.cmx \
+ library/libobject.cmi
+library/library.cmo: kernel/environ.cmi library/global.cmi \
+ library/goptions.cmi library/lib.cmi library/libobject.cmi \
+ kernel/names.cmi lib/pp.cmi library/summary.cmi lib/system.cmi \
+ lib/util.cmi library/library.cmi
+library/library.cmx: kernel/environ.cmx library/global.cmx \
+ library/goptions.cmx library/lib.cmx library/libobject.cmx \
+ kernel/names.cmx lib/pp.cmx library/summary.cmx lib/system.cmx \
+ lib/util.cmx library/library.cmi
+library/nametab.cmo: kernel/names.cmi library/summary.cmi library/nametab.cmi
+library/nametab.cmx: kernel/names.cmx library/summary.cmx library/nametab.cmi
+library/states.cmo: library/lib.cmi library/library.cmi library/summary.cmi \
+ lib/system.cmi library/states.cmi
+library/states.cmx: library/lib.cmx library/library.cmx library/summary.cmx \
+ lib/system.cmx library/states.cmi
+library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \
+ library/summary.cmi
+library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \
+ library/summary.cmi
+parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi lib/hashcons.cmi \
+ kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi
+parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx lib/hashcons.cmx \
+ kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/ast.cmi
+parsing/astterm.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
+ kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \
+ library/global.cmi library/impargs.cmi kernel/names.cmi \
+ parsing/pattern.cmi lib/pp.cmi pretyping/pretype_errors.cmi \
+ pretyping/pretyping.cmi pretyping/rawterm.cmi kernel/reduction.cmi \
+ pretyping/retyping.cmi kernel/sign.cmi pretyping/syntax_def.cmi \
+ kernel/term.cmi pretyping/typing.cmi kernel/univ.cmi lib/util.cmi \
+ parsing/astterm.cmi
+parsing/astterm.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
+ kernel/environ.cmx pretyping/evarutil.cmx kernel/evd.cmx \
+ library/global.cmx library/impargs.cmx kernel/names.cmx \
+ parsing/pattern.cmx lib/pp.cmx pretyping/pretype_errors.cmx \
+ pretyping/pretyping.cmx pretyping/rawterm.cmx kernel/reduction.cmx \
+ pretyping/retyping.cmx kernel/sign.cmx pretyping/syntax_def.cmx \
+ kernel/term.cmx pretyping/typing.cmx kernel/univ.cmx lib/util.cmx \
+ parsing/astterm.cmi
+parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi parsing/coqast.cmi
+parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx parsing/coqast.cmi
+parsing/egrammar.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
+ parsing/lexer.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi \
+ parsing/egrammar.cmi
+parsing/egrammar.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmx \
+ parsing/lexer.cmx parsing/pcoq.cmx lib/pp.cmx lib/util.cmx \
+ parsing/egrammar.cmi
+parsing/esyntax.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
+ lib/gmap.cmi lib/gmapl.cmi lib/pp.cmi lib/util.cmi parsing/esyntax.cmi
+parsing/esyntax.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmx \
+ lib/gmap.cmx lib/gmapl.cmx lib/pp.cmx lib/util.cmx parsing/esyntax.cmi
+parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/lexer.cmi \
+ parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/extend.cmi
+parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/lexer.cmx \
+ parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/extend.cmi
+parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
+ toplevel/vernac.cmi
+parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
+ toplevel/vernac.cmx
+parsing/g_cases.cmo: parsing/coqast.cmi parsing/pcoq.cmi
+parsing/g_cases.cmx: parsing/coqast.cmx parsing/pcoq.cmx
+parsing/g_constr.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi
+parsing/g_constr.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx
+parsing/g_natsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \
+ parsing/coqast.cmi parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi \
+ lib/pp.cmi lib/util.cmi parsing/g_natsyntax.cmi
+parsing/g_natsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \
+ parsing/coqast.cmx parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmx \
+ lib/pp.cmx lib/util.cmx parsing/g_natsyntax.cmi
+parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi
+parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmx
+parsing/g_proofs.cmo: parsing/coqast.cmi parsing/pcoq.cmi lib/pp.cmi \
+ lib/util.cmi toplevel/vernac.cmi
+parsing/g_proofs.cmx: parsing/coqast.cmx parsing/pcoq.cmx lib/pp.cmx \
+ lib/util.cmx toplevel/vernac.cmx
+parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
+ lib/pp.cmi lib/util.cmi
+parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
+ lib/pp.cmx lib/util.cmx
+parsing/g_vernac.cmo: parsing/coqast.cmi parsing/pcoq.cmi lib/pp.cmi \
+ lib/util.cmi toplevel/vernac.cmi
+parsing/g_vernac.cmx: parsing/coqast.cmx parsing/pcoq.cmx lib/pp.cmx \
+ lib/util.cmx toplevel/vernac.cmx
+parsing/g_zsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
+ parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \
+ lib/util.cmi parsing/g_zsyntax.cmi
+parsing/g_zsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \
+ parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx \
+ lib/util.cmx parsing/g_zsyntax.cmi
+parsing/lexer.cmo: lib/util.cmi parsing/lexer.cmi
+parsing/lexer.cmx: lib/util.cmx parsing/lexer.cmi
+parsing/pattern.cmo: kernel/names.cmi pretyping/rawterm.cmi \
+ kernel/reduction.cmi kernel/term.cmi lib/util.cmi parsing/pattern.cmi
+parsing/pattern.cmx: kernel/names.cmx pretyping/rawterm.cmx \
+ kernel/reduction.cmx kernel/term.cmx lib/util.cmx parsing/pattern.cmi
+parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \
+ lib/util.cmi parsing/pcoq.cmi
+parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \
+ lib/util.cmx parsing/pcoq.cmi
+parsing/pretty.cmo: pretyping/classops.cmi kernel/declarations.cmi \
+ library/declare.cmi kernel/environ.cmi kernel/evd.cmi library/global.cmi \
+ library/impargs.cmi kernel/inductive.cmi kernel/instantiate.cmi \
+ library/lib.cmi library/libobject.cmi library/library.cmi \
+ kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/printer.cmi \
+ kernel/reduction.cmi kernel/sign.cmi pretyping/syntax_def.cmi \
+ kernel/term.cmi kernel/typeops.cmi lib/util.cmi parsing/pretty.cmi
+parsing/pretty.cmx: pretyping/classops.cmx kernel/declarations.cmx \
+ library/declare.cmx kernel/environ.cmx kernel/evd.cmx library/global.cmx \
+ library/impargs.cmx kernel/inductive.cmx kernel/instantiate.cmx \
+ library/lib.cmx library/libobject.cmx library/library.cmx \
+ kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/printer.cmx \
+ kernel/reduction.cmx kernel/sign.cmx pretyping/syntax_def.cmx \
+ kernel/term.cmx kernel/typeops.cmx lib/util.cmx parsing/pretty.cmi
+parsing/printer.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
+ kernel/environ.cmi parsing/esyntax.cmi parsing/extend.cmi \
+ library/global.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
+ parsing/pattern.cmi lib/pp.cmi kernel/sign.cmi kernel/term.cmi \
+ parsing/termast.cmi lib/util.cmi parsing/printer.cmi
+parsing/printer.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
+ kernel/environ.cmx parsing/esyntax.cmx parsing/extend.cmx \
+ library/global.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
+ parsing/pattern.cmx lib/pp.cmx kernel/sign.cmx kernel/term.cmx \
+ parsing/termast.cmx lib/util.cmx parsing/printer.cmi
+parsing/q_coqast.cmo: parsing/coqast.cmi parsing/pcoq.cmi
+parsing/q_coqast.cmx: parsing/coqast.cmx parsing/pcoq.cmx
+parsing/termast.cmo: parsing/ast.cmi pretyping/classops.cmi \
+ parsing/coqast.cmi library/declare.cmi pretyping/detyping.cmi \
+ kernel/environ.cmi library/impargs.cmi kernel/inductive.cmi \
+ kernel/names.cmi parsing/pattern.cmi lib/pp.cmi pretyping/rawterm.cmi \
+ kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi \
+ lib/util.cmi parsing/termast.cmi
+parsing/termast.cmx: parsing/ast.cmx pretyping/classops.cmx \
+ parsing/coqast.cmx library/declare.cmx pretyping/detyping.cmx \
+ kernel/environ.cmx library/impargs.cmx kernel/inductive.cmx \
+ kernel/names.cmx parsing/pattern.cmx lib/pp.cmx pretyping/rawterm.cmx \
+ kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx kernel/univ.cmx \
+ lib/util.cmx parsing/termast.cmi
+pretyping/cases.cmo: pretyping/coercion.cmi kernel/declarations.cmi \
+ kernel/environ.cmi pretyping/evarconv.cmi pretyping/evarutil.cmi \
+ library/global.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
+ pretyping/pretype_errors.cmi pretyping/rawterm.cmi kernel/reduction.cmi \
+ pretyping/retyping.cmi kernel/sign.cmi kernel/term.cmi \
+ kernel/type_errors.cmi kernel/typeops.cmi kernel/univ.cmi lib/util.cmi \
+ pretyping/cases.cmi
+pretyping/cases.cmx: pretyping/coercion.cmx kernel/declarations.cmx \
+ kernel/environ.cmx pretyping/evarconv.cmx pretyping/evarutil.cmx \
+ library/global.cmx kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \
+ pretyping/pretype_errors.cmx pretyping/rawterm.cmx kernel/reduction.cmx \
+ pretyping/retyping.cmx kernel/sign.cmx kernel/term.cmx \
+ kernel/type_errors.cmx kernel/typeops.cmx kernel/univ.cmx lib/util.cmx \
+ pretyping/cases.cmi
+pretyping/class.cmo: pretyping/classops.cmi kernel/declarations.cmi \
+ library/declare.cmi kernel/environ.cmi kernel/evd.cmi library/global.cmi \
+ kernel/inductive.cmi kernel/instantiate.cmi library/lib.cmi \
+ kernel/names.cmi lib/pp.cmi pretyping/retyping.cmi kernel/sign.cmi \
+ kernel/term.cmi pretyping/typing.cmi lib/util.cmi pretyping/class.cmi
+pretyping/class.cmx: pretyping/classops.cmx kernel/declarations.cmx \
+ library/declare.cmx kernel/environ.cmx kernel/evd.cmx library/global.cmx \
+ kernel/inductive.cmx kernel/instantiate.cmx library/lib.cmx \
+ kernel/names.cmx lib/pp.cmx pretyping/retyping.cmx kernel/sign.cmx \
+ kernel/term.cmx pretyping/typing.cmx lib/util.cmx pretyping/class.cmi
+pretyping/classops.cmo: library/declare.cmi kernel/environ.cmi \
+ library/lib.cmi library/libobject.cmi kernel/names.cmi lib/options.cmi \
+ lib/pp.cmi pretyping/rawterm.cmi library/summary.cmi pretyping/tacred.cmi \
+ kernel/term.cmi lib/util.cmi pretyping/classops.cmi
+pretyping/classops.cmx: library/declare.cmx kernel/environ.cmx \
+ library/lib.cmx library/libobject.cmx kernel/names.cmx lib/options.cmx \
+ lib/pp.cmx pretyping/rawterm.cmx library/summary.cmx pretyping/tacred.cmx \
+ kernel/term.cmx lib/util.cmx pretyping/classops.cmi
+pretyping/coercion.cmo: pretyping/classops.cmi kernel/environ.cmi \
+ pretyping/evarconv.cmi kernel/evd.cmi kernel/names.cmi \
+ pretyping/pretype_errors.cmi pretyping/recordops.cmi kernel/reduction.cmi \
+ pretyping/retyping.cmi kernel/term.cmi kernel/typeops.cmi lib/util.cmi \
+ pretyping/coercion.cmi
+pretyping/coercion.cmx: pretyping/classops.cmx kernel/environ.cmx \
+ pretyping/evarconv.cmx kernel/evd.cmx kernel/names.cmx \
+ pretyping/pretype_errors.cmx pretyping/recordops.cmx kernel/reduction.cmx \
+ pretyping/retyping.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \
+ pretyping/coercion.cmi
+pretyping/detyping.cmo: kernel/declarations.cmi library/declare.cmi \
+ library/global.cmi library/goptions.cmi library/impargs.cmi \
+ kernel/inductive.cmi kernel/names.cmi lib/pp.cmi pretyping/rawterm.cmi \
+ kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
+ pretyping/detyping.cmi
+pretyping/detyping.cmx: kernel/declarations.cmx library/declare.cmx \
+ library/global.cmx library/goptions.cmx library/impargs.cmx \
+ kernel/inductive.cmx kernel/names.cmx lib/pp.cmx pretyping/rawterm.cmx \
+ kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
+ pretyping/detyping.cmi
+pretyping/evarconv.cmo: pretyping/classops.cmi kernel/environ.cmi \
+ pretyping/evarutil.cmi kernel/evd.cmi kernel/instantiate.cmi \
+ kernel/names.cmi pretyping/recordops.cmi kernel/reduction.cmi \
+ kernel/term.cmi pretyping/typing.cmi lib/util.cmi pretyping/evarconv.cmi
+pretyping/evarconv.cmx: pretyping/classops.cmx kernel/environ.cmx \
+ pretyping/evarutil.cmx kernel/evd.cmx kernel/instantiate.cmx \
+ kernel/names.cmx pretyping/recordops.cmx kernel/reduction.cmx \
+ kernel/term.cmx pretyping/typing.cmx lib/util.cmx pretyping/evarconv.cmi
+pretyping/evarutil.cmo: kernel/environ.cmi kernel/evd.cmi library/global.cmi \
+ library/indrec.cmi kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \
+ pretyping/pretype_errors.cmi kernel/reduction.cmi kernel/sign.cmi \
+ kernel/term.cmi kernel/type_errors.cmi kernel/univ.cmi lib/util.cmi \
+ pretyping/evarutil.cmi
+pretyping/evarutil.cmx: kernel/environ.cmx kernel/evd.cmx library/global.cmx \
+ library/indrec.cmx kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \
+ pretyping/pretype_errors.cmx kernel/reduction.cmx kernel/sign.cmx \
+ kernel/term.cmx kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx \
+ pretyping/evarutil.cmi
+pretyping/pretype_errors.cmo: kernel/environ.cmi library/global.cmi \
+ kernel/names.cmi pretyping/rawterm.cmi kernel/sign.cmi \
+ kernel/type_errors.cmi pretyping/pretype_errors.cmi
+pretyping/pretype_errors.cmx: kernel/environ.cmx library/global.cmx \
+ kernel/names.cmx pretyping/rawterm.cmx kernel/sign.cmx \
+ kernel/type_errors.cmx pretyping/pretype_errors.cmi
+pretyping/pretyping.cmo: pretyping/cases.cmi pretyping/classops.cmi \
+ pretyping/coercion.cmi kernel/environ.cmi pretyping/evarconv.cmi \
+ pretyping/evarutil.cmi kernel/evd.cmi library/indrec.cmi \
+ kernel/inductive.cmi kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \
+ pretyping/pretype_errors.cmi pretyping/rawterm.cmi \
+ pretyping/recordops.cmi kernel/reduction.cmi pretyping/retyping.cmi \
+ kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi \
+ kernel/univ.cmi lib/util.cmi pretyping/pretyping.cmi
+pretyping/pretyping.cmx: pretyping/cases.cmx pretyping/classops.cmx \
+ pretyping/coercion.cmx kernel/environ.cmx pretyping/evarconv.cmx \
+ pretyping/evarutil.cmx kernel/evd.cmx library/indrec.cmx \
+ kernel/inductive.cmx kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \
+ pretyping/pretype_errors.cmx pretyping/rawterm.cmx \
+ pretyping/recordops.cmx kernel/reduction.cmx pretyping/retyping.cmx \
+ kernel/sign.cmx kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx \
+ kernel/univ.cmx lib/util.cmx pretyping/pretyping.cmi
+pretyping/rawterm.cmo: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
+ lib/util.cmi pretyping/rawterm.cmi
+pretyping/rawterm.cmx: kernel/names.cmx kernel/sign.cmx kernel/term.cmx \
+ lib/util.cmx pretyping/rawterm.cmi
+pretyping/recordops.cmo: pretyping/classops.cmi library/lib.cmi \
+ library/libobject.cmi library/library.cmi kernel/names.cmi lib/pp.cmi \
+ library/summary.cmi kernel/term.cmi kernel/typeops.cmi lib/util.cmi \
+ pretyping/recordops.cmi
+pretyping/recordops.cmx: pretyping/classops.cmx library/lib.cmx \
+ library/libobject.cmx library/library.cmx kernel/names.cmx lib/pp.cmx \
+ library/summary.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \
+ pretyping/recordops.cmi
+pretyping/retyping.cmo: kernel/environ.cmi kernel/inductive.cmi \
+ kernel/names.cmi kernel/reduction.cmi kernel/term.cmi kernel/typeops.cmi \
+ kernel/univ.cmi lib/util.cmi pretyping/retyping.cmi
+pretyping/retyping.cmx: kernel/environ.cmx kernel/inductive.cmx \
+ kernel/names.cmx kernel/reduction.cmx kernel/term.cmx kernel/typeops.cmx \
+ kernel/univ.cmx lib/util.cmx pretyping/retyping.cmi
+pretyping/syntax_def.cmo: library/lib.cmi library/libobject.cmi \
+ kernel/names.cmi library/nametab.cmi pretyping/rawterm.cmi \
+ library/summary.cmi pretyping/syntax_def.cmi
+pretyping/syntax_def.cmx: library/lib.cmx library/libobject.cmx \
+ kernel/names.cmx library/nametab.cmx pretyping/rawterm.cmx \
+ library/summary.cmx pretyping/syntax_def.cmi
+pretyping/tacred.cmo: kernel/closure.cmi library/declare.cmi \
+ kernel/environ.cmi kernel/evd.cmi library/global.cmi kernel/inductive.cmi \
+ kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/reduction.cmi \
+ library/summary.cmi kernel/term.cmi lib/util.cmi pretyping/tacred.cmi
+pretyping/tacred.cmx: kernel/closure.cmx library/declare.cmx \
+ kernel/environ.cmx kernel/evd.cmx library/global.cmx kernel/inductive.cmx \
+ kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx kernel/reduction.cmx \
+ library/summary.cmx kernel/term.cmx lib/util.cmx pretyping/tacred.cmi
+pretyping/typing.cmo: kernel/environ.cmi kernel/names.cmi \
+ kernel/reduction.cmi kernel/term.cmi kernel/type_errors.cmi \
+ kernel/typeops.cmi lib/util.cmi pretyping/typing.cmi
+pretyping/typing.cmx: kernel/environ.cmx kernel/names.cmx \
+ kernel/reduction.cmx kernel/term.cmx kernel/type_errors.cmx \
+ kernel/typeops.cmx lib/util.cmx pretyping/typing.cmi
+proofs/clenv.cmo: kernel/environ.cmi kernel/evd.cmi kernel/instantiate.cmi \
+ proofs/logic.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \
+ proofs/proof_type.cmi kernel/reduction.cmi pretyping/retyping.cmi \
+ kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi pretyping/typing.cmi \
+ lib/util.cmi proofs/clenv.cmi
+proofs/clenv.cmx: kernel/environ.cmx kernel/evd.cmx kernel/instantiate.cmx \
+ proofs/logic.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \
+ proofs/proof_type.cmx kernel/reduction.cmx pretyping/retyping.cmx \
+ kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx \
+ lib/util.cmx proofs/clenv.cmi
+proofs/evar_refiner.cmo: parsing/astterm.cmi kernel/environ.cmi \
+ pretyping/evarutil.cmi kernel/evd.cmi library/global.cmi proofs/logic.cmi \
+ kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \
+ kernel/reduction.cmi proofs/refiner.cmi kernel/sign.cmi lib/stamps.cmi \
+ kernel/term.cmi pretyping/typing.cmi lib/util.cmi proofs/evar_refiner.cmi
+proofs/evar_refiner.cmx: parsing/astterm.cmx kernel/environ.cmx \
+ pretyping/evarutil.cmx kernel/evd.cmx library/global.cmx proofs/logic.cmx \
+ kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \
+ kernel/reduction.cmx proofs/refiner.cmx kernel/sign.cmx lib/stamps.cmx \
+ kernel/term.cmx pretyping/typing.cmx lib/util.cmx proofs/evar_refiner.cmi
+proofs/logic.cmo: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \
+ pretyping/evarutil.cmi kernel/evd.cmi library/global.cmi \
+ kernel/inductive.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \
+ proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \
+ pretyping/retyping.cmi kernel/sign.cmi kernel/term.cmi \
+ kernel/type_errors.cmi kernel/typeops.cmi pretyping/typing.cmi \
+ lib/util.cmi proofs/logic.cmi
+proofs/logic.cmx: parsing/coqast.cmx library/declare.cmx kernel/environ.cmx \
+ pretyping/evarutil.cmx kernel/evd.cmx library/global.cmx \
+ kernel/inductive.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \
+ proofs/proof_trees.cmx proofs/proof_type.cmx kernel/reduction.cmx \
+ pretyping/retyping.cmx kernel/sign.cmx kernel/term.cmx \
+ kernel/type_errors.cmx kernel/typeops.cmx pretyping/typing.cmx \
+ lib/util.cmx proofs/logic.cmi
+proofs/macros.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \
+ library/libobject.cmi library/library.cmi kernel/names.cmi \
+ parsing/pcoq.cmi lib/pp.cmi proofs/proof_type.cmi library/summary.cmi \
+ kernel/term.cmi lib/util.cmi proofs/macros.cmi
+proofs/macros.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \
+ library/libobject.cmx library/library.cmx kernel/names.cmx \
+ parsing/pcoq.cmx lib/pp.cmx proofs/proof_type.cmx library/summary.cmx \
+ kernel/term.cmx lib/util.cmx proofs/macros.cmi
+proofs/pfedit.cmo: parsing/astterm.cmi kernel/declarations.cmi \
+ library/declare.cmi lib/edit.cmi kernel/environ.cmi kernel/evd.cmi \
+ library/lib.cmi kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \
+ proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \
+ pretyping/typing.cmi lib/util.cmi proofs/pfedit.cmi
+proofs/pfedit.cmx: parsing/astterm.cmx kernel/declarations.cmx \
+ library/declare.cmx lib/edit.cmx kernel/environ.cmx kernel/evd.cmx \
+ library/lib.cmx kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx \
+ proofs/proof_type.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \
+ pretyping/typing.cmx lib/util.cmx proofs/pfedit.cmi
+proofs/proof_trees.cmo: parsing/ast.cmi pretyping/detyping.cmi \
+ kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \
+ library/global.cmi kernel/names.cmi lib/pp.cmi parsing/pretty.cmi \
+ parsing/printer.cmi proofs/proof_type.cmi kernel/sign.cmi lib/stamps.cmi \
+ kernel/term.cmi parsing/termast.cmi pretyping/typing.cmi lib/util.cmi \
+ proofs/proof_trees.cmi
+proofs/proof_trees.cmx: parsing/ast.cmx pretyping/detyping.cmx \
+ kernel/environ.cmx pretyping/evarutil.cmx kernel/evd.cmx \
+ library/global.cmx kernel/names.cmx lib/pp.cmx parsing/pretty.cmx \
+ parsing/printer.cmx proofs/proof_type.cmx kernel/sign.cmx lib/stamps.cmx \
+ kernel/term.cmx parsing/termast.cmx pretyping/typing.cmx lib/util.cmx \
+ proofs/proof_trees.cmi
+proofs/proof_type.cmo: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
+ kernel/names.cmi lib/stamps.cmi pretyping/tacred.cmi kernel/term.cmi \
+ lib/util.cmi proofs/proof_type.cmi
+proofs/proof_type.cmx: parsing/coqast.cmx kernel/environ.cmx kernel/evd.cmx \
+ kernel/names.cmx lib/stamps.cmx pretyping/tacred.cmx kernel/term.cmx \
+ lib/util.cmx proofs/proof_type.cmi
+proofs/refiner.cmo: parsing/ast.cmi kernel/environ.cmi kernel/evd.cmi \
+ kernel/instantiate.cmi proofs/logic.cmi lib/pp.cmi parsing/printer.cmi \
+ proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \
+ kernel/sign.cmi lib/stamps.cmi kernel/term.cmi kernel/type_errors.cmi \
+ lib/util.cmi proofs/refiner.cmi
+proofs/refiner.cmx: parsing/ast.cmx kernel/environ.cmx kernel/evd.cmx \
+ kernel/instantiate.cmx proofs/logic.cmx lib/pp.cmx parsing/printer.cmx \
+ proofs/proof_trees.cmx proofs/proof_type.cmx kernel/reduction.cmx \
+ kernel/sign.cmx lib/stamps.cmx kernel/term.cmx kernel/type_errors.cmx \
+ lib/util.cmx proofs/refiner.cmi
+proofs/stock.cmo: lib/bij.cmi lib/gmap.cmi lib/gmapl.cmi library/library.cmi \
+ kernel/names.cmi lib/pp.cmi lib/util.cmi proofs/stock.cmi
+proofs/stock.cmx: lib/bij.cmx lib/gmap.cmx lib/gmapl.cmx library/library.cmx \
+ kernel/names.cmx lib/pp.cmx lib/util.cmx proofs/stock.cmi
+proofs/tacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/closure.cmi \
+ parsing/coqast.cmi library/declare.cmi lib/dyn.cmi kernel/environ.cmi \
+ kernel/evd.cmi lib/gmap.cmi library/lib.cmi library/libobject.cmi \
+ proofs/macros.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
+ parsing/pattern.cmi lib/pp.cmi proofs/proof_type.cmi \
+ pretyping/rawterm.cmi kernel/sign.cmi library/summary.cmi \
+ proofs/tacmach.cmi pretyping/tacred.cmi proofs/tactic_debug.cmi \
+ kernel/term.cmi pretyping/typing.cmi lib/util.cmi proofs/tacinterp.cmi
+proofs/tacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/closure.cmx \
+ parsing/coqast.cmx library/declare.cmx lib/dyn.cmx kernel/environ.cmx \
+ kernel/evd.cmx lib/gmap.cmx library/lib.cmx library/libobject.cmx \
+ proofs/macros.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
+ parsing/pattern.cmx lib/pp.cmx proofs/proof_type.cmx \
+ pretyping/rawterm.cmx kernel/sign.cmx library/summary.cmx \
+ proofs/tacmach.cmx pretyping/tacred.cmx proofs/tactic_debug.cmx \
+ kernel/term.cmx pretyping/typing.cmx lib/util.cmx proofs/tacinterp.cmi
+proofs/tacmach.cmo: parsing/ast.cmi parsing/astterm.cmi library/declare.cmi \
+ kernel/environ.cmi proofs/evar_refiner.cmi pretyping/evarutil.cmi \
+ kernel/evd.cmi library/global.cmi kernel/instantiate.cmi proofs/logic.cmi \
+ kernel/names.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \
+ proofs/proof_type.cmi kernel/reduction.cmi proofs/refiner.cmi \
+ kernel/sign.cmi lib/stamps.cmi pretyping/tacred.cmi kernel/term.cmi \
+ pretyping/typing.cmi lib/util.cmi proofs/tacmach.cmi
+proofs/tacmach.cmx: parsing/ast.cmx parsing/astterm.cmx library/declare.cmx \
+ kernel/environ.cmx proofs/evar_refiner.cmx pretyping/evarutil.cmx \
+ kernel/evd.cmx library/global.cmx kernel/instantiate.cmx proofs/logic.cmx \
+ kernel/names.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \
+ proofs/proof_type.cmx kernel/reduction.cmx proofs/refiner.cmx \
+ kernel/sign.cmx lib/stamps.cmx pretyping/tacred.cmx kernel/term.cmx \
+ pretyping/typing.cmx lib/util.cmx proofs/tacmach.cmi
+proofs/tactic_debug.cmo: parsing/ast.cmi lib/pp.cmi parsing/printer.cmi \
+ proofs/proof_trees.cmi proofs/tacmach.cmi proofs/tactic_debug.cmi
+proofs/tactic_debug.cmx: parsing/ast.cmx lib/pp.cmx parsing/printer.cmx \
+ proofs/proof_trees.cmx proofs/tacmach.cmx proofs/tactic_debug.cmi
+scripts/coqc.cmo: config/coq_config.cmi toplevel/usage.cmi
+scripts/coqc.cmx: config/coq_config.cmx toplevel/usage.cmx
+scripts/coqmktop.cmo: config/coq_config.cmi scripts/tolink.cmo
+scripts/coqmktop.cmx: config/coq_config.cmx scripts/tolink.cmx
+tactics/auto.cmo: parsing/astterm.cmi tactics/btermdn.cmi proofs/clenv.cmi \
+ parsing/coqast.cmi library/declare.cmi tactics/dhyp.cmi kernel/evd.cmi \
+ library/global.cmi tactics/hiddentac.cmi tactics/hipattern.cmi \
+ kernel/inductive.cmi library/lib.cmi library/libobject.cmi \
+ library/library.cmi proofs/logic.cmi kernel/names.cmi lib/options.cmi \
+ parsing/pattern.cmi proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi \
+ proofs/proof_type.cmi pretyping/rawterm.cmi kernel/reduction.cmi \
+ kernel/sign.cmi library/summary.cmi proofs/tacmach.cmi \
+ pretyping/tacred.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+ kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
+ toplevel/vernacinterp.cmi tactics/auto.cmi
+tactics/auto.cmx: parsing/astterm.cmx tactics/btermdn.cmx proofs/clenv.cmx \
+ parsing/coqast.cmx library/declare.cmx tactics/dhyp.cmx kernel/evd.cmx \
+ library/global.cmx tactics/hiddentac.cmx tactics/hipattern.cmx \
+ kernel/inductive.cmx library/lib.cmx library/libobject.cmx \
+ library/library.cmx proofs/logic.cmx kernel/names.cmx lib/options.cmx \
+ parsing/pattern.cmx proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx \
+ proofs/proof_type.cmx pretyping/rawterm.cmx kernel/reduction.cmx \
+ kernel/sign.cmx library/summary.cmx proofs/tacmach.cmx \
+ pretyping/tacred.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+ kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
+ toplevel/vernacinterp.cmx tactics/auto.cmi
+tactics/btermdn.cmo: tactics/dn.cmi parsing/pattern.cmi kernel/term.cmi \
+ tactics/termdn.cmi tactics/btermdn.cmi
+tactics/btermdn.cmx: tactics/dn.cmx parsing/pattern.cmx kernel/term.cmx \
+ tactics/termdn.cmx tactics/btermdn.cmi
+tactics/dhyp.cmo: parsing/ast.cmi parsing/astterm.cmi proofs/clenv.cmi \
+ parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi library/global.cmi \
+ library/lib.cmi library/libobject.cmi library/library.cmi \
+ kernel/names.cmi tactics/nbtermdn.cmi parsing/pattern.cmi \
+ parsing/pcoq.cmi lib/pp.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \
+ kernel/reduction.cmi library/summary.cmi proofs/tacinterp.cmi \
+ proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+ kernel/term.cmi lib/util.cmi toplevel/vernacinterp.cmi tactics/dhyp.cmi
+tactics/dhyp.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \
+ parsing/coqast.cmx kernel/environ.cmx kernel/evd.cmx library/global.cmx \
+ library/lib.cmx library/libobject.cmx library/library.cmx \
+ kernel/names.cmx tactics/nbtermdn.cmx parsing/pattern.cmx \
+ parsing/pcoq.cmx lib/pp.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \
+ kernel/reduction.cmx library/summary.cmx proofs/tacinterp.cmx \
+ proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+ kernel/term.cmx lib/util.cmx toplevel/vernacinterp.cmx tactics/dhyp.cmi
+tactics/dn.cmo: lib/tlm.cmi tactics/dn.cmi
+tactics/dn.cmx: lib/tlm.cmx tactics/dn.cmi
+tactics/eauto.cmo: tactics/auto.cmi proofs/clenv.cmi kernel/evd.cmi \
+ kernel/instantiate.cmi kernel/names.cmi parsing/pattern.cmi lib/pp.cmi \
+ proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \
+ kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
+ tactics/tactics.cmi kernel/term.cmi lib/util.cmi
+tactics/eauto.cmx: tactics/auto.cmx proofs/clenv.cmx kernel/evd.cmx \
+ kernel/instantiate.cmx kernel/names.cmx parsing/pattern.cmx lib/pp.cmx \
+ proofs/proof_trees.cmx proofs/proof_type.cmx kernel/reduction.cmx \
+ kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
+ tactics/tactics.cmx kernel/term.cmx lib/util.cmx
+tactics/elim.cmo: proofs/clenv.cmi tactics/hiddentac.cmi \
+ tactics/hipattern.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
+ proofs/proof_type.cmi kernel/reduction.cmi proofs/tacmach.cmi \
+ tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi lib/util.cmi \
+ tactics/elim.cmi
+tactics/elim.cmx: proofs/clenv.cmx tactics/hiddentac.cmx \
+ tactics/hipattern.cmx kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \
+ proofs/proof_type.cmx kernel/reduction.cmx proofs/tacmach.cmx \
+ tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx \
+ tactics/elim.cmi
+tactics/equality.cmo: parsing/astterm.cmi parsing/coqast.cmi \
+ library/declare.cmi kernel/environ.cmi kernel/evd.cmi library/global.cmi \
+ lib/gmapl.cmi tactics/hipattern.cmi kernel/inductive.cmi \
+ kernel/instantiate.cmi library/lib.cmi library/libobject.cmi \
+ proofs/logic.cmi kernel/names.cmi parsing/pattern.cmi lib/pp.cmi \
+ proofs/proof_type.cmi kernel/reduction.cmi pretyping/retyping.cmi \
+ library/summary.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \
+ pretyping/tacred.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+ kernel/term.cmi kernel/typeops.cmi pretyping/typing.cmi kernel/univ.cmi \
+ lib/util.cmi toplevel/vernacinterp.cmi tactics/wcclausenv.cmi \
+ tactics/equality.cmi
+tactics/equality.cmx: parsing/astterm.cmx parsing/coqast.cmx \
+ library/declare.cmx kernel/environ.cmx kernel/evd.cmx library/global.cmx \
+ lib/gmapl.cmx tactics/hipattern.cmx kernel/inductive.cmx \
+ kernel/instantiate.cmx library/lib.cmx library/libobject.cmx \
+ proofs/logic.cmx kernel/names.cmx parsing/pattern.cmx lib/pp.cmx \
+ proofs/proof_type.cmx kernel/reduction.cmx pretyping/retyping.cmx \
+ library/summary.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \
+ pretyping/tacred.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+ kernel/term.cmx kernel/typeops.cmx pretyping/typing.cmx kernel/univ.cmx \
+ lib/util.cmx toplevel/vernacinterp.cmx tactics/wcclausenv.cmx \
+ tactics/equality.cmi
+tactics/hiddentac.cmo: proofs/proof_type.cmi tactics/tacentries.cmi \
+ proofs/tacmach.cmi kernel/term.cmi tactics/hiddentac.cmi
+tactics/hiddentac.cmx: proofs/proof_type.cmx tactics/tacentries.cmx \
+ proofs/tacmach.cmx kernel/term.cmx tactics/hiddentac.cmi
+tactics/hipattern.cmo: parsing/astterm.cmi proofs/clenv.cmi \
+ library/declare.cmi kernel/environ.cmi kernel/evd.cmi library/global.cmi \
+ kernel/inductive.cmi library/library.cmi kernel/names.cmi \
+ parsing/pattern.cmi parsing/pcoq.cmi lib/pp.cmi parsing/printer.cmi \
+ proofs/proof_trees.cmi kernel/reduction.cmi proofs/stock.cmi \
+ kernel/term.cmi lib/util.cmi tactics/hipattern.cmi
+tactics/hipattern.cmx: parsing/astterm.cmx proofs/clenv.cmx \
+ library/declare.cmx kernel/environ.cmx kernel/evd.cmx library/global.cmx \
+ kernel/inductive.cmx library/library.cmx kernel/names.cmx \
+ parsing/pattern.cmx parsing/pcoq.cmx lib/pp.cmx parsing/printer.cmx \
+ proofs/proof_trees.cmx kernel/reduction.cmx proofs/stock.cmx \
+ kernel/term.cmx lib/util.cmx tactics/hipattern.cmi
+tactics/inv.cmo: tactics/auto.cmi proofs/clenv.cmi tactics/elim.cmi \
+ kernel/environ.cmi tactics/equality.cmi library/global.cmi \
+ kernel/inductive.cmi kernel/names.cmi parsing/pattern.cmi lib/pp.cmi \
+ parsing/printer.cmi proofs/proof_type.cmi kernel/reduction.cmi \
+ pretyping/retyping.cmi kernel/sign.cmi proofs/tacmach.cmi \
+ tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \
+ pretyping/typing.cmi lib/util.cmi tactics/wcclausenv.cmi tactics/inv.cmi
+tactics/inv.cmx: tactics/auto.cmx proofs/clenv.cmx tactics/elim.cmx \
+ kernel/environ.cmx tactics/equality.cmx library/global.cmx \
+ kernel/inductive.cmx kernel/names.cmx parsing/pattern.cmx lib/pp.cmx \
+ parsing/printer.cmx proofs/proof_type.cmx kernel/reduction.cmx \
+ pretyping/retyping.cmx kernel/sign.cmx proofs/tacmach.cmx \
+ tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
+ pretyping/typing.cmx lib/util.cmx tactics/wcclausenv.cmx tactics/inv.cmi
+tactics/leminv.cmo: parsing/astterm.cmi proofs/clenv.cmi \
+ kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
+ kernel/evd.cmi library/global.cmi kernel/inductive.cmi tactics/inv.cmi \
+ kernel/names.cmi proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi \
+ proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \
+ kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
+ tactics/tactics.cmi kernel/term.cmi lib/util.cmi \
+ toplevel/vernacinterp.cmi tactics/wcclausenv.cmi
+tactics/leminv.cmx: parsing/astterm.cmx proofs/clenv.cmx \
+ kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \
+ kernel/evd.cmx library/global.cmx kernel/inductive.cmx tactics/inv.cmx \
+ kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx \
+ proofs/proof_trees.cmx proofs/proof_type.cmx kernel/reduction.cmx \
+ kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
+ tactics/tactics.cmx kernel/term.cmx lib/util.cmx \
+ toplevel/vernacinterp.cmx tactics/wcclausenv.cmx
+tactics/nbtermdn.cmo: tactics/btermdn.cmi lib/gmap.cmi library/libobject.cmi \
+ library/library.cmi kernel/names.cmi parsing/pattern.cmi kernel/term.cmi \
+ tactics/termdn.cmi lib/util.cmi tactics/nbtermdn.cmi
+tactics/nbtermdn.cmx: tactics/btermdn.cmx lib/gmap.cmx library/libobject.cmx \
+ library/library.cmx kernel/names.cmx parsing/pattern.cmx kernel/term.cmx \
+ tactics/termdn.cmx lib/util.cmx tactics/nbtermdn.cmi
+tactics/refine.cmo: parsing/astterm.cmi kernel/environ.cmi kernel/evd.cmi \
+ kernel/names.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi \
+ kernel/reduction.cmi pretyping/retyping.cmi kernel/sign.cmi \
+ proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+ kernel/term.cmi pretyping/typing.cmi lib/util.cmi tactics/refine.cmi
+tactics/refine.cmx: parsing/astterm.cmx kernel/environ.cmx kernel/evd.cmx \
+ kernel/names.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx \
+ kernel/reduction.cmx pretyping/retyping.cmx kernel/sign.cmx \
+ proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+ kernel/term.cmx pretyping/typing.cmx lib/util.cmx tactics/refine.cmi
+tactics/tacentries.cmo: proofs/proof_trees.cmi proofs/tacmach.cmi \
+ tactics/tacticals.cmi tactics/tactics.cmi tactics/tacentries.cmi
+tactics/tacentries.cmx: proofs/proof_trees.cmx proofs/tacmach.cmx \
+ tactics/tacticals.cmx tactics/tactics.cmx tactics/tacentries.cmi
+tactics/tacticals.cmo: proofs/clenv.cmi parsing/coqast.cmi \
+ kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
+ library/global.cmi library/indrec.cmi kernel/inductive.cmi \
+ kernel/names.cmi parsing/pattern.cmi lib/pp.cmi parsing/pretty.cmi \
+ kernel/reduction.cmi kernel/sign.cmi lib/stamps.cmi proofs/tacinterp.cmi \
+ proofs/tacmach.cmi kernel/term.cmi parsing/termast.cmi lib/util.cmi \
+ tactics/wcclausenv.cmi tactics/tacticals.cmi
+tactics/tacticals.cmx: proofs/clenv.cmx parsing/coqast.cmx \
+ kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \
+ library/global.cmx library/indrec.cmx kernel/inductive.cmx \
+ kernel/names.cmx parsing/pattern.cmx lib/pp.cmx parsing/pretty.cmx \
+ kernel/reduction.cmx kernel/sign.cmx lib/stamps.cmx proofs/tacinterp.cmx \
+ proofs/tacmach.cmx kernel/term.cmx parsing/termast.cmx lib/util.cmx \
+ tactics/wcclausenv.cmx tactics/tacticals.cmi
+tactics/tactics.cmo: parsing/ast.cmi parsing/astterm.cmi proofs/clenv.cmi \
+ library/declare.cmi kernel/environ.cmi kernel/evd.cmi library/global.cmi \
+ tactics/hipattern.cmi library/indrec.cmi kernel/inductive.cmi \
+ proofs/logic.cmi kernel/names.cmi proofs/pfedit.cmi lib/pp.cmi \
+ proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \
+ kernel/sign.cmi lib/stamps.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \
+ pretyping/tacred.cmi tactics/tacticals.cmi kernel/term.cmi lib/util.cmi \
+ tactics/tactics.cmi
+tactics/tactics.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \
+ library/declare.cmx kernel/environ.cmx kernel/evd.cmx library/global.cmx \
+ tactics/hipattern.cmx library/indrec.cmx kernel/inductive.cmx \
+ proofs/logic.cmx kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx \
+ proofs/proof_trees.cmx proofs/proof_type.cmx kernel/reduction.cmx \
+ kernel/sign.cmx lib/stamps.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \
+ pretyping/tacred.cmx tactics/tacticals.cmx kernel/term.cmx lib/util.cmx \
+ tactics/tactics.cmi
+tactics/tauto.cmo: parsing/ast.cmi parsing/coqast.cmi tactics/hipattern.cmi \
+ kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacinterp.cmi \
+ proofs/tacmach.cmi tactics/tacticals.cmi
+tactics/tauto.cmx: parsing/ast.cmx parsing/coqast.cmx tactics/hipattern.cmx \
+ kernel/names.cmx lib/pp.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \
+ proofs/tacmach.cmx tactics/tacticals.cmx
+tactics/termdn.cmo: tactics/dn.cmi kernel/names.cmi parsing/pattern.cmi \
+ pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi tactics/termdn.cmi
+tactics/termdn.cmx: tactics/dn.cmx kernel/names.cmx parsing/pattern.cmx \
+ pretyping/rawterm.cmx kernel/term.cmx lib/util.cmx tactics/termdn.cmi
+tactics/wcclausenv.cmo: proofs/clenv.cmi kernel/environ.cmi kernel/evd.cmi \
+ library/global.cmi proofs/logic.cmi kernel/names.cmi lib/pp.cmi \
+ proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \
+ proofs/tacmach.cmi kernel/term.cmi lib/util.cmi tactics/wcclausenv.cmi
+tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \
+ library/global.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \
+ proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \
+ proofs/tacmach.cmx kernel/term.cmx lib/util.cmx tactics/wcclausenv.cmi
+tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo
+tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx
+tools/coqdep_lexer.cmo: config/coq_config.cmi
+tools/coqdep_lexer.cmx: config/coq_config.cmx
+toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
+ kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
+ kernel/evd.cmi library/global.cmi library/indrec.cmi kernel/inductive.cmi \
+ library/lib.cmi library/libobject.cmi library/library.cmi \
+ proofs/logic.cmi kernel/names.cmi lib/options.cmi proofs/pfedit.cmi \
+ lib/pp.cmi kernel/reduction.cmi library/states.cmi \
+ pretyping/syntax_def.cmi pretyping/tacred.cmi kernel/term.cmi \
+ lib/util.cmi toplevel/command.cmi
+toplevel/command.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \
+ kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \
+ kernel/evd.cmx library/global.cmx library/indrec.cmx kernel/inductive.cmx \
+ library/lib.cmx library/libobject.cmx library/library.cmx \
+ proofs/logic.cmx kernel/names.cmx lib/options.cmx proofs/pfedit.cmx \
+ lib/pp.cmx kernel/reduction.cmx library/states.cmx \
+ pretyping/syntax_def.cmx pretyping/tacred.cmx kernel/term.cmx \
+ lib/util.cmx toplevel/command.cmi
+toplevel/coqinit.cmo: config/coq_config.cmi library/library.cmi \
+ toplevel/mltop.cmi lib/options.cmi lib/pp.cmi lib/system.cmi \
+ toplevel/toplevel.cmi toplevel/vernac.cmi toplevel/coqinit.cmi
+toplevel/coqinit.cmx: config/coq_config.cmx library/library.cmx \
+ toplevel/mltop.cmi lib/options.cmx lib/pp.cmx lib/system.cmx \
+ toplevel/toplevel.cmx toplevel/vernac.cmx toplevel/coqinit.cmi
+toplevel/coqtop.cmo: config/coq_config.cmi toplevel/coqinit.cmi \
+ toplevel/errors.cmi library/lib.cmi library/library.cmi \
+ toplevel/mltop.cmi lib/options.cmi lib/pp.cmi lib/profile.cmi \
+ library/states.cmi lib/system.cmi toplevel/toplevel.cmi \
+ toplevel/usage.cmi lib/util.cmi toplevel/vernac.cmi toplevel/coqtop.cmi
+toplevel/coqtop.cmx: config/coq_config.cmx toplevel/coqinit.cmx \
+ toplevel/errors.cmx library/lib.cmx library/library.cmx \
+ toplevel/mltop.cmi lib/options.cmx lib/pp.cmx lib/profile.cmx \
+ library/states.cmx lib/system.cmx toplevel/toplevel.cmx \
+ toplevel/usage.cmx lib/util.cmx toplevel/vernac.cmx toplevel/coqtop.cmi
+toplevel/discharge.cmo: pretyping/class.cmi pretyping/classops.cmi \
+ kernel/cooking.cmi kernel/declarations.cmi library/declare.cmi \
+ kernel/environ.cmi kernel/evd.cmi library/global.cmi library/impargs.cmi \
+ kernel/inductive.cmi kernel/instantiate.cmi library/lib.cmi \
+ library/libobject.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \
+ pretyping/recordops.cmi kernel/reduction.cmi kernel/sign.cmi \
+ kernel/term.cmi kernel/typeops.cmi lib/util.cmi toplevel/discharge.cmi
+toplevel/discharge.cmx: pretyping/class.cmx pretyping/classops.cmx \
+ kernel/cooking.cmx kernel/declarations.cmx library/declare.cmx \
+ kernel/environ.cmx kernel/evd.cmx library/global.cmx library/impargs.cmx \
+ kernel/inductive.cmx kernel/instantiate.cmx library/lib.cmx \
+ library/libobject.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \
+ pretyping/recordops.cmx kernel/reduction.cmx kernel/sign.cmx \
+ kernel/term.cmx kernel/typeops.cmx lib/util.cmx toplevel/discharge.cmi
+toplevel/errors.cmo: parsing/ast.cmi toplevel/himsg.cmi kernel/indtypes.cmi \
+ parsing/lexer.cmi proofs/logic.cmi lib/options.cmi lib/pp.cmi \
+ proofs/tacmach.cmi kernel/type_errors.cmi lib/util.cmi \
+ toplevel/errors.cmi
+toplevel/errors.cmx: parsing/ast.cmx toplevel/himsg.cmx kernel/indtypes.cmx \
+ parsing/lexer.cmx proofs/logic.cmx lib/options.cmx lib/pp.cmx \
+ proofs/tacmach.cmx kernel/type_errors.cmx lib/util.cmx \
+ toplevel/errors.cmi
+toplevel/fhimsg.cmo: kernel/environ.cmi parsing/g_minicoq.cmi \
+ kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \
+ kernel/term.cmi kernel/type_errors.cmi lib/util.cmi toplevel/fhimsg.cmi
+toplevel/fhimsg.cmx: kernel/environ.cmx parsing/g_minicoq.cmi \
+ kernel/names.cmx lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx \
+ kernel/term.cmx kernel/type_errors.cmx lib/util.cmx toplevel/fhimsg.cmi
+toplevel/himsg.cmo: parsing/ast.cmi kernel/environ.cmi library/global.cmi \
+ kernel/indtypes.cmi kernel/inductive.cmi proofs/logic.cmi \
+ kernel/names.cmi lib/options.cmi lib/pp.cmi parsing/pretty.cmi \
+ parsing/printer.cmi kernel/reduction.cmi kernel/sign.cmi \
+ proofs/tacmach.cmi kernel/term.cmi kernel/type_errors.cmi lib/util.cmi \
+ toplevel/himsg.cmi
+toplevel/himsg.cmx: parsing/ast.cmx kernel/environ.cmx library/global.cmx \
+ kernel/indtypes.cmx kernel/inductive.cmx proofs/logic.cmx \
+ kernel/names.cmx lib/options.cmx lib/pp.cmx parsing/pretty.cmx \
+ parsing/printer.cmx kernel/reduction.cmx kernel/sign.cmx \
+ proofs/tacmach.cmx kernel/term.cmx kernel/type_errors.cmx lib/util.cmx \
+ toplevel/himsg.cmi
+toplevel/metasyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \
+ parsing/coqast.cmi parsing/egrammar.cmi parsing/esyntax.cmi \
+ parsing/extend.cmi library/lib.cmi library/libobject.cmi \
+ library/library.cmi parsing/pcoq.cmi lib/pp.cmi library/summary.cmi \
+ lib/util.cmi toplevel/vernac.cmi toplevel/metasyntax.cmi
+toplevel/metasyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \
+ parsing/coqast.cmx parsing/egrammar.cmx parsing/esyntax.cmx \
+ parsing/extend.cmx library/lib.cmx library/libobject.cmx \
+ library/library.cmx parsing/pcoq.cmx lib/pp.cmx library/summary.cmx \
+ lib/util.cmx toplevel/vernac.cmx toplevel/metasyntax.cmi
+toplevel/minicoq.cmo: kernel/declarations.cmi toplevel/fhimsg.cmi \
+ parsing/g_minicoq.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
+ kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi \
+ kernel/type_errors.cmi lib/util.cmi
+toplevel/minicoq.cmx: kernel/declarations.cmx toplevel/fhimsg.cmx \
+ parsing/g_minicoq.cmi kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \
+ kernel/safe_typing.cmx kernel/sign.cmx kernel/term.cmx \
+ kernel/type_errors.cmx lib/util.cmx
+toplevel/protectedtoplevel.cmo: toplevel/errors.cmi parsing/pcoq.cmi \
+ lib/pp.cmi toplevel/vernac.cmi toplevel/vernacinterp.cmi \
+ toplevel/protectedtoplevel.cmi
+toplevel/protectedtoplevel.cmx: toplevel/errors.cmx parsing/pcoq.cmx \
+ lib/pp.cmx toplevel/vernac.cmx toplevel/vernacinterp.cmx \
+ toplevel/protectedtoplevel.cmi
+toplevel/record.cmo: parsing/ast.cmi parsing/astterm.cmi pretyping/class.cmi \
+ toplevel/command.cmi parsing/coqast.cmi kernel/declarations.cmi \
+ library/declare.cmi kernel/environ.cmi kernel/evd.cmi library/global.cmi \
+ toplevel/himsg.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
+ pretyping/recordops.cmi kernel/term.cmi kernel/type_errors.cmi \
+ lib/util.cmi toplevel/record.cmi
+toplevel/record.cmx: parsing/ast.cmx parsing/astterm.cmx pretyping/class.cmx \
+ toplevel/command.cmx parsing/coqast.cmx kernel/declarations.cmx \
+ library/declare.cmx kernel/environ.cmx kernel/evd.cmx library/global.cmx \
+ toplevel/himsg.cmx kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \
+ pretyping/recordops.cmx kernel/term.cmx kernel/type_errors.cmx \
+ lib/util.cmx toplevel/record.cmi
+toplevel/toplevel.cmo: parsing/ast.cmi toplevel/errors.cmi toplevel/mltop.cmi \
+ kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
+ lib/pp.cmi toplevel/protectedtoplevel.cmi lib/util.cmi \
+ toplevel/vernac.cmi toplevel/vernacinterp.cmi toplevel/toplevel.cmi
+toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmi \
+ kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
+ lib/pp.cmx toplevel/protectedtoplevel.cmx lib/util.cmx \
+ toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi
+toplevel/usage.cmo: toplevel/usage.cmi
+toplevel/usage.cmx: toplevel/usage.cmi
+toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/library.cmi \
+ lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \
+ library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \
+ toplevel/vernac.cmi
+toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \
+ lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \
+ library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \
+ toplevel/vernac.cmi
+toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
+ pretyping/class.cmi toplevel/command.cmi parsing/coqast.cmi \
+ library/declare.cmi toplevel/discharge.cmi kernel/environ.cmi \
+ pretyping/evarutil.cmi kernel/evd.cmi parsing/extend.cmi \
+ library/global.cmi library/goptions.cmi library/impargs.cmi \
+ library/lib.cmi library/libobject.cmi library/library.cmi \
+ toplevel/metasyntax.cmi kernel/names.cmi library/nametab.cmi \
+ lib/options.cmi proofs/pfedit.cmi lib/pp.cmi lib/pp_control.cmi \
+ parsing/pretty.cmi parsing/printer.cmi proofs/proof_trees.cmi \
+ proofs/proof_type.cmi toplevel/record.cmi kernel/reduction.cmi \
+ proofs/refiner.cmi lib/stamps.cmi library/states.cmi lib/system.cmi \
+ proofs/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
+ proofs/tactic_debug.cmi tactics/tactics.cmi kernel/term.cmi \
+ kernel/typeops.cmi lib/util.cmi toplevel/vernacinterp.cmi \
+ toplevel/vernacentries.cmi
+toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \
+ pretyping/class.cmx toplevel/command.cmx parsing/coqast.cmx \
+ library/declare.cmx toplevel/discharge.cmx kernel/environ.cmx \
+ pretyping/evarutil.cmx kernel/evd.cmx parsing/extend.cmx \
+ library/global.cmx library/goptions.cmx library/impargs.cmx \
+ library/lib.cmx library/libobject.cmx library/library.cmx \
+ toplevel/metasyntax.cmx kernel/names.cmx library/nametab.cmx \
+ lib/options.cmx proofs/pfedit.cmx lib/pp.cmx lib/pp_control.cmx \
+ parsing/pretty.cmx parsing/printer.cmx proofs/proof_trees.cmx \
+ proofs/proof_type.cmx toplevel/record.cmx kernel/reduction.cmx \
+ proofs/refiner.cmx lib/stamps.cmx library/states.cmx lib/system.cmx \
+ proofs/tacinterp.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
+ proofs/tactic_debug.cmx tactics/tactics.cmx kernel/term.cmx \
+ kernel/typeops.cmx lib/util.cmx toplevel/vernacinterp.cmx \
+ toplevel/vernacentries.cmi
+toplevel/vernacinterp.cmo: parsing/ast.cmi toplevel/command.cmi \
+ parsing/coqast.cmi lib/dyn.cmi toplevel/himsg.cmi kernel/names.cmi \
+ lib/options.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacinterp.cmi \
+ lib/util.cmi toplevel/vernacinterp.cmi
+toplevel/vernacinterp.cmx: parsing/ast.cmx toplevel/command.cmx \
+ parsing/coqast.cmx lib/dyn.cmx toplevel/himsg.cmx kernel/names.cmx \
+ lib/options.cmx lib/pp.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \
+ lib/util.cmx toplevel/vernacinterp.cmi
+contrib/omega/coq_omega.cmo: parsing/ast.cmi proofs/clenv.cmi \
+ library/declare.cmi kernel/environ.cmi tactics/equality.cmi \
+ kernel/evd.cmi library/global.cmi kernel/inductive.cmi proofs/logic.cmi \
+ kernel/names.cmi contrib/omega/omega.cmo lib/pp.cmi parsing/printer.cmi \
+ proofs/proof_type.cmi kernel/reduction.cmi pretyping/retyping.cmi \
+ kernel/sign.cmi proofs/tacmach.cmi tactics/tactics.cmi kernel/term.cmi \
+ lib/util.cmi
+contrib/omega/coq_omega.cmx: parsing/ast.cmx proofs/clenv.cmx \
+ library/declare.cmx kernel/environ.cmx tactics/equality.cmx \
+ kernel/evd.cmx library/global.cmx kernel/inductive.cmx proofs/logic.cmx \
+ kernel/names.cmx contrib/omega/omega.cmx lib/pp.cmx parsing/printer.cmx \
+ proofs/proof_type.cmx kernel/reduction.cmx pretyping/retyping.cmx \
+ kernel/sign.cmx proofs/tacmach.cmx tactics/tactics.cmx kernel/term.cmx \
+ lib/util.cmx
+contrib/omega/omega.cmo: lib/util.cmi
+contrib/omega/omega.cmx: lib/util.cmx
+contrib/ring/quote.cmo: library/declare.cmi library/global.cmi \
+ kernel/instantiate.cmi kernel/names.cmi parsing/pattern.cmi lib/pp.cmi \
+ proofs/proof_trees.cmi proofs/proof_type.cmi proofs/tacmach.cmi \
+ tactics/tactics.cmi kernel/term.cmi lib/util.cmi
+contrib/ring/quote.cmx: library/declare.cmx library/global.cmx \
+ kernel/instantiate.cmx kernel/names.cmx parsing/pattern.cmx lib/pp.cmx \
+ proofs/proof_trees.cmx proofs/proof_type.cmx proofs/tacmach.cmx \
+ tactics/tactics.cmx kernel/term.cmx lib/util.cmx
+contrib/ring/ring.cmo: parsing/astterm.cmi kernel/closure.cmi \
+ library/declare.cmi tactics/equality.cmi kernel/evd.cmi \
+ library/global.cmi tactics/hiddentac.cmi tactics/hipattern.cmi \
+ library/lib.cmi library/libobject.cmi kernel/names.cmi \
+ parsing/pattern.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \
+ proofs/proof_type.cmi contrib/ring/quote.cmo kernel/reduction.cmi \
+ library/summary.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
+ tactics/tactics.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \
+ toplevel/vernacinterp.cmi
+contrib/ring/ring.cmx: parsing/astterm.cmx kernel/closure.cmx \
+ library/declare.cmx tactics/equality.cmx kernel/evd.cmx \
+ library/global.cmx tactics/hiddentac.cmx tactics/hipattern.cmx \
+ library/lib.cmx library/libobject.cmx kernel/names.cmx \
+ parsing/pattern.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \
+ proofs/proof_type.cmx contrib/ring/quote.cmx kernel/reduction.cmx \
+ library/summary.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
+ tactics/tactics.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
+ toplevel/vernacinterp.cmx
+contrib/xml/xml.cmo: contrib/xml/xml.cmi
+contrib/xml/xml.cmx: contrib/xml/xml.cmi
+contrib/xml/xmlcommand.cmo: kernel/declarations.cmi library/declare.cmi \
+ kernel/evd.cmi library/global.cmi library/lib.cmi library/libobject.cmi \
+ library/library.cmi kernel/names.cmi library/nametab.cmi \
+ proofs/pfedit.cmi proofs/proof_trees.cmi proofs/tacmach.cmi \
+ kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi \
+ contrib/xml/xmlcommand.cmi
+contrib/xml/xmlcommand.cmx: kernel/declarations.cmx library/declare.cmx \
+ kernel/evd.cmx library/global.cmx library/lib.cmx library/libobject.cmx \
+ library/library.cmx kernel/names.cmx library/nametab.cmx \
+ proofs/pfedit.cmx proofs/proof_trees.cmx proofs/tacmach.cmx \
+ kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx \
+ contrib/xml/xmlcommand.cmi
+contrib/xml/xmlentries.cmo: lib/util.cmi toplevel/vernacinterp.cmi \
+ contrib/xml/xmlcommand.cmi
+contrib/xml/xmlentries.cmx: lib/util.cmx toplevel/vernacinterp.cmx \
+ contrib/xml/xmlcommand.cmx
diff --git a/Makefile b/Makefile
index 95c1971c84..de15e784f4 100644
--- a/Makefile
+++ b/Makefile
@@ -69,7 +69,7 @@ KERNEL=kernel/names.cmo kernel/univ.cmo kernel/term.cmo \
kernel/environ.cmo kernel/evd.cmo kernel/instantiate.cmo \
kernel/closure.cmo kernel/reduction.cmo kernel/inductive.cmo\
kernel/type_errors.cmo kernel/typeops.cmo kernel/indtypes.cmo \
- kernel/safe_typing.cmo
+ kernel/cooking.cmo kernel/safe_typing.cmo
LIBRARY=library/libobject.cmo library/summary.cmo library/lib.cmo \
library/goptions.cmo \
@@ -385,26 +385,35 @@ minicoq: $(MINICOQCMO)
install: install-$(BEST) install-binaries install-library install-manpages
install-byte:
+ $(MKDIR) $(BINDIR)
cp $(COQMKTOP) $(COQC) coqtop.byte $(BINDIR)
cd $(BINDIR); ln -s coqtop.byte coqtop
install-opt:
+ $(MKDIR) $(BINDIR)
cp $(COQMKTOP) $(COQC) coqtop.byte coqtop.opt $(BINDIR)
cd $(BINDIR); ln -s coqtop.opt coqtop
install-binaries:
+ $(MKDIR) $(BINDIR)
cp tools/coqdep tools/gallina tools/coq_makefile tools/coq-tex \
$(BINDIR)
ALLVO=$(INITVO) $(TACTICSVO) $(THEORIESVO) $(CONTRIBVO)
install-library:
- cp $(ALLVO) $(COQLIB)
+ $(MKDIR) $(COQLIB)
+ for f in $(ALLVO); do \
+ $(MKDIR) $(COQLIB)/`dirname $$f`; \
+ cp $$f $(COQLIB)/`dirname $$f`; \
+ done
+ $(MKDIR) $(EMACSLIB)
cp tools/coq.el tools/coq.elc $(EMACSLIB)
MANPAGES=tools/coq-tex.1 tools/coqdep.1 tools/gallina.1
install-manpages:
+ $(MKDIR) $(MANDIR)/man1
cp $(MANPAGES) $(MANDIR)/man1
###########################################################################
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index bb8ab61257..edf93963f8 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -543,7 +543,8 @@ let print id fn =
begin
match val0 with
None -> print_axiom id typ [] hyps
- | Some lcvr ->
+ | Some c -> print_definition id c typ [] hyps
+ (*i No more recipes inside constants
match !lcvr with
D.Cooked c -> print_definition id c typ [] hyps
| D.Recipe _ ->
@@ -557,8 +558,9 @@ let print id fn =
Some {contents= D.Cooked c} ->
print_definition id c typ [] hyps
| _ -> Util.error "COOKING FAILED"
- end
- end
+ end
+ i*)
+ end
with
Not_found ->
try
@@ -656,10 +658,7 @@ let print_object o id sp dn fv =
begin
match val0 with
None -> print_axiom id typ fv hyps
- | Some lcvr ->
- match !lcvr with
- D.Cooked c -> print_definition id c typ fv hyps
- | D.Recipe _ -> Util.anomaly "trying to print a recipe"
+ | Some c -> print_definition id c typ fv hyps
end
| "INDUCTIVE" ->
(*CSC: QUI CI SONO ANCHE LE VARIABILI, CREDO, CHIAMATE mind_hyps *)
diff --git a/doc/kernel.dep.ps b/doc/kernel.dep.ps
index 7b66406111..692a28e87c 100644
--- a/doc/kernel.dep.ps
+++ b/doc/kernel.dep.ps
@@ -1,9 +1,9 @@
%!PS-Adobe-2.0
%%Creator: dot version uwin98 (01-26-98)
-%%For: (jacek) Jacek Chrzaszcz
+%%For: Gros nain
%%Title: G
%%Pages: (atend)
-%%BoundingBox: 36 36 577 70
+%%BoundingBox: 36 36 576 73
%%EndComments
%%BeginProlog
save
@@ -47,7 +47,7 @@ DotDict begin
gsave
coordfont setfont
0 0 moveto
- (\() show i str cvs show (,) show j str cvs show (\)) show
+ (() show i str cvs show (,) show j str cvs show ()) show
grestore
} if
} bind def
@@ -139,41 +139,41 @@ def
% /arrowwidth 5 def
%%EndSetup
%%Page: 1 1
-%%PageBoundingBox: 36 36 577 70
+%%PageBoundingBox: 36 36 576 73
gsave
-35 35 542 35 boxprim clip newpath
+35 35 541 38 boxprim clip newpath
36 36 translate
0 0 1 beginpage
-0.3745 set_scale
+0.3994 set_scale
0 0 translate 0 rotate
0.000 0.000 0.000 graphcolor
14.00 /Times-Roman set_font
% Univ
gsave 10 dict begin
-1319 45 27 18 ellipse_path
+1229 47 27 18 ellipse_path
stroke
gsave 10 dict begin
-1319 46 moveto (Univ) 28 14.00 -0.50 alignedtext
+1229 48 moveto (Univ) 28 14.00 -0.50 alignedtext
end grestore
end grestore
% Names
gsave 10 dict begin
-1412 45 29 18 ellipse_path
+1322 47 29 18 ellipse_path
stroke
gsave 10 dict begin
-1412 46 moveto (Names) 38 14.00 -0.50 alignedtext
+1322 48 moveto (Names) 38 14.00 -0.50 alignedtext
end grestore
end grestore
% Univ -> Names
-newpath 1346 45 moveto
-1354 45 1363 45 1372 45 curveto
+newpath 1256 47 moveto
+1264 47 1273 47 1282 47 curveto
stroke
-newpath 1372 43 moveto
-1382 45 lineto
-1372 48 lineto
+newpath 1282 45 moveto
+1292 47 lineto
+1282 50 lineto
closepath
gsave 0 setgray stroke grestore fill
@@ -274,39 +274,39 @@ gsave 0 setgray stroke grestore fill
% Term
gsave 10 dict begin
-1229 45 27 18 ellipse_path
+1139 47 27 18 ellipse_path
stroke
gsave 10 dict begin
-1229 46 moveto (Term) 30 14.00 -0.50 alignedtext
+1139 48 moveto (Term) 30 14.00 -0.50 alignedtext
end grestore
end grestore
% Term -> Univ
-newpath 1256 45 moveto
-1264 45 1273 45 1282 45 curveto
+newpath 1166 47 moveto
+1174 47 1183 47 1192 47 curveto
stroke
-newpath 1282 43 moveto
-1292 45 lineto
-1282 48 lineto
+newpath 1192 45 moveto
+1202 47 lineto
+1192 50 lineto
closepath
gsave 0 setgray stroke grestore fill
% Sign
gsave 10 dict begin
-1139 45 27 18 ellipse_path
+1049 47 27 18 ellipse_path
stroke
gsave 10 dict begin
-1139 46 moveto (Sign) 25 14.00 -0.50 alignedtext
+1049 48 moveto (Sign) 25 14.00 -0.50 alignedtext
end grestore
end grestore
% Sign -> Term
-newpath 1166 45 moveto
-1174 45 1183 45 1192 45 curveto
+newpath 1076 47 moveto
+1084 47 1093 47 1102 47 curveto
stroke
-newpath 1192 43 moveto
-1202 45 lineto
-1192 48 lineto
+newpath 1102 45 moveto
+1112 47 lineto
+1102 50 lineto
closepath
gsave 0 setgray stroke grestore fill
@@ -367,70 +367,80 @@ newpath 666 43 moveto
closepath
gsave 0 setgray stroke grestore fill
-% Evd
+% Environ
gsave 10 dict begin
-819 45 27 18 ellipse_path
+825 72 33 18 ellipse_path
stroke
gsave 10 dict begin
-819 46 moveto (Evd) 22 14.00 -0.50 alignedtext
+825 73 moveto (Environ) 45 14.00 -0.50 alignedtext
end grestore
end grestore
-% Instantiate -> Evd
-newpath 756 45 moveto
-765 45 774 45 782 45 curveto
+% Instantiate -> Environ
+newpath 751 54 moveto
+762 57 774 60 786 62 curveto
stroke
-newpath 782 43 moveto
-792 45 lineto
-782 48 lineto
+newpath 786 59 moveto
+795 65 lineto
+785 64 lineto
closepath
gsave 0 setgray stroke grestore fill
-% Environ
+% Evd
gsave 10 dict begin
-915 45 33 18 ellipse_path
+940 20 27 18 ellipse_path
stroke
gsave 10 dict begin
-915 46 moveto (Environ) 45 14.00 -0.50 alignedtext
+940 21 moveto (Evd) 22 14.00 -0.50 alignedtext
end grestore
end grestore
-% Evd -> Environ
-newpath 846 45 moveto
-854 45 863 45 872 45 curveto
+% Instantiate -> Evd
+newpath 755 41 moveto
+797 36 864 29 905 24 curveto
stroke
-newpath 872 43 moveto
-882 45 lineto
-872 48 lineto
+newpath 903 22 moveto
+913 23 lineto
+903 27 lineto
closepath
gsave 0 setgray stroke grestore fill
% Declarations
gsave 10 dict begin
-1030 45 45 18 ellipse_path
+940 74 45 18 ellipse_path
stroke
gsave 10 dict begin
-1030 46 moveto (Declarations) 70 14.00 -0.50 alignedtext
+940 75 moveto (Declarations) 70 14.00 -0.50 alignedtext
end grestore
end grestore
% Environ -> Declarations
-newpath 948 45 moveto
-956 45 965 45 974 45 curveto
+newpath 858 73 moveto
+866 73 875 73 884 73 curveto
+stroke
+newpath 884 71 moveto
+894 73 lineto
+884 76 lineto
+closepath
+gsave 0 setgray stroke grestore fill
+
+% Evd -> Sign
+newpath 966 26 moveto
+980 29 998 34 1015 38 curveto
stroke
-newpath 974 43 moveto
-984 45 lineto
-974 48 lineto
+newpath 1015 35 moveto
+1024 41 lineto
+1014 40 lineto
closepath
gsave 0 setgray stroke grestore fill
% Declarations -> Sign
-newpath 1076 45 moveto
-1085 45 1094 45 1102 45 curveto
+newpath 979 64 moveto
+991 62 1003 59 1015 56 curveto
stroke
-newpath 1102 43 moveto
-1112 45 lineto
-1102 48 lineto
+newpath 1014 54 moveto
+1024 53 lineto
+1015 59 lineto
closepath
gsave 0 setgray stroke grestore fill
endpage
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
new file mode 100644
index 0000000000..58fc1795b5
--- /dev/null
+++ b/kernel/cooking.ml
@@ -0,0 +1,158 @@
+
+(*i $Id$ i*)
+
+open Pp
+open Util
+open Names
+open Term
+open Sign
+open Declarations
+open Instantiate
+open Environ
+open Reduction
+
+(*s Cooking the constants. *)
+
+type modification_action = ABSTRACT | ERASE
+
+type 'a modification =
+ | NOT_OCCUR
+ | DO_ABSTRACT of 'a * modification_action list
+ | DO_REPLACE
+
+type work_alist = (global_reference * global_reference modification) list
+
+type recipe = {
+ d_from : section_path;
+ d_abstract : identifier list;
+ d_modlist : (global_reference * global_reference modification) list }
+
+let interp_modif absfun oper (oper',modif) cl =
+ let rec interprec = function
+ | ([], cl) ->
+ (match oper' with
+ | ConstRef sp -> mkConst (sp,Array.of_list cl)
+ | ConstructRef sp -> mkMutConstruct (sp,Array.of_list cl)
+ | IndRef sp -> mkMutInd (sp,Array.of_list cl))
+ | (ERASE::tlm, c::cl) -> interprec (tlm,cl)
+ | (ABSTRACT::tlm, c::cl) -> absfun (interprec (tlm,cl)) c
+ | _ -> assert false
+ in
+ interprec (modif,cl)
+
+let modify_opers replfun absfun oper_alist =
+ let failure () =
+ anomalylabstrm "generic__modify_opers"
+ [< 'sTR"An oper which was never supposed to appear has just appeared" ;
+ 'sPC ; 'sTR"Either this is in system code, and you need to" ; 'sPC;
+ 'sTR"report this error," ; 'sPC ;
+ 'sTR"Or you are using a user-written tactic which calls" ; 'sPC ;
+ 'sTR"generic__modify_opers, in which case the user-written code" ;
+ 'sPC ; 'sTR"is broken - this function is an internal system" ;
+ 'sPC ; 'sTR"for internal system use only" >]
+ in
+ let rec substrec c =
+ let op, cl = splay_constr c in
+ let cl' = Array.map substrec cl in
+ match op with
+ (* Hack pour le sp dans l'annotation du Cases *)
+ | OpMutCase (n,(spi,a,b,c,d) as oper) ->
+ (try
+ match List.assoc (IndRef spi) oper_alist with
+ | DO_ABSTRACT (IndRef spi',_) ->
+ gather_constr (OpMutCase (n,(spi',a,b,c,d)),cl')
+ | _ -> raise Not_found
+ with
+ | Not_found -> gather_constr (op,cl'))
+
+ | OpMutInd spi ->
+ (try
+ (match List.assoc (IndRef spi) oper_alist with
+ | NOT_OCCUR -> failure ()
+ | DO_ABSTRACT (oper',modif) ->
+ assert (List.length modif <= Array.length cl);
+ interp_modif absfun (IndRef spi) (oper',modif)
+ (Array.to_list cl')
+ | DO_REPLACE -> assert false)
+ with
+ | Not_found -> mkMutInd (spi,cl'))
+
+ | OpMutConstruct spi ->
+ (try
+ (match List.assoc (ConstructRef spi) oper_alist with
+ | NOT_OCCUR -> failure ()
+ | DO_ABSTRACT (oper',modif) ->
+ assert (List.length modif <= Array.length cl);
+ interp_modif absfun (ConstructRef spi) (oper',modif)
+ (Array.to_list cl')
+ | DO_REPLACE -> assert false)
+ with
+ | Not_found -> mkMutConstruct (spi,cl'))
+
+ | OpConst sp ->
+ (try
+ (match List.assoc (ConstRef sp) oper_alist with
+ | NOT_OCCUR -> failure ()
+ | DO_ABSTRACT (oper',modif) ->
+ assert (List.length modif <= Array.length cl);
+ interp_modif absfun (ConstRef sp) (oper',modif)
+ (Array.to_list cl')
+ | DO_REPLACE -> substrec (replfun (sp,cl')))
+ with
+ | Not_found -> mkConst (sp,cl'))
+
+ | _ -> gather_constr (op, cl')
+ in
+ if oper_alist = [] then fun x -> x else substrec
+
+let expmod_constr oldenv modlist c =
+ let sigma = Evd.empty in
+ let simpfun =
+ if modlist = [] then fun x -> x else nf_betaiota oldenv sigma in
+ let expfun cst =
+ try
+ constant_value oldenv cst
+ with NotEvaluableConst Opaque ->
+ let (sp,_) = cst in
+ errorlabstrm "expmod_constr"
+ [< 'sTR"Cannot unfold the value of ";
+ 'sTR(string_of_path sp); 'sPC;
+ 'sTR"You cannot declare local lemmas as being opaque"; 'sPC;
+ 'sTR"and then require that theorems which use them"; 'sPC;
+ 'sTR"be transparent" >];
+ in
+ let c' = modify_opers expfun (fun a b -> mkApp (a, [|b|])) modlist c in
+ match kind_of_term c' with
+ | IsCast (val_0,typ) -> mkCast (simpfun val_0,simpfun typ)
+ | _ -> simpfun c'
+
+let expmod_type oldenv modlist c =
+ type_app (expmod_constr oldenv modlist) c
+
+let abstract_constant ids_to_abs hyps (body,typ) =
+ let abstract_once ((hyps,body,typ) as sofar) id =
+ match hyps with
+ | [] ->
+ sofar
+ | (hyp,c,t as decl)::rest ->
+ if hyp <> id then
+ sofar
+ else
+ let body' = match body with
+ | None -> None
+ | Some c -> Some (mkNamedLambda_or_LetIn decl c)
+ in
+ let typ' = mkNamedProd_or_LetIn decl typ in
+ (rest, body', typ')
+ in
+ let (_,body',typ') =
+ List.fold_left abstract_once (hyps,body,typ) ids_to_abs in
+ (body',typ')
+
+let cook_constant env r =
+ let cb = lookup_constant r.d_from env in
+ let typ = expmod_type env r.d_modlist cb.const_type in
+ let body = option_app (expmod_constr env r.d_modlist) cb.const_body in
+ let hyps = map_named_context (expmod_constr env r.d_modlist) cb.const_hyps in
+ abstract_constant r.d_abstract hyps (body,typ)
+
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
new file mode 100644
index 0000000000..7d1bc39881
--- /dev/null
+++ b/kernel/cooking.mli
@@ -0,0 +1,32 @@
+
+(*i $Id$ i*)
+
+open Names
+open Term
+open Declarations
+open Environ
+
+(*s Cooking the constants. *)
+
+type modification_action = ABSTRACT | ERASE
+
+type 'a modification =
+ | NOT_OCCUR
+ | DO_ABSTRACT of 'a * modification_action list
+ | DO_REPLACE
+
+type work_alist = (global_reference * global_reference modification) list
+
+type recipe = {
+ d_from : section_path;
+ d_abstract : identifier list;
+ d_modlist : work_alist }
+
+val cook_constant : env -> recipe -> constr option * constr
+
+(*s Utility functions used in module [Discharge]. *)
+
+val expmod_constr : env -> work_alist -> constr -> constr
+val expmod_type : env -> work_alist -> types -> types
+
+
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index ff80c338f9..96eef57001 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -8,15 +8,9 @@ open Sign
(* Constant entries *)
-type lazy_constant_value =
- | Cooked of constr
- | Recipe of (unit -> constr)
-
-type constant_value = lazy_constant_value ref
-
type constant_body = {
const_kind : path_kind;
- const_body : constant_value option;
+ const_body : constr option;
const_type : types;
const_hyps : named_context;
const_constraints : constraints;
@@ -27,12 +21,8 @@ let is_defined cb =
let is_opaque cb = cb.const_opaque
-let cook_constant = function
- | { contents = Cooked c } -> c
- | { contents = Recipe f } as v -> let c = f () in v := Cooked c; c
-
type constant_entry = {
- const_entry_body : lazy_constant_value;
+ const_entry_body : constr;
const_entry_type : constr option }
(* Inductive entries *)
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 3be72f3fd1..3e7d8a9bdc 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -13,15 +13,9 @@ open Sign
(*s Constants (internal representation) (Definition/Axiom) *)
-type lazy_constant_value =
- | Cooked of constr
- | Recipe of (unit -> constr)
-
-type constant_value = lazy_constant_value ref
-
type constant_body = {
const_kind : path_kind;
- const_body : constant_value option;
+ const_body : constr option;
const_type : types;
const_hyps : named_context; (* New: younger hyp at top *)
const_constraints : constraints;
@@ -31,12 +25,10 @@ val is_defined : constant_body -> bool
val is_opaque : constant_body -> bool
-val cook_constant : constant_value -> constr
-
(*s Constant declaration. *)
type constant_entry = {
- const_entry_body : lazy_constant_value;
+ const_entry_body : constr;
const_entry_type : constr option }
(*s Inductive types (internal representation). *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 00e6d66f6a..2613199ffd 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -310,6 +310,16 @@ let evaluable_constant env k =
with Not_found ->
false
+(*s Opaque / Transparent switching *)
+
+let set_opaque env sp =
+ let cb = lookup_constant sp env in
+ cb.const_opaque <- true
+
+let set_transparent env sp =
+ let cb = lookup_constant sp env in
+ cb.const_opaque <- false
+
(*s Modules (i.e. compiled environments). *)
type compiled_env = {
diff --git a/kernel/environ.mli b/kernel/environ.mli
index c4a5e4659e..84f384759c 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -144,6 +144,11 @@ val prod_create : env -> types * constr -> constr
val defined_constant : env -> constant -> bool
val evaluable_constant : env -> constant -> bool
+(*s Opaque / Transparent switching *)
+
+val set_opaque : env -> section_path -> unit
+val set_transparent : env -> section_path -> unit
+
(*s Modules. *)
type compiled_env
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index f99ccb0c47..7f6f1258b5 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -41,15 +41,12 @@ exception NotEvaluableConst of const_evaluation_result
let constant_value env (sp,args) =
let cb = lookup_constant sp env in
- if cb.const_opaque then raise (NotEvaluableConst Opaque) else
- if not (is_defined cb) then raise (NotEvaluableConst NoBody) else
+ if cb.const_opaque then raise (NotEvaluableConst Opaque);
match cb.const_body with
- | Some v ->
- let body = cook_constant v in
+ | Some body ->
instantiate_constr cb.const_hyps body (Array.to_list args)
| None ->
- anomalylabstrm "termenv__constant_value"
- [< 'sTR "a defined constant with no body." >]
+ raise (NotEvaluableConst NoBody)
let constant_opt_value env cst =
try Some (constant_value env cst)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 48d9ad1848..db2f57d67c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -270,6 +270,20 @@ let push_rels_with_univ vars env =
(* Insertion of constants and parameters in environment. *)
+let add_parameter sp t env =
+ let (jt,cst) = safe_infer env t in
+ let env' = add_constraints cst env in
+ let ids = global_vars_set jt.uj_val in
+ let cb = {
+ const_kind = kind_of_path sp;
+ const_body = None;
+ const_type = assumption_of_judgment env' Evd.empty jt;
+ const_hyps = keep_hyps ids (named_context env);
+ const_constraints = cst;
+ const_opaque = false }
+ in
+ Environ.add_constant sp cb env'
+
let add_constant_with_value sp body typ env =
let (jb,cst) = safe_infer env body in
let env' = add_constraints cst env in
@@ -296,7 +310,7 @@ let add_constant_with_value sp body typ env =
in
let cb = {
const_kind = kind_of_path sp;
- const_body = Some (ref (Cooked body));
+ const_body = Some body;
const_type = ty;
const_hyps = keep_hyps ids (named_context env);
const_constraints = Constraint.union cst cst';
@@ -304,41 +318,29 @@ let add_constant_with_value sp body typ env =
in
add_constant sp cb env''
-let add_lazy_constant sp f t env =
- let (jt,cst) = safe_infer env t in
- let env' = add_constraints cst env in
- let ids = global_vars_set jt.uj_val in
- let cb = {
- const_kind = kind_of_path sp;
- const_body = Some (ref (Recipe f));
- const_type = assumption_of_judgment env' Evd.empty jt;
- const_hyps = keep_hyps ids (named_context env);
- const_constraints = cst;
- const_opaque = false }
- in
- add_constant sp cb env'
+let add_discharged_constant sp r env =
+ let (body,typ) = Cooking.cook_constant env r in
+ match body with
+ | None ->
+ add_parameter sp typ env
+ | Some c ->
+ let (jtyp,cst) = safe_infer env typ in
+ let env' = add_constraints cst env in
+ let ids =
+ Idset.union (global_vars_set c)
+ (global_vars_set (body_of_type jtyp.uj_type))
+ in
+ let cb = { const_kind = kind_of_path sp;
+ const_body = body;
+ const_type = assumption_of_judgment env' Evd.empty jtyp;
+ const_hyps = keep_hyps ids (named_context env);
+ const_constraints = cst;
+ const_opaque = false }
+ in
+ add_constant sp cb env'
let add_constant sp ce env =
- match ce.const_entry_body with
- | Cooked c -> add_constant_with_value sp c ce.const_entry_type env
- | Recipe f ->
- (match ce.const_entry_type with
- | Some typ -> add_lazy_constant sp f typ env
- | None -> error "you cannot declare a lazy constant without type")
-
-let add_parameter sp t env =
- let (jt,cst) = safe_infer env t in
- let env' = add_constraints cst env in
- let ids = global_vars_set jt.uj_val in
- let cb = {
- const_kind = kind_of_path sp;
- const_body = None;
- const_type = assumption_of_judgment env' Evd.empty jt;
- const_hyps = keep_hyps ids (named_context env);
- const_constraints = cst;
- const_opaque = false }
- in
- Environ.add_constant sp cb env'
+ add_constant_with_value sp ce.const_entry_body ce.const_entry_type env
(* Insertion of inductive types. *)
@@ -462,6 +464,9 @@ let rec pop_named_decls idl env =
| [] -> env
| id::l -> pop_named_decls l (Environ.pop_named_decl id env)
+let set_opaque = Environ.set_opaque
+let set_transparent = Environ.set_transparent
+
let export = export
let import = import
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 89e3fbbb76..011d0e414e 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -31,13 +31,13 @@ val push_named_assum :
val push_named_def :
identifier * constr -> safe_environment -> safe_environment
-val add_constant :
- section_path -> constant_entry -> safe_environment -> safe_environment
-val add_lazy_constant :
- section_path -> (unit -> constr) -> constr -> safe_environment
- -> safe_environment
val add_parameter :
section_path -> constr -> safe_environment -> safe_environment
+val add_constant :
+ section_path -> constant_entry -> safe_environment -> safe_environment
+val add_discharged_constant :
+ section_path -> Cooking.recipe -> safe_environment -> safe_environment
+
val add_mind :
section_path -> mutual_inductive_entry -> safe_environment
-> safe_environment
@@ -46,13 +46,13 @@ val add_constraints : constraints -> safe_environment -> safe_environment
val pop_named_decls : identifier list -> safe_environment -> safe_environment
val lookup_named : identifier -> safe_environment -> constr option * types
-(*i
-val lookup_rel : int -> safe_environment -> name * types
-i*)
val lookup_constant : section_path -> safe_environment -> constant_body
val lookup_mind : section_path -> safe_environment -> mutual_inductive_body
val lookup_mind_specif : inductive -> safe_environment -> inductive_instance
+val set_opaque : safe_environment -> section_path -> unit
+val set_transparent : safe_environment -> section_path -> unit
+
val export : safe_environment -> string -> compiled_env
val import : compiled_env -> safe_environment -> safe_environment
diff --git a/lib/system.ml b/lib/system.ml
index cc567360b4..8c8dca7ba5 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -92,7 +92,7 @@ let try_remove f =
with _ -> mSGNL [< 'sTR"Warning: " ; 'sTR"Could not remove file " ;
'sTR f ; 'sTR" which is corrupted!" >]
-let marshal_out ch v = Marshal.to_channel ch v [Marshal.Closures]
+let marshal_out ch v = Marshal.to_channel ch v []
let marshal_in ch = Marshal.from_channel ch
exception Bad_magic_number of string
diff --git a/library/declare.ml b/library/declare.ml
index b46cf0e581..84cc2e5751 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -110,24 +110,31 @@ let declare_parameter id c =
(* Constants. *)
-type constant_declaration = constant_entry * strength
+type constant_declaration_type =
+ | ConstantEntry of constant_entry
+ | ConstantRecipe of Cooking.recipe
-let csttab = ref (Spmap.empty : constant_declaration Spmap.t)
+type constant_declaration = constant_declaration_type * strength
+
+let csttab = ref (Spmap.empty : strength Spmap.t)
let _ = Summary.declare_summary "CONSTANT"
{ Summary.freeze_function = (fun () -> !csttab);
Summary.unfreeze_function = (fun ft -> csttab := ft);
Summary.init_function = (fun () -> csttab := Spmap.empty) }
-let cache_constant (sp,((ce,_) as cd,imps)) =
- Global.add_constant sp ce;
+let cache_constant (sp,((cdt,stre),imps)) =
+ begin match cdt with
+ | ConstantEntry ce -> Global.add_constant sp ce
+ | ConstantRecipe r -> Global.add_discharged_constant sp r
+ end;
Nametab.push (basename sp) sp;
if imps then declare_constant_implicits sp;
- csttab := Spmap.add sp cd !csttab
+ csttab := Spmap.add sp stre !csttab
-let load_constant (sp,((ce,_) as cd,imps)) =
+let load_constant (sp,((ce,stre),imps)) =
if imps then declare_constant_implicits sp;
- csttab := Spmap.add sp cd !csttab
+ csttab := Spmap.add sp stre !csttab
let open_constant (sp,_) =
Nametab.push (basename sp) sp
@@ -192,8 +199,7 @@ let declare_mind mie =
let is_constant sp =
try let _ = Global.lookup_constant sp in true with Not_found -> false
-let constant_strength sp =
- let (_,stre) = Spmap.find sp !csttab in stre
+let constant_strength sp = Spmap.find sp !csttab
let constant_or_parameter_strength sp =
try constant_strength sp with Not_found -> NeverDischarge
@@ -359,7 +365,7 @@ let declare_eliminations sp i =
let mindstr = string_of_id (mis_typename mispec) in
let declare na c =
declare_constant (id_of_string na)
- ({ const_entry_body = Cooked c; const_entry_type = None },
+ (ConstantEntry { const_entry_body = c; const_entry_type = None },
NeverDischarge);
if Options.is_verbose() then pPNL [< 'sTR na; 'sTR " is defined" >]
in
diff --git a/library/declare.mli b/library/declare.mli
index cd931d94d6..b8e45bdea6 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -27,9 +27,15 @@ type section_variable_entry =
type sticky = bool
type variable_declaration = section_variable_entry * strength * sticky
+
val declare_variable : identifier -> variable_declaration -> unit
-type constant_declaration = constant_entry * strength
+type constant_declaration_type =
+ | ConstantEntry of constant_entry
+ | ConstantRecipe of Cooking.recipe
+
+type constant_declaration = constant_declaration_type * strength
+
val declare_constant : identifier -> constant_declaration -> unit
val declare_parameter : identifier -> constr -> unit
diff --git a/library/global.ml b/library/global.ml
index 7b69ca0a85..6a2dfe145e 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -33,21 +33,23 @@ let named_context () = named_context !global_env
let push_named_def idc = global_env := push_named_def idc !global_env
let push_named_assum idc = global_env := push_named_assum idc !global_env
-let add_constant sp ce = global_env := add_constant sp ce !global_env
let add_parameter sp c = global_env := add_parameter sp c !global_env
+let add_constant sp ce = global_env := add_constant sp ce !global_env
+let add_discharged_constant sp r =
+ global_env := add_discharged_constant sp r !global_env
let add_mind sp mie = global_env := add_mind sp mie !global_env
let add_constraints c = global_env := add_constraints c !global_env
let pop_named_decls ids = global_env := pop_named_decls ids !global_env
let lookup_named id = lookup_named id !global_env
-(*
-let lookup_rel n = lookup_rel n !global_env
-*)
let lookup_constant sp = lookup_constant sp !global_env
let lookup_mind sp = lookup_mind sp !global_env
let lookup_mind_specif c = lookup_mind_specif c !global_env
+let set_opaque sp = set_opaque !global_env sp
+let set_transparent sp = set_transparent !global_env sp
+
let export s = export !global_env s
let import cenv = global_env := import cenv !global_env
diff --git a/library/global.mli b/library/global.mli
index a59c998231..0dcaef62a1 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -26,19 +26,22 @@ val named_context : unit -> named_context
val push_named_assum : identifier * constr -> unit
val push_named_def : identifier * constr -> unit
-val add_constant : section_path -> constant_entry -> unit
val add_parameter : section_path -> constr -> unit
+val add_constant : section_path -> constant_entry -> unit
+val add_discharged_constant : section_path -> Cooking.recipe -> unit
val add_mind : section_path -> mutual_inductive_entry -> unit
val add_constraints : constraints -> unit
val pop_named_decls : identifier list -> unit
val lookup_named : identifier -> constr option * types
-(*i val lookup_rel : int -> name * types i*)
val lookup_constant : section_path -> constant_body
val lookup_mind : section_path -> mutual_inductive_body
val lookup_mind_specif : inductive -> inductive_instance
+val set_opaque : section_path -> unit
+val set_transparent : section_path -> unit
+
val export : string -> compiled_env
val import : compiled_env -> unit
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 75d6dc4ce1..35d36bfca3 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -51,20 +51,6 @@ let pkprinters = function
| CCI -> (prterm,prterm_env)
| _ -> anomaly "pkprinters"
-let print_recipe = function
- | Some { contents = Cooked c } -> prterm c
- | Some { contents = Recipe _ } -> [< 'sTR"<recipe>" >]
- | None -> [< 'sTR"<uncookable>" >]
-
-(*
-let fprint_recipe = function
- | Some c -> fprterm c
- | None -> [< 'sTR"<uncookable>" >]
-*)
-
-let print_typed_recipe (val_0,typ) =
- [< print_recipe val_0; 'fNL; 'sTR " : "; prtype typ; 'fNL >]
-
let print_impl_args = function
| [] -> [<>]
| [i] -> [< 'sTR"Position ["; 'iNT i; 'sTR"] is implicit" >]
@@ -211,6 +197,13 @@ let print_section_variable sp =
let l = implicits_of_var id in
[< print_named_decl d; print_impl_args l; 'fNL >]
+let print_body = function
+ | Some c -> prterm c
+ | None -> [< 'sTR"<no body>" >]
+
+let print_typed_body (val_0,typ) =
+ [< print_body val_0; 'fNL; 'sTR " : "; prtype typ; 'fNL >]
+
let print_constant with_values sep sp =
let cb = Global.lookup_constant sp in
if kind_of_path sp = CCI then
@@ -226,7 +219,7 @@ let print_constant with_values sep sp =
[< 'sTR(print_basename (ccisp_of sp)) ;
'sTR sep; 'cUT ;
if with_values then
- print_typed_recipe (val_0,typ)
+ print_typed_body (val_0,typ)
else
[< prtype typ ; 'fNL >] >]);
print_impl_args (list_of_implicits l); 'fNL >]
@@ -483,7 +476,7 @@ let print_local_context () =
Global.lookup_constant sp in
[< print_last_const rest;
'sTR(print_basename sp) ;'sTR" = ";
- print_typed_recipe (val_0,typ) >]
+ print_typed_body (val_0,typ) >]
| "INDUCTIVE" ->
let mib = Global.lookup_mind sp in
[< print_last_const rest;print_mutual sp mib; 'fNL >]
diff --git a/pretyping/class.ml b/pretyping/class.ml
index 0ea8e3113a..6dfb3ca0b9 100644
--- a/pretyping/class.ml
+++ b/pretyping/class.ml
@@ -259,8 +259,8 @@ let build_id_coercion idf_opt ids =
(string_of_cl (fst (constructor_at_head t))))
in
let constr_entry =
- { const_entry_body = Cooked constr_f; const_entry_type = None } in
- declare_constant idf (constr_entry,NeverDischarge);
+ { const_entry_body = constr_f; const_entry_type = None } in
+ declare_constant idf (ConstantEntry constr_entry,NeverDischarge);
idf
let add_new_coercion_in_graph1 (coef,v,stre,isid,cls,clt) idf ps =
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7534214839..d12a65db61 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -187,7 +187,7 @@ let cook_proof () =
and strength = ts.top_strength in
let pfterm = extract_pftreestate pfs in
(ident,
- ({ const_entry_body = Cooked pfterm; const_entry_type = Some concl },
+ ({ const_entry_body = pfterm; const_entry_type = Some concl },
strength))
(*********************************************************************)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index d562b0ed90..9290fd5a1c 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -231,7 +231,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
let add_inversion_lemma name env sigma t sort dep inv_op =
let invProof = inversion_scheme env sigma t sort dep inv_op in
declare_constant name
- ({ const_entry_body = Cooked invProof; const_entry_type = None },
+ (ConstantEntry { const_entry_body = invProof; const_entry_type = None },
NeverDischarge)
(* open Pfedit *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8b9a8d0af1..20bed0eab6 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1663,7 +1663,7 @@ let abstract_subproof name tac gls =
with e when catchable_exception e ->
(delete_current_proof(); raise e)
in (* Faudrait un peu fonctionnaliser cela *)
- Declare.declare_constant na (const,strength);
+ Declare.declare_constant na (ConstantEntry const,strength);
let newenv = Global.env() in
Declare.construct_reference newenv CCI na
in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index d51cf629c4..1a236c3ff7 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -33,29 +33,26 @@ let constant_entry_of_com (com,comtypopt) =
let env = Global.env() in
match comtypopt with
None ->
- { const_entry_body = Cooked (interp_constr sigma env com);
+ { const_entry_body = interp_constr sigma env com;
const_entry_type = None }
| Some comtyp ->
let typ = interp_type sigma env comtyp in
- { const_entry_body = Cooked (interp_casted_constr sigma env com typ);
+ { const_entry_body = interp_casted_constr sigma env com typ;
const_entry_type = Some typ }
let red_constant_entry ce = function
| None -> ce
| Some red ->
- let body = match ce.const_entry_body with
- | Cooked c -> c
- | Recipe _ -> assert false
- in
+ let body = ce.const_entry_body in
{ const_entry_body =
- Cooked (reduction_of_redexp red (Global.env()) Evd.empty body);
+ reduction_of_redexp red (Global.env()) Evd.empty body;
const_entry_type =
ce.const_entry_type }
let definition_body_red ident n com comtypeopt red_option =
let ce = constant_entry_of_com (com,comtypeopt) in
let ce' = red_constant_entry ce red_option in
- declare_constant ident (ce',n);
+ declare_constant ident (ConstantEntry ce',n);
if is_verbose() then message ((string_of_id ident) ^ " is defined")
let definition_body ident n com typ = definition_body_red ident n com typ None
@@ -237,13 +234,12 @@ let build_recursive lnameargsardef =
| fi::lf ->
let ce =
{ const_entry_body =
- Cooked
- (mkFix ((Array.of_list nvrec,i),
- (varrec,List.map (fun id -> Name id) lnamerec,
- recvec)));
+ mkFix ((Array.of_list nvrec,i),
+ (varrec,List.map (fun id -> Name id) lnamerec,
+ recvec));
const_entry_type = None }
in
- declare_constant fi (ce, n);
+ declare_constant fi (ConstantEntry ce, n);
declare (i+1) lf
| _ -> ()
in
@@ -256,9 +252,9 @@ let build_recursive lnameargsardef =
let _ =
List.fold_left
(fun subst (f,def) ->
- let ce = { const_entry_body = Cooked (replace_vars subst def);
+ let ce = { const_entry_body = replace_vars subst def;
const_entry_type = None } in
- declare_constant f (ce,n);
+ declare_constant f (ConstantEntry ce,n);
warning ((string_of_id f)^" is non-recursively defined");
(var_subst f) :: subst)
(List.map var_subst lnamerec)
@@ -308,12 +304,11 @@ let build_corecursive lnameardef =
| fi::lf ->
let ce =
{ const_entry_body =
- Cooked
- (mkCoFix (i, (varrec,List.map (fun id -> Name id) lnamerec,
- recvec)));
+ mkCoFix (i, (varrec,List.map (fun id -> Name id) lnamerec,
+ recvec));
const_entry_type = None }
in
- declare_constant fi (ce,n);
+ declare_constant fi (ConstantEntry ce,n);
declare (i+1) lf
| _ -> ()
in
@@ -324,9 +319,9 @@ let build_corecursive lnameardef =
let _ =
List.fold_left
(fun subst (f,def) ->
- let ce = { const_entry_body = Cooked (replace_vars subst def);
+ let ce = { const_entry_body = replace_vars subst def;
const_entry_type = None } in
- declare_constant f (ce,n);
+ declare_constant f (ConstantEntry ce,n);
warning ((string_of_id f)^" is non-recursively defined");
(var_subst f) :: subst)
(List.map var_subst lnamerec)
@@ -358,8 +353,8 @@ let build_scheme lnamedepindsort =
let n = NeverDischarge in
let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in
let rec declare decl fi =
- let ce = { const_entry_body = Cooked decl; const_entry_type = None }
- in declare_constant fi (ce,n)
+ let ce = { const_entry_body = decl; const_entry_type = None }
+ in declare_constant fi (ConstantEntry ce,n)
in
List.iter2 declare listdecl lrecnames;
if is_verbose() then pPNL(recursive_message lrecnames)
@@ -377,7 +372,7 @@ let start_proof_com sopt stre com =
let save_named opacity =
let id,(const,strength) = Pfedit.cook_proof () in
- declare_constant id (const,strength);
+ declare_constant id (ConstantEntry const,strength);
Pfedit.delete_current_proof ();
if Options.is_verbose() then message ((string_of_id id) ^ " is defined")
@@ -385,7 +380,7 @@ let save_anonymous opacity save_ident strength =
let id,(const,_) = Pfedit.cook_proof () in
if atompart_of_id id <> "Unnamed_thm" then
message("Overriding name "^(string_of_id id)^" and using "^save_ident);
- declare_constant (id_of_string save_ident) (const,strength);
+ declare_constant (id_of_string save_ident) (ConstantEntry const,strength);
Pfedit.delete_current_proof ();
if Options.is_verbose() then message (save_ident ^ " is defined")
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 2e64ccab17..b922aa13e7 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -10,6 +10,7 @@ open Declarations
open Inductive
open Instantiate
open Reduction
+open Cooking
open Typeops
open Libobject
open Lib
@@ -22,102 +23,14 @@ open Recordops
let recalc_sp sp =
let (_,spid,k) = repr_path sp in Lib.make_path spid k
-(* Abstractions. *)
+let build_abstract_list hyps ids_to_discard =
+ map_succeed
+ (fun id ->
+ if not (mem_named_context id hyps) then failwith "caugth"; ABSTRACT)
+ ids_to_discard
-let whd_all c = whd_betadeltaiota (Global.env()) Evd.empty c
-
-type modification_action = ABSTRACT | ERASE
-
-let interp_modif absfun oper (oper',modif) cl =
- let rec interprec = function
- | ([], cl) ->
- (match oper' with
- | ConstRef sp -> mkConst (sp,Array.of_list cl)
- | ConstructRef sp -> mkMutConstruct (sp,Array.of_list cl)
- | IndRef sp -> mkMutInd (sp,Array.of_list cl))
- | (ERASE::tlm, c::cl) -> interprec (tlm,cl)
- | (ABSTRACT::tlm, c::cl) -> absfun (interprec (tlm,cl)) c
- | _ -> assert false
- in
- interprec (modif,cl)
-
-type 'a modification =
- | NOT_OCCUR
- | DO_ABSTRACT of 'a * modification_action list
- | DO_REPLACE
-
-let modify_opers replfun absfun oper_alist =
- let failure () =
- anomalylabstrm "generic__modify_opers"
- [< 'sTR"An oper which was never supposed to appear has just appeared" ;
- 'sPC ; 'sTR"Either this is in system code, and you need to" ; 'sPC;
- 'sTR"report this error," ; 'sPC ;
- 'sTR"Or you are using a user-written tactic which calls" ; 'sPC ;
- 'sTR"generic__modify_opers, in which case the user-written code" ;
- 'sPC ; 'sTR"is broken - this function is an internal system" ;
- 'sPC ; 'sTR"for internal system use only" >]
- in
- let rec substrec c =
- let op, cl = splay_constr c in
- let cl' = Array.map substrec cl in
- match op with
- (* Hack pour le sp dans l'annotation du Cases *)
- | OpMutCase (n,(spi,a,b,c,d) as oper) ->
- (try
- match List.assoc (IndRef spi) oper_alist with
- | DO_ABSTRACT (IndRef spi',_) ->
- gather_constr (OpMutCase (n,(spi',a,b,c,d)),cl')
- | _ -> raise Not_found
- with
- | Not_found -> gather_constr (op,cl'))
-
- | OpMutInd spi ->
- (try
- (match List.assoc (IndRef spi) oper_alist with
- | NOT_OCCUR -> failure ()
- | DO_ABSTRACT (oper',modif) ->
- if List.length modif > Array.length cl then
- anomaly "found a reference with too few args"
- else
- interp_modif absfun (IndRef spi) (oper',modif)
- (Array.to_list cl')
- | DO_REPLACE -> assert false)
- with
- | Not_found -> mkMutInd (spi,cl'))
-
- | OpMutConstruct spi ->
- (try
- (match List.assoc (ConstructRef spi) oper_alist with
- | NOT_OCCUR -> failure ()
- | DO_ABSTRACT (oper',modif) ->
- if List.length modif > Array.length cl then
- anomaly "found a reference with too few args"
- else
- interp_modif absfun (ConstructRef spi) (oper',modif)
- (Array.to_list cl')
- | DO_REPLACE -> assert false)
- with
- | Not_found -> mkMutConstruct (spi,cl'))
-
- | OpConst sp ->
- (try
- (match List.assoc (ConstRef sp) oper_alist with
- | NOT_OCCUR -> failure ()
- | DO_ABSTRACT (oper',modif) ->
- if List.length modif > Array.length cl then
- anomaly "found a reference with too few args"
- else
- interp_modif absfun (ConstRef sp) (oper',modif)
- (Array.to_list cl')
- | DO_REPLACE -> substrec (replfun (sp,cl')))
- with
- | Not_found -> mkConst (sp,cl'))
-
- | _ -> gather_constr (op, cl')
- in
- if oper_alist = [] then fun x -> x else substrec
-
-(**)
+(* Discharge of inductives is done here (while discharge of constants
+ is done by the kernel for efficiency). *)
let abstract_inductive ids_to_abs hyps inds =
let abstract_one_var d inds =
@@ -153,72 +66,6 @@ let abstract_inductive ids_to_abs hyps inds =
inds' in
(inds'', List.rev revmodl)
-let abstract_constant ids_to_abs hyps (body,typ) =
- let abstract_once ((hyps,body,typ,modl) as sofar) id =
- match hyps with
- | [] -> sofar
- | (hyp,c,t as decl)::rest ->
- if hyp <> id then sofar
- else
- let body' = match body with
- | None -> None
- | Some { contents = Cooked c } ->
- Some (ref (Cooked (mkNamedLambda_or_LetIn decl c)))
- | Some { contents = Recipe f } ->
- Some (ref (Recipe (fun () -> mkNamedLambda_or_LetIn decl (f()))))
- in
- let typ' = mkNamedProd_or_LetIn decl typ in
- (rest, body', typ', ABSTRACT::modl)
- in
- let (_,body',typ',revmodl) =
- List.fold_left abstract_once (hyps,body,typ,[]) ids_to_abs in
- (body',typ', List.rev revmodl)
-
-
-(* Substitutions. *)
-
-let expmod_constr oldenv modlist c =
- let sigma = Evd.empty in
- let simpfun =
- if modlist = [] then fun x -> x else nf_betaiota oldenv sigma in
- let expfun cst =
- try
- constant_value oldenv cst
- with NotEvaluableConst Opaque ->
- let (sp,_) = cst in
- errorlabstrm "expmod_constr"
- [< 'sTR"Cannot unfold the value of " ;
- 'sTR(string_of_path sp) ; 'sPC;
- 'sTR"You cannot declare local lemmas as being opaque"; 'sPC;
- 'sTR"and then require that theorems which use them"; 'sPC;
- 'sTR"be transparent" >];
- in
- let under_casts f c = match kind_of_term c with
- | IsCast (c,t) -> mkCast (f c,f t)
- | _ -> f c
- in
- let c' = modify_opers expfun (fun a b -> mkApp (a, [|b|])) modlist c in
- match kind_of_term c' with
- | IsCast (val_0,typ) -> mkCast (simpfun val_0,simpfun typ)
- | _ -> simpfun c'
-
-let expmod_type oldenv modlist c =
- type_app (expmod_constr oldenv modlist) c
-
-let expmod_constant_value opaque oldenv modlist = function
- | None -> None
- | Some { contents = Cooked c } ->
- if opaque then
- (* None *)
- Some (ref (Recipe (fun () -> expmod_constr oldenv modlist c)))
- else
- Some (ref (Cooked (expmod_constr oldenv modlist c)))
- | Some { contents = Recipe f } ->
- Some (ref (Recipe (fun () -> expmod_constr oldenv modlist (f ()))))
-
-
-(* Discharge of inductive types. *)
-
let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
assert (Array.length mib.mind_packets > 0);
let finite = mib.mind_packets.(0).mind_finite in
@@ -250,24 +97,10 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
mind_entry_inds = inds' },
modifs)
-
-(* Discharge of constants. *)
-
-let process_constant osecsp nsecsp oldenv (ids_to_discard,modlist) cb =
- let body =
- expmod_constant_value cb.const_opaque oldenv modlist cb.const_body in
- let typ = expmod_type oldenv modlist cb.const_type in
- let hyps = map_named_context (expmod_constr oldenv modlist) cb.const_hyps in
- let (body',typ',modl) = abstract_constant ids_to_discard hyps (body,typ) in
- let mods = [ (ConstRef osecsp, DO_ABSTRACT(ConstRef nsecsp,modl)) ] in
- (body', body_of_type typ', mods)
-
-
-(* Discharge of the various objects of the environment. *)
+(* Discharge messages. *)
let constant_message id =
- if Options.is_verbose() then
- pPNL [< print_id id; 'sTR " is discharged." >]
+ if Options.is_verbose() then pPNL [< print_id id; 'sTR " is discharged." >]
let inductive_message inds =
if Options.is_verbose() then
@@ -279,16 +112,21 @@ let inductive_message inds =
(fun (id,_,_,_) -> print_id id) l;
'sPC; 'sTR "are discharged.">]))
+(* Discharge operations for the various objects of the environment. *)
+
type discharge_operation =
| Variable of identifier * section_variable_entry * strength * bool * bool
| Parameter of identifier * constr * bool
- | Constant of identifier * constant_entry * strength * bool
+ | Constant of identifier * recipe * strength * bool
| Inductive of mutual_inductive_entry * bool
| Class of cl_typ * cl_info_typ
| Struc of inductive_path * struc_typ
| Coercion of ((coe_typ * coe_info_typ) * cl_typ * cl_typ)
* identifier * int
+(* Main function to traverse the library segment and compute the various
+ discharge operations. *)
+
let process_object oldenv sec_sp (ops,ids_to_discard,work_alist) (sp,lobj) =
let tag = object_tag lobj in
match tag with
@@ -319,17 +157,15 @@ let process_object oldenv sec_sp (ops,ids_to_discard,work_alist) (sp,lobj) =
let spid = basename sp in
let imp = is_implicit_constant sp in
let newsp = recalc_sp sp in
- let (body,typ,mods) =
- process_constant sp newsp oldenv (ids_to_discard,work_alist) cb in
- let op = match body with
- | None ->
- Parameter (spid,typ,imp)
- | Some { contents = b } ->
- let ce =
- { const_entry_body = b; const_entry_type = Some typ } in
- Constant (spid,ce,stre,imp)
+ let mods =
+ let modl = build_abstract_list cb.const_hyps ids_to_discard in
+ [ (ConstRef sp, DO_ABSTRACT(ConstRef newsp,modl)) ]
in
- (op::ops, ids_to_discard, mods@work_alist)
+ let r = { d_from = sp;
+ d_modlist = work_alist;
+ d_abstract = ids_to_discard } in
+ let op = Constant (spid,r,stre,imp) in
+ (op :: ops, ids_to_discard, mods @ work_alist)
| "INDUCTIVE" ->
let mib = Environ.lookup_mind sp oldenv in
@@ -337,7 +173,7 @@ let process_object oldenv sec_sp (ops,ids_to_discard,work_alist) (sp,lobj) =
let imp = is_implicit_inductive_definition sp in
let (mie,mods) =
process_inductive sp newsp oldenv (ids_to_discard,work_alist) mib in
- ((Inductive(mie,imp))::ops, ids_to_discard, mods@work_alist)
+ ((Inductive(mie,imp)) :: ops, ids_to_discard, mods @ work_alist)
| "CLASS" ->
let ((cl,clinfo) as x) = outClass lobj in
@@ -386,8 +222,8 @@ let process_operation = function
| Parameter (spid,typ,imp) ->
with_implicits imp (declare_parameter spid) typ;
constant_message spid
- | Constant (spid,ce,stre,imp) ->
- with_implicits imp (declare_constant spid) (ce,stre);
+ | Constant (spid,r,stre,imp) ->
+ with_implicits imp (declare_constant spid) (ConstantRecipe r,stre);
constant_message spid
| Inductive (mie,imp) ->
let _ = with_implicits imp declare_mind mie in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 559c3f33f5..d377b46e8c 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -140,9 +140,9 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
let ok =
try
let cie =
- { const_entry_body = Cooked proj;
+ { const_entry_body = proj;
const_entry_type = None } in
- (declare_constant fi (cie,NeverDischarge); true)
+ (declare_constant fi (ConstantEntry cie,NeverDischarge); true)
with Type_errors.TypeError (k,ctx,te) ->
((warning_or_error coe
[<'sTR (string_of_id fi);
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index dffccf3f9c..114665bada 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -459,13 +459,13 @@ let _ =
save_anonymous_remark true (string_of_id id))
| _ -> bad_vernac_args "SaveAnonymousRmk")
-(***
let _ =
add "TRANSPARENT"
(fun id_list () ->
List.iter
(function
- | VARG_IDENTIFIER id -> set_transparent id
+ | VARG_IDENTIFIER id ->
+ let sp = Nametab.sp_of_id CCI id in Global.set_transparent sp
| _ -> bad_vernac_args "TRANSPARENT")
id_list)
@@ -474,10 +474,10 @@ let _ =
(fun id_list () ->
List.iter
(function
- | VARG_IDENTIFIER id -> set_opaque id
+ | VARG_IDENTIFIER id ->
+ let sp = Nametab.sp_of_id CCI id in Global.set_opaque sp
| _ -> bad_vernac_args "OPAQUE")
id_list)
-***)
let _ =
add "UNDO"
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:42:51 +0000