diff options
54 files changed, 734 insertions, 588 deletions
@@ -27,13 +27,14 @@ interp/symbols.cmi: lib/bignat.cmi pretyping/classops.cmi \ interp/syntax_def.cmi: kernel/names.cmi pretyping/rawterm.cmi \ interp/topconstr.cmi lib/util.cmi interp/topconstr.cmi: lib/bignat.cmi lib/dyn.cmi pretyping/evd.cmi \ - library/libnames.cmi kernel/names.cmi lib/pp.cmi pretyping/rawterm.cmi \ - kernel/term.cmi lib/util.cmi + library/libnames.cmi kernel/mod_subst.cmi kernel/names.cmi lib/pp.cmi \ + pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi kernel/cbytecodes.cmi: kernel/names.cmi kernel/term.cmi kernel/cbytegen.cmi: kernel/cbytecodes.cmi kernel/cemitcodes.cmi \ kernel/declarations.cmi kernel/environ.cmi kernel/names.cmi \ kernel/term.cmi -kernel/cemitcodes.cmi: kernel/cbytecodes.cmi kernel/names.cmi +kernel/cemitcodes.cmi: kernel/cbytecodes.cmi kernel/mod_subst.cmi \ + kernel/names.cmi kernel/closure.cmi: kernel/environ.cmi kernel/esubst.cmi kernel/names.cmi \ lib/pp.cmi kernel/term.cmi kernel/conv_oracle.cmi: kernel/names.cmi @@ -41,8 +42,8 @@ kernel/cooking.cmi: kernel/declarations.cmi kernel/environ.cmi \ kernel/names.cmi kernel/term.cmi kernel/univ.cmi kernel/csymtable.cmi: kernel/environ.cmi kernel/names.cmi kernel/term.cmi kernel/declarations.cmi: kernel/cbytecodes.cmi kernel/cemitcodes.cmi \ - kernel/names.cmi lib/rtree.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/univ.cmi + kernel/mod_subst.cmi kernel/names.cmi lib/rtree.cmi kernel/sign.cmi \ + kernel/term.cmi kernel/univ.cmi kernel/entries.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 \ @@ -53,10 +54,12 @@ kernel/indtypes.cmi: kernel/declarations.cmi kernel/entries.cmi \ kernel/univ.cmi kernel/inductive.cmi: kernel/declarations.cmi kernel/environ.cmi \ kernel/names.cmi kernel/term.cmi kernel/univ.cmi +kernel/modops.cmi: kernel/declarations.cmi kernel/entries.cmi \ + kernel/environ.cmi kernel/mod_subst.cmi kernel/names.cmi kernel/univ.cmi \ + lib/util.cmi +kernel/mod_subst.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \ kernel/environ.cmi -kernel/modops.cmi: kernel/declarations.cmi kernel/entries.cmi \ - kernel/environ.cmi kernel/names.cmi kernel/univ.cmi lib/util.cmi kernel/names.cmi: lib/pp.cmi lib/predicate.cmi kernel/reduction.cmi: kernel/environ.cmi kernel/sign.cmi kernel/term.cmi \ kernel/univ.cmi @@ -75,14 +78,11 @@ kernel/typeops.cmi: kernel/entries.cmi kernel/environ.cmi kernel/names.cmi \ kernel/sign.cmi kernel/term.cmi kernel/univ.cmi kernel/univ.cmi: kernel/names.cmi lib/pp.cmi kernel/vconv.cmi: kernel/environ.cmi kernel/names.cmi kernel/reduction.cmi \ - kernel/term.cmi + kernel/term.cmi kernel/vm.cmi kernel/vm.cmi: kernel/cbytecodes.cmi kernel/cemitcodes.cmi kernel/names.cmi \ kernel/term.cmi lib/bignat.cmi: lib/pp.cmi lib/pp.cmi: lib/pp_control.cmi -lib/rtree.cmi: lib/pp.cmi -lib/system.cmi: lib/pp.cmi -lib/util.cmi: lib/compat.cmo lib/pp.cmi library/declare.cmi: kernel/cooking.cmi library/decl_kinds.cmo \ kernel/declarations.cmi library/dischargedhypsmap.cmi kernel/entries.cmi \ kernel/indtypes.cmi library/libnames.cmi library/libobject.cmi \ @@ -97,34 +97,39 @@ library/global.cmi: kernel/declarations.cmi kernel/entries.cmi \ kernel/environ.cmi kernel/indtypes.cmi library/libnames.cmi \ kernel/names.cmi kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi \ kernel/univ.cmi -library/goptions.cmi: library/libnames.cmi kernel/names.cmi \ - library/nametab.cmi lib/pp.cmi kernel/term.cmi lib/util.cmi +library/goptions.cmi: library/libnames.cmi kernel/mod_subst.cmi \ + kernel/names.cmi library/nametab.cmi lib/pp.cmi kernel/term.cmi \ + lib/util.cmi library/impargs.cmi: kernel/environ.cmi library/libnames.cmi kernel/names.cmi \ library/nametab.cmi kernel/term.cmi interp/topconstr.cmi -library/lib.cmi: library/libnames.cmi library/libobject.cmi kernel/names.cmi \ - library/summary.cmi lib/util.cmi -library/libnames.cmi: kernel/names.cmi lib/pp.cmi lib/predicate.cmi \ - kernel/term.cmi lib/util.cmi -library/libobject.cmi: library/libnames.cmi kernel/names.cmi +library/lib.cmi: library/libnames.cmi library/libobject.cmi \ + kernel/mod_subst.cmi kernel/names.cmi library/summary.cmi lib/util.cmi +library/libnames.cmi: kernel/mod_subst.cmi kernel/names.cmi lib/pp.cmi \ + lib/predicate.cmi kernel/term.cmi lib/util.cmi +library/libobject.cmi: library/libnames.cmi kernel/mod_subst.cmi \ + kernel/names.cmi library/library.cmi: library/libnames.cmi library/libobject.cmi \ kernel/names.cmi lib/pp.cmi lib/system.cmi lib/util.cmi library/nameops.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi library/nametab.cmi: library/libnames.cmi kernel/names.cmi lib/pp.cmi \ lib/util.cmi +lib/rtree.cmi: lib/pp.cmi +lib/system.cmi: lib/pp.cmi +lib/util.cmi: lib/compat.cmo lib/pp.cmi parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi interp/genarg.cmi \ - library/libnames.cmi kernel/names.cmi lib/pp.cmi interp/topconstr.cmi \ - lib/util.cmi -parsing/coqast.cmi: lib/dyn.cmi library/libnames.cmi kernel/names.cmi \ - lib/util.cmi + library/libnames.cmi kernel/mod_subst.cmi kernel/names.cmi lib/pp.cmi \ + interp/topconstr.cmi lib/util.cmi +parsing/coqast.cmi: lib/dyn.cmi library/libnames.cmi kernel/mod_subst.cmi \ + kernel/names.cmi lib/util.cmi parsing/egrammar.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \ - interp/genarg.cmi kernel/names.cmi pretyping/rawterm.cmi \ - proofs/tacexpr.cmo interp/topconstr.cmi lib/util.cmi \ - toplevel/vernacexpr.cmo + interp/genarg.cmi kernel/mod_subst.cmi kernel/names.cmi \ + pretyping/rawterm.cmi proofs/tacexpr.cmo interp/topconstr.cmi \ + lib/util.cmi toplevel/vernacexpr.cmo parsing/esyntax.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \ lib/pp.cmi interp/ppextend.cmi interp/symbols.cmi interp/topconstr.cmi parsing/extend.cmi: parsing/ast.cmi parsing/coqast.cmi interp/genarg.cmi \ - kernel/names.cmi lib/pp.cmi interp/ppextend.cmi interp/topconstr.cmi \ - lib/util.cmi + kernel/mod_subst.cmi kernel/names.cmi lib/pp.cmi interp/ppextend.cmi \ + interp/topconstr.cmi lib/util.cmi parsing/g_minicoq.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ kernel/term.cmi parsing/lexer.cmi: lib/pp.cmi lib/util.cmi @@ -166,10 +171,11 @@ pretyping/cbv.cmi: kernel/closure.cmi kernel/environ.cmi kernel/esubst.cmi \ kernel/names.cmi kernel/term.cmi pretyping/classops.cmi: library/decl_kinds.cmo kernel/environ.cmi \ pretyping/evd.cmi library/libnames.cmi library/libobject.cmi \ - kernel/names.cmi library/nametab.cmi lib/pp.cmi kernel/term.cmi + kernel/mod_subst.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ + kernel/term.cmi pretyping/clenv.cmi: kernel/environ.cmi pretyping/evarutil.cmi \ - pretyping/evd.cmi kernel/names.cmi lib/pp.cmi pretyping/rawterm.cmi \ - kernel/sign.cmi kernel/term.cmi lib/util.cmi + pretyping/evd.cmi kernel/mod_subst.cmi kernel/names.cmi lib/pp.cmi \ + pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi lib/util.cmi pretyping/coercion.cmi: kernel/environ.cmi pretyping/evarutil.cmi \ pretyping/evd.cmi kernel/names.cmi pretyping/rawterm.cmi kernel/sign.cmi \ kernel/term.cmi lib/util.cmi @@ -181,9 +187,9 @@ pretyping/evarconv.cmi: kernel/environ.cmi pretyping/evd.cmi \ pretyping/evarutil.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \ pretyping/rawterm.cmi pretyping/reductionops.cmi kernel/sign.cmi \ kernel/term.cmi pretyping/termops.cmi lib/util.cmi -pretyping/evd.cmi: kernel/environ.cmi library/libnames.cmi kernel/names.cmi \ - lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \ - lib/util.cmi +pretyping/evd.cmi: kernel/environ.cmi library/libnames.cmi \ + kernel/mod_subst.cmi kernel/names.cmi lib/pp.cmi kernel/reduction.cmi \ + kernel/sign.cmi kernel/term.cmi lib/util.cmi pretyping/indrec.cmi: kernel/declarations.cmi kernel/environ.cmi \ pretyping/evd.cmi pretyping/inductiveops.cmi kernel/names.cmi \ kernel/term.cmi @@ -192,8 +198,8 @@ pretyping/inductiveops.cmi: kernel/declarations.cmi kernel/environ.cmi \ pretyping/matching.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \ pretyping/pattern.cmi kernel/term.cmi pretyping/termops.cmi pretyping/pattern.cmi: kernel/environ.cmi library/libnames.cmi \ - kernel/names.cmi library/nametab.cmi lib/pp.cmi pretyping/rawterm.cmi \ - kernel/sign.cmi kernel/term.cmi + kernel/mod_subst.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ + pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi pretyping/pretype_errors.cmi: kernel/environ.cmi pretyping/evd.cmi \ pretyping/inductiveops.cmi kernel/names.cmi lib/pp.cmi \ pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi lib/util.cmi @@ -201,8 +207,8 @@ pretyping/pretyping.cmi: lib/dyn.cmi kernel/environ.cmi \ pretyping/evarutil.cmi pretyping/evd.cmi kernel/names.cmi \ pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi pretyping/rawterm.cmi: lib/dyn.cmi pretyping/evd.cmi library/libnames.cmi \ - kernel/names.cmi library/nametab.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/univ.cmi lib/util.cmi + kernel/mod_subst.cmi kernel/names.cmi library/nametab.cmi kernel/sign.cmi \ + kernel/term.cmi kernel/univ.cmi lib/util.cmi pretyping/recordops.cmi: pretyping/classops.cmi library/libnames.cmi \ library/libobject.cmi library/library.cmi kernel/names.cmi \ library/nametab.cmi kernel/term.cmi @@ -249,8 +255,8 @@ proofs/tactic_debug.cmi: kernel/environ.cmi pretyping/evd.cmi \ kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi \ proofs/tacexpr.cmo kernel/term.cmi tactics/auto.cmi: tactics/btermdn.cmi pretyping/clenv.cmi kernel/environ.cmi \ - pretyping/evd.cmi library/libnames.cmi kernel/names.cmi \ - pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi \ + pretyping/evd.cmi library/libnames.cmi kernel/mod_subst.cmi \ + kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi \ pretyping/rawterm.cmi kernel/sign.cmi proofs/tacexpr.cmo \ proofs/tacmach.cmi kernel/term.cmi lib/util.cmi toplevel/vernacexpr.cmo tactics/autorewrite.cmi: proofs/tacexpr.cmo proofs/tacmach.cmi \ @@ -293,10 +299,10 @@ tactics/refine.cmi: pretyping/evd.cmi proofs/tacmach.cmi tactics/setoid_replace.cmi: kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi \ kernel/term.cmi interp/topconstr.cmi tactics/tacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/environ.cmi \ - pretyping/evd.cmi interp/genarg.cmi kernel/names.cmi library/nametab.cmi \ - lib/pp.cmi proofs/proof_type.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \ - pretyping/tacred.cmi proofs/tactic_debug.cmi kernel/term.cmi \ - interp/topconstr.cmi lib/util.cmi + pretyping/evd.cmi interp/genarg.cmi kernel/mod_subst.cmi kernel/names.cmi \ + library/nametab.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacexpr.cmo \ + proofs/tacmach.cmi pretyping/tacred.cmi proofs/tactic_debug.cmi \ + kernel/term.cmi interp/topconstr.cmi lib/util.cmi tactics/tacticals.cmi: pretyping/clenv.cmi interp/genarg.cmi kernel/names.cmi \ pretyping/pattern.cmi proofs/proof_type.cmi kernel/reduction.cmi \ kernel/sign.cmi proofs/tacexpr.cmo proofs/tacmach.cmi kernel/term.cmi @@ -337,11 +343,11 @@ toplevel/recordobj.cmi: library/libnames.cmi proofs/tacexpr.cmo 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/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \ library/libnames.cmi kernel/names.cmi kernel/term.cmi \ interp/topconstr.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernacinterp.cmi: proofs/tacexpr.cmo +toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo translate/ppconstrnew.cmi: parsing/coqast.cmi kernel/environ.cmi \ parsing/extend.cmi interp/genarg.cmi library/libnames.cmi \ kernel/names.cmi pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi \ @@ -361,9 +367,9 @@ contrib/cc/ccalgo.cmi: kernel/names.cmi kernel/term.cmi contrib/cc/ccproof.cmi: contrib/cc/ccalgo.cmi kernel/names.cmi contrib/correctness/past.cmi: kernel/names.cmi kernel/term.cmi \ interp/topconstr.cmi lib/util.cmi -contrib/correctness/pcic.cmi: pretyping/rawterm.cmi contrib/correctness/pcicenv.cmi: kernel/names.cmi kernel/sign.cmi \ kernel/term.cmi +contrib/correctness/pcic.cmi: pretyping/rawterm.cmi contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi contrib/correctness/penv.cmi: library/libnames.cmi kernel/names.cmi \ @@ -397,7 +403,8 @@ contrib/extraction/mlutil.cmi: library/libnames.cmi \ contrib/extraction/miniml.cmi kernel/names.cmi kernel/term.cmi \ lib/util.cmi contrib/extraction/modutil.cmi: kernel/declarations.cmi kernel/environ.cmi \ - library/libnames.cmi contrib/extraction/miniml.cmi kernel/names.cmi + library/libnames.cmi contrib/extraction/miniml.cmi kernel/mod_subst.cmi \ + kernel/names.cmi contrib/extraction/ocaml.cmi: library/libnames.cmi \ contrib/extraction/miniml.cmi kernel/names.cmi lib/pp.cmi contrib/extraction/scheme.cmi: contrib/extraction/miniml.cmi kernel/names.cmi \ @@ -473,7 +480,7 @@ dev/top_printers.cmo: parsing/ast.cmi kernel/cbytecodes.cmi \ parsing/pptactic.cmi parsing/printer.cmi proofs/proof_trees.cmi \ proofs/refiner.cmi kernel/sign.cmi lib/system.cmi proofs/tacmach.cmi \ parsing/tactic_printer.cmi kernel/term.cmi pretyping/termops.cmi \ - kernel/univ.cmi + kernel/univ.cmi kernel/vm.cmi dev/top_printers.cmx: parsing/ast.cmx kernel/cbytecodes.cmx \ kernel/cemitcodes.cmx toplevel/cerrors.cmx pretyping/clenv.cmx \ kernel/closure.cmx interp/constrextern.cmx kernel/declarations.cmx \ @@ -482,7 +489,7 @@ dev/top_printers.cmx: parsing/ast.cmx kernel/cbytecodes.cmx \ parsing/pptactic.cmx parsing/printer.cmx proofs/proof_trees.cmx \ proofs/refiner.cmx kernel/sign.cmx lib/system.cmx proofs/tacmach.cmx \ parsing/tactic_printer.cmx kernel/term.cmx pretyping/termops.cmx \ - kernel/univ.cmx + kernel/univ.cmx kernel/vm.cmx doc/parse.cmo: parsing/ast.cmi doc/parse.cmx: parsing/ast.cmx ide/blaster_window.cmo: ide/coq.cmi ide/ideutils.cmi @@ -495,6 +502,14 @@ ide/config_lexer.cmo: ide/config_parser.cmi lib/util.cmi ide/config_lexer.cmx: ide/config_parser.cmx lib/util.cmx ide/config_parser.cmo: lib/util.cmi ide/config_parser.cmi ide/config_parser.cmx: lib/util.cmx ide/config_parser.cmi +ide/coqide.cmo: ide/blaster_window.cmo ide/command_windows.cmi ide/coq.cmi \ + ide/coq_commands.cmo ide/find_phrase.cmo ide/highlight.cmo \ + ide/ideutils.cmi proofs/pfedit.cmi ide/preferences.cmi lib/system.cmi \ + ide/undo.cmi lib/util.cmi toplevel/vernacexpr.cmo ide/coqide.cmi +ide/coqide.cmx: ide/blaster_window.cmx ide/command_windows.cmx ide/coq.cmx \ + ide/coq_commands.cmx ide/find_phrase.cmx ide/highlight.cmx \ + ide/ideutils.cmx proofs/pfedit.cmx ide/preferences.cmx lib/system.cmx \ + ide/undo.cmx lib/util.cmx toplevel/vernacexpr.cmx ide/coqide.cmi ide/coq.cmo: toplevel/cerrors.cmi config/coq_config.cmi toplevel/coqtop.cmi \ kernel/declarations.cmi kernel/environ.cmi pretyping/evarutil.cmi \ pretyping/evd.cmi library/global.cmi tactics/hipattern.cmi \ @@ -517,14 +532,6 @@ ide/coq.cmx: toplevel/cerrors.cmx config/coq_config.cmx toplevel/coqtop.cmx \ toplevel/vernacentries.cmx toplevel/vernacexpr.cmx ide/coq.cmi ide/coq_tactics.cmo: ide/coq_tactics.cmi ide/coq_tactics.cmx: ide/coq_tactics.cmi -ide/coqide.cmo: ide/blaster_window.cmo ide/command_windows.cmi ide/coq.cmi \ - ide/coq_commands.cmo ide/find_phrase.cmo ide/highlight.cmo \ - ide/ideutils.cmi proofs/pfedit.cmi ide/preferences.cmi lib/system.cmi \ - ide/undo.cmi lib/util.cmi toplevel/vernacexpr.cmo ide/coqide.cmi -ide/coqide.cmx: ide/blaster_window.cmx ide/command_windows.cmx ide/coq.cmx \ - ide/coq_commands.cmx ide/find_phrase.cmx ide/highlight.cmx \ - ide/ideutils.cmx proofs/pfedit.cmx ide/preferences.cmx lib/system.cmx \ - ide/undo.cmx lib/util.cmx toplevel/vernacexpr.cmx ide/coqide.cmi ide/find_phrase.cmo: ide/ideutils.cmi ide/find_phrase.cmx: ide/ideutils.cmx ide/highlight.cmo: ide/ideutils.cmi @@ -630,25 +637,27 @@ interp/syntax_def.cmx: library/lib.cmx library/libnames.cmx \ library/nametab.cmx lib/pp.cmx library/summary.cmx interp/symbols.cmx \ interp/topconstr.cmx lib/util.cmx interp/syntax_def.cmi interp/topconstr.cmo: lib/bignat.cmi lib/dyn.cmi pretyping/evd.cmi \ - library/libnames.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \ - lib/pp.cmi pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi \ - interp/topconstr.cmi + library/libnames.cmi kernel/mod_subst.cmi library/nameops.cmi \ + kernel/names.cmi lib/options.cmi lib/pp.cmi pretyping/rawterm.cmi \ + kernel/term.cmi lib/util.cmi interp/topconstr.cmi interp/topconstr.cmx: lib/bignat.cmx lib/dyn.cmx pretyping/evd.cmx \ - library/libnames.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \ - lib/pp.cmx pretyping/rawterm.cmx kernel/term.cmx lib/util.cmx \ - interp/topconstr.cmi + library/libnames.cmx kernel/mod_subst.cmx library/nameops.cmx \ + kernel/names.cmx lib/options.cmx lib/pp.cmx pretyping/rawterm.cmx \ + kernel/term.cmx lib/util.cmx interp/topconstr.cmi kernel/cbytecodes.cmo: kernel/names.cmi kernel/term.cmi kernel/cbytecodes.cmi kernel/cbytecodes.cmx: kernel/names.cmx kernel/term.cmx kernel/cbytecodes.cmi kernel/cbytegen.cmo: kernel/cbytecodes.cmi kernel/cemitcodes.cmi \ kernel/declarations.cmi kernel/environ.cmi kernel/names.cmi \ - kernel/term.cmi lib/util.cmi kernel/cbytegen.cmi + lib/options.cmi kernel/term.cmi lib/util.cmi kernel/cbytegen.cmi kernel/cbytegen.cmx: kernel/cbytecodes.cmx kernel/cemitcodes.cmx \ kernel/declarations.cmx kernel/environ.cmx kernel/names.cmx \ - kernel/term.cmx lib/util.cmx kernel/cbytegen.cmi + lib/options.cmx kernel/term.cmx lib/util.cmx kernel/cbytegen.cmi kernel/cemitcodes.cmo: kernel/cbytecodes.cmi kernel/copcodes.cmo \ - kernel/names.cmi kernel/term.cmi kernel/cemitcodes.cmi + kernel/mod_subst.cmi kernel/names.cmi kernel/term.cmi \ + kernel/cemitcodes.cmi kernel/cemitcodes.cmx: kernel/cbytecodes.cmx kernel/copcodes.cmx \ - kernel/names.cmx kernel/term.cmx kernel/cemitcodes.cmi + kernel/mod_subst.cmx kernel/names.cmx kernel/term.cmx \ + kernel/cemitcodes.cmi kernel/closure.cmo: kernel/declarations.cmi kernel/environ.cmi \ kernel/esubst.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \ lib/util.cmi kernel/closure.cmi @@ -670,11 +679,11 @@ kernel/csymtable.cmx: kernel/cbytecodes.cmx kernel/cbytegen.cmx \ kernel/cemitcodes.cmx kernel/declarations.cmx kernel/environ.cmx \ kernel/names.cmx kernel/term.cmx kernel/vm.cmx kernel/csymtable.cmi kernel/declarations.cmo: kernel/cbytecodes.cmi kernel/cemitcodes.cmi \ - kernel/names.cmi lib/rtree.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/univ.cmi lib/util.cmi kernel/declarations.cmi + kernel/mod_subst.cmi kernel/names.cmi lib/rtree.cmi kernel/sign.cmi \ + kernel/term.cmi kernel/univ.cmi lib/util.cmi kernel/declarations.cmi kernel/declarations.cmx: kernel/cbytecodes.cmx kernel/cemitcodes.cmx \ - kernel/names.cmx lib/rtree.cmx kernel/sign.cmx kernel/term.cmx \ - kernel/univ.cmx lib/util.cmx kernel/declarations.cmi + kernel/mod_subst.cmx kernel/names.cmx lib/rtree.cmx kernel/sign.cmx \ + kernel/term.cmx kernel/univ.cmx lib/util.cmx kernel/declarations.cmi kernel/entries.cmo: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \ kernel/univ.cmi kernel/entries.cmi kernel/entries.cmx: kernel/names.cmx kernel/sign.cmx kernel/term.cmx \ @@ -699,20 +708,26 @@ kernel/inductive.cmo: kernel/declarations.cmi kernel/environ.cmi \ kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \ kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \ kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx kernel/inductive.cmi -kernel/mod_typing.cmo: kernel/declarations.cmi kernel/entries.cmi \ - kernel/environ.cmi kernel/modops.cmi kernel/names.cmi \ - kernel/reduction.cmi kernel/subtyping.cmi kernel/term_typing.cmi \ - kernel/typeops.cmi kernel/univ.cmi lib/util.cmi kernel/mod_typing.cmi -kernel/mod_typing.cmx: kernel/declarations.cmx kernel/entries.cmx \ - kernel/environ.cmx kernel/modops.cmx kernel/names.cmx \ - kernel/reduction.cmx kernel/subtyping.cmx kernel/term_typing.cmx \ - kernel/typeops.cmx kernel/univ.cmx lib/util.cmx kernel/mod_typing.cmi kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \ - kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \ - kernel/univ.cmi lib/util.cmi kernel/modops.cmi + kernel/environ.cmi kernel/mod_subst.cmi kernel/names.cmi lib/pp.cmi \ + kernel/term.cmi kernel/univ.cmi lib/util.cmi kernel/modops.cmi kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \ - kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \ - kernel/univ.cmx lib/util.cmx kernel/modops.cmi + kernel/environ.cmx kernel/mod_subst.cmx kernel/names.cmx lib/pp.cmx \ + kernel/term.cmx kernel/univ.cmx lib/util.cmx kernel/modops.cmi +kernel/mod_subst.cmo: kernel/names.cmi lib/pp.cmi kernel/term.cmi \ + lib/util.cmi kernel/mod_subst.cmi +kernel/mod_subst.cmx: kernel/names.cmx lib/pp.cmx kernel/term.cmx \ + lib/util.cmx kernel/mod_subst.cmi +kernel/mod_typing.cmo: kernel/declarations.cmi kernel/entries.cmi \ + kernel/environ.cmi kernel/mod_subst.cmi kernel/modops.cmi \ + kernel/names.cmi kernel/reduction.cmi kernel/subtyping.cmi \ + kernel/term_typing.cmi kernel/typeops.cmi kernel/univ.cmi lib/util.cmi \ + kernel/mod_typing.cmi +kernel/mod_typing.cmx: kernel/declarations.cmx kernel/entries.cmx \ + kernel/environ.cmx kernel/mod_subst.cmx kernel/modops.cmx \ + kernel/names.cmx kernel/reduction.cmx kernel/subtyping.cmx \ + kernel/term_typing.cmx kernel/typeops.cmx kernel/univ.cmx lib/util.cmx \ + kernel/mod_typing.cmi kernel/names.cmo: lib/hashcons.cmi lib/options.cmi lib/pp.cmi \ lib/predicate.cmi lib/util.cmi kernel/names.cmi kernel/names.cmx: lib/hashcons.cmx lib/options.cmx lib/pp.cmx \ @@ -744,13 +759,13 @@ kernel/sign.cmo: kernel/names.cmi kernel/term.cmi lib/util.cmi \ kernel/sign.cmx: kernel/names.cmx kernel/term.cmx lib/util.cmx \ kernel/sign.cmi kernel/subtyping.cmo: kernel/declarations.cmi kernel/environ.cmi \ - kernel/inductive.cmi kernel/modops.cmi kernel/names.cmi \ - kernel/reduction.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \ - kernel/subtyping.cmi + kernel/inductive.cmi kernel/mod_subst.cmi kernel/modops.cmi \ + kernel/names.cmi kernel/reduction.cmi kernel/term.cmi kernel/univ.cmi \ + lib/util.cmi kernel/subtyping.cmi kernel/subtyping.cmx: kernel/declarations.cmx kernel/environ.cmx \ - kernel/inductive.cmx kernel/modops.cmx kernel/names.cmx \ - kernel/reduction.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \ - kernel/subtyping.cmi + kernel/inductive.cmx kernel/mod_subst.cmx kernel/modops.cmx \ + kernel/names.cmx kernel/reduction.cmx kernel/term.cmx kernel/univ.cmx \ + lib/util.cmx kernel/subtyping.cmi kernel/term.cmo: kernel/esubst.cmi lib/hashcons.cmi kernel/names.cmi \ lib/pp.cmi kernel/univ.cmi lib/util.cmi kernel/term.cmi kernel/term.cmx: kernel/esubst.cmx lib/hashcons.cmx kernel/names.cmx \ @@ -809,10 +824,10 @@ 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/explore.cmo: lib/explore.cmi lib/explore.cmx: lib/explore.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/gmap.cmo: lib/gmap.cmi +lib/gmap.cmx: lib/gmap.cmi lib/gset.cmo: lib/gset.cmi lib/gset.cmx: lib/gset.cmi lib/hashcons.cmo: lib/hashcons.cmi @@ -821,24 +836,14 @@ lib/heap.cmo: lib/heap.cmi lib/heap.cmx: lib/heap.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/pp.cmo: lib/pp_control.cmi lib/pp.cmi +lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi lib/predicate.cmo: lib/predicate.cmi lib/predicate.cmx: lib/predicate.cmi lib/profile.cmo: lib/profile.cmi lib/profile.cmx: lib/profile.cmi -lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi -lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi -lib/stamps.cmo: lib/stamps.cmi -lib/stamps.cmx: lib/stamps.cmi -lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi -lib/system.cmx: config/coq_config.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/compat.cmo lib/pp.cmi lib/util.cmi -lib/util.cmx: lib/compat.cmx lib/pp.cmx lib/util.cmi library/declare.cmo: library/decl_kinds.cmo kernel/declarations.cmi \ library/dischargedhypsmap.cmi kernel/entries.cmi kernel/environ.cmi \ library/global.cmi library/impargs.cmi kernel/indtypes.cmi \ @@ -859,16 +864,16 @@ library/declare.cmx: library/decl_kinds.cmx kernel/declarations.cmx \ kernel/typeops.cmx kernel/univ.cmx lib/util.cmx library/declare.cmi library/declaremods.cmo: kernel/declarations.cmi kernel/entries.cmi \ kernel/environ.cmi library/global.cmi library/lib.cmi \ - library/libnames.cmi library/libobject.cmi kernel/mod_typing.cmi \ - kernel/modops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ - kernel/subtyping.cmi library/summary.cmi lib/util.cmi \ - library/declaremods.cmi + library/libnames.cmi library/libobject.cmi kernel/mod_subst.cmi \ + kernel/mod_typing.cmi kernel/modops.cmi kernel/names.cmi \ + library/nametab.cmi lib/pp.cmi kernel/subtyping.cmi library/summary.cmi \ + lib/util.cmi library/declaremods.cmi library/declaremods.cmx: kernel/declarations.cmx kernel/entries.cmx \ kernel/environ.cmx library/global.cmx library/lib.cmx \ - library/libnames.cmx library/libobject.cmx kernel/mod_typing.cmx \ - kernel/modops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ - kernel/subtyping.cmx library/summary.cmx lib/util.cmx \ - library/declaremods.cmi + library/libnames.cmx library/libobject.cmx kernel/mod_subst.cmx \ + kernel/mod_typing.cmx kernel/modops.cmx kernel/names.cmx \ + library/nametab.cmx lib/pp.cmx kernel/subtyping.cmx library/summary.cmx \ + lib/util.cmx library/declaremods.cmi library/dischargedhypsmap.cmo: kernel/declarations.cmi kernel/environ.cmi \ kernel/inductive.cmi library/lib.cmi library/libnames.cmi \ library/libobject.cmi kernel/names.cmi library/nametab.cmi \ @@ -888,11 +893,13 @@ library/global.cmx: kernel/environ.cmx kernel/inductive.cmx \ kernel/sign.cmx library/summary.cmx kernel/term.cmx lib/util.cmx \ library/global.cmi library/goptions.cmo: library/lib.cmi library/libnames.cmi \ - library/libobject.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ - library/summary.cmi kernel/term.cmi lib/util.cmi library/goptions.cmi + library/libobject.cmi kernel/mod_subst.cmi kernel/names.cmi \ + library/nametab.cmi lib/pp.cmi library/summary.cmi kernel/term.cmi \ + lib/util.cmi library/goptions.cmi library/goptions.cmx: library/lib.cmx library/libnames.cmx \ - library/libobject.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ - library/summary.cmx kernel/term.cmx lib/util.cmx library/goptions.cmi + library/libobject.cmx kernel/mod_subst.cmx kernel/names.cmx \ + library/nametab.cmx lib/pp.cmx library/summary.cmx kernel/term.cmx \ + lib/util.cmx library/goptions.cmi library/impargs.cmo: kernel/declarations.cmi kernel/environ.cmi \ library/global.cmi kernel/inductive.cmi library/lib.cmi \ library/libnames.cmi library/libobject.cmi kernel/names.cmi \ @@ -911,14 +918,16 @@ library/lib.cmo: library/libnames.cmi library/libobject.cmi \ library/lib.cmx: library/libnames.cmx library/libobject.cmx \ library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ lib/pp.cmx library/summary.cmx lib/util.cmx library/lib.cmi -library/libnames.cmo: library/nameops.cmi kernel/names.cmi lib/pp.cmi \ - lib/predicate.cmi kernel/term.cmi lib/util.cmi library/libnames.cmi -library/libnames.cmx: library/nameops.cmx kernel/names.cmx lib/pp.cmx \ - lib/predicate.cmx kernel/term.cmx lib/util.cmx library/libnames.cmi -library/libobject.cmo: lib/dyn.cmi library/libnames.cmi kernel/names.cmi \ - lib/util.cmi library/libobject.cmi -library/libobject.cmx: lib/dyn.cmx library/libnames.cmx kernel/names.cmx \ - lib/util.cmx library/libobject.cmi +library/libnames.cmo: kernel/mod_subst.cmi library/nameops.cmi \ + kernel/names.cmi lib/pp.cmi lib/predicate.cmi kernel/term.cmi \ + lib/util.cmi library/libnames.cmi +library/libnames.cmx: kernel/mod_subst.cmx library/nameops.cmx \ + kernel/names.cmx lib/pp.cmx lib/predicate.cmx kernel/term.cmx \ + lib/util.cmx library/libnames.cmi +library/libobject.cmo: lib/dyn.cmi library/libnames.cmi kernel/mod_subst.cmi \ + kernel/names.cmi lib/util.cmi library/libobject.cmi +library/libobject.cmx: lib/dyn.cmx library/libnames.cmx kernel/mod_subst.cmx \ + kernel/names.cmx lib/util.cmx library/libobject.cmi library/library.cmo: library/declaremods.cmi library/lib.cmi \ library/libnames.cmi library/libobject.cmi library/nameops.cmi \ kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \ @@ -945,6 +954,16 @@ library/states.cmx: library/lib.cmx library/library.cmx library/summary.cmx \ lib/system.cmx library/states.cmi library/summary.cmo: lib/dyn.cmi lib/pp.cmi lib/util.cmi library/summary.cmi library/summary.cmx: lib/dyn.cmx lib/pp.cmx lib/util.cmx library/summary.cmi +lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi +lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi +lib/stamps.cmo: lib/stamps.cmi +lib/stamps.cmx: lib/stamps.cmi +lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi +lib/system.cmx: config/coq_config.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/compat.cmo lib/pp.cmi lib/util.cmi +lib/util.cmx: lib/compat.cmx lib/pp.cmx lib/util.cmi parsing/argextend.cmo: parsing/ast.cmi interp/genarg.cmi parsing/pcoq.cmi \ parsing/q_coqast.cmo parsing/q_util.cmi lib/util.cmi \ toplevel/vernacexpr.cmo @@ -958,9 +977,9 @@ parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx interp/genarg.cmx \ library/libnames.cmx kernel/names.cmx lib/pp.cmx interp/topconstr.cmx \ lib/util.cmx parsing/ast.cmi parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi library/libnames.cmi \ - kernel/names.cmi lib/util.cmi parsing/coqast.cmi + kernel/mod_subst.cmi kernel/names.cmi lib/util.cmi parsing/coqast.cmi parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx library/libnames.cmx \ - kernel/names.cmx lib/util.cmx parsing/coqast.cmi + kernel/mod_subst.cmx kernel/names.cmx lib/util.cmx parsing/coqast.cmi parsing/egrammar.cmo: parsing/ast.cmi lib/bignat.cmi parsing/extend.cmi \ interp/genarg.cmi parsing/lexer.cmi library/libnames.cmi \ library/nameops.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \ @@ -1156,13 +1175,13 @@ parsing/ppconstr.cmo: parsing/ast.cmi lib/bignat.cmi interp/constrextern.cmi \ library/libnames.cmi library/nameops.cmi kernel/names.cmi \ library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi interp/ppextend.cmi \ pretyping/rawterm.cmi interp/symbols.cmi kernel/term.cmi \ - interp/topconstr.cmi lib/util.cmi parsing/ppconstr.cmi + interp/topconstr.cmi kernel/univ.cmi lib/util.cmi parsing/ppconstr.cmi parsing/ppconstr.cmx: parsing/ast.cmx lib/bignat.cmx interp/constrextern.cmx \ parsing/coqast.cmx pretyping/evd.cmx interp/genarg.cmx \ library/libnames.cmx library/nameops.cmx kernel/names.cmx \ library/nametab.cmx pretyping/pattern.cmx lib/pp.cmx interp/ppextend.cmx \ pretyping/rawterm.cmx interp/symbols.cmx kernel/term.cmx \ - interp/topconstr.cmx lib/util.cmx parsing/ppconstr.cmi + interp/topconstr.cmx kernel/univ.cmx lib/util.cmx parsing/ppconstr.cmi parsing/pptactic.cmo: kernel/closure.cmi interp/constrextern.cmi lib/dyn.cmi \ parsing/extend.cmi interp/genarg.cmi library/libnames.cmi \ library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ @@ -1314,33 +1333,35 @@ pretyping/cbv.cmx: kernel/closure.cmx kernel/conv_oracle.cmx \ pretyping/classops.cmo: library/decl_kinds.cmo kernel/environ.cmi \ pretyping/evd.cmi library/global.cmi lib/gmap.cmi library/goptions.cmi \ library/lib.cmi library/libnames.cmi library/libobject.cmi \ - library/library.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ - lib/pp.cmi pretyping/rawterm.cmi pretyping/reductionops.cmi \ - library/summary.cmi pretyping/tacred.cmi kernel/term.cmi \ - pretyping/termops.cmi lib/util.cmi pretyping/classops.cmi + library/library.cmi kernel/mod_subst.cmi kernel/names.cmi \ + library/nametab.cmi lib/options.cmi lib/pp.cmi pretyping/rawterm.cmi \ + pretyping/reductionops.cmi library/summary.cmi pretyping/tacred.cmi \ + kernel/term.cmi pretyping/termops.cmi lib/util.cmi pretyping/classops.cmi pretyping/classops.cmx: library/decl_kinds.cmx kernel/environ.cmx \ pretyping/evd.cmx library/global.cmx lib/gmap.cmx library/goptions.cmx \ library/lib.cmx library/libnames.cmx library/libobject.cmx \ - library/library.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ - lib/pp.cmx pretyping/rawterm.cmx pretyping/reductionops.cmx \ - library/summary.cmx pretyping/tacred.cmx kernel/term.cmx \ - pretyping/termops.cmx lib/util.cmx pretyping/classops.cmi + library/library.cmx kernel/mod_subst.cmx kernel/names.cmx \ + library/nametab.cmx lib/options.cmx lib/pp.cmx pretyping/rawterm.cmx \ + pretyping/reductionops.cmx library/summary.cmx pretyping/tacred.cmx \ + kernel/term.cmx pretyping/termops.cmx lib/util.cmx pretyping/classops.cmi pretyping/clenv.cmo: pretyping/coercion.cmi kernel/environ.cmi \ pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \ - library/nameops.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \ - pretyping/pretype_errors.cmi pretyping/rawterm.cmi kernel/reduction.cmi \ - pretyping/reductionops.cmi pretyping/retyping.cmi kernel/sign.cmi \ - proofs/tacexpr.cmo pretyping/tacred.cmi kernel/term.cmi \ - pretyping/termops.cmi pretyping/typing.cmi pretyping/unification.cmi \ - lib/util.cmi pretyping/clenv.cmi + kernel/mod_subst.cmi library/nameops.cmi kernel/names.cmi \ + pretyping/pattern.cmi lib/pp.cmi pretyping/pretype_errors.cmi \ + pretyping/rawterm.cmi kernel/reduction.cmi pretyping/reductionops.cmi \ + pretyping/retyping.cmi kernel/sign.cmi proofs/tacexpr.cmo \ + pretyping/tacred.cmi kernel/term.cmi pretyping/termops.cmi \ + pretyping/typing.cmi pretyping/unification.cmi lib/util.cmi \ + pretyping/clenv.cmi pretyping/clenv.cmx: pretyping/coercion.cmx kernel/environ.cmx \ pretyping/evarutil.cmx pretyping/evd.cmx library/global.cmx \ - library/nameops.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \ - pretyping/pretype_errors.cmx pretyping/rawterm.cmx kernel/reduction.cmx \ - pretyping/reductionops.cmx pretyping/retyping.cmx kernel/sign.cmx \ - proofs/tacexpr.cmx pretyping/tacred.cmx kernel/term.cmx \ - pretyping/termops.cmx pretyping/typing.cmx pretyping/unification.cmx \ - lib/util.cmx pretyping/clenv.cmi + kernel/mod_subst.cmx library/nameops.cmx kernel/names.cmx \ + pretyping/pattern.cmx lib/pp.cmx pretyping/pretype_errors.cmx \ + pretyping/rawterm.cmx kernel/reduction.cmx pretyping/reductionops.cmx \ + pretyping/retyping.cmx kernel/sign.cmx proofs/tacexpr.cmx \ + pretyping/tacred.cmx kernel/term.cmx pretyping/termops.cmx \ + pretyping/typing.cmx pretyping/unification.cmx lib/util.cmx \ + pretyping/clenv.cmi pretyping/coercion.cmo: pretyping/classops.cmi kernel/environ.cmi \ pretyping/evarconv.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ kernel/names.cmi pretyping/pretype_errors.cmi pretyping/rawterm.cmi \ @@ -1356,15 +1377,17 @@ pretyping/coercion.cmx: pretyping/classops.cmx kernel/environ.cmx \ pretyping/detyping.cmo: kernel/declarations.cmi kernel/environ.cmi \ pretyping/evd.cmi library/global.cmi library/goptions.cmi \ kernel/inductive.cmi pretyping/inductiveops.cmi library/libnames.cmi \ - library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ - lib/pp.cmi pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \ - pretyping/termops.cmi kernel/univ.cmi lib/util.cmi pretyping/detyping.cmi + kernel/mod_subst.cmi library/nameops.cmi kernel/names.cmi \ + library/nametab.cmi lib/options.cmi lib/pp.cmi pretyping/rawterm.cmi \ + kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi kernel/univ.cmi \ + lib/util.cmi pretyping/detyping.cmi pretyping/detyping.cmx: kernel/declarations.cmx kernel/environ.cmx \ pretyping/evd.cmx library/global.cmx library/goptions.cmx \ kernel/inductive.cmx pretyping/inductiveops.cmx library/libnames.cmx \ - library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ - lib/pp.cmx pretyping/rawterm.cmx kernel/sign.cmx kernel/term.cmx \ - pretyping/termops.cmx kernel/univ.cmx lib/util.cmx pretyping/detyping.cmi + kernel/mod_subst.cmx library/nameops.cmx kernel/names.cmx \ + library/nametab.cmx lib/options.cmx lib/pp.cmx pretyping/rawterm.cmx \ + kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx kernel/univ.cmx \ + lib/util.cmx pretyping/detyping.cmi pretyping/evarconv.cmo: pretyping/classops.cmi kernel/closure.cmi \ kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ library/libnames.cmi kernel/names.cmi pretyping/recordops.cmi \ @@ -1388,13 +1411,13 @@ pretyping/evarutil.cmx: kernel/environ.cmx pretyping/evd.cmx \ pretyping/termops.cmx kernel/type_errors.cmx kernel/typeops.cmx \ pretyping/typing.cmx kernel/univ.cmx lib/util.cmx pretyping/evarutil.cmi pretyping/evd.cmo: kernel/environ.cmi library/global.cmi library/libnames.cmi \ - library/nameops.cmi kernel/names.cmi lib/pp.cmi kernel/reduction.cmi \ - kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \ - pretyping/evd.cmi + kernel/mod_subst.cmi library/nameops.cmi kernel/names.cmi lib/pp.cmi \ + kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \ + pretyping/termops.cmi lib/util.cmi pretyping/evd.cmi pretyping/evd.cmx: kernel/environ.cmx library/global.cmx library/libnames.cmx \ - library/nameops.cmx kernel/names.cmx lib/pp.cmx kernel/reduction.cmx \ - kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ - pretyping/evd.cmi + kernel/mod_subst.cmx library/nameops.cmx kernel/names.cmx lib/pp.cmx \ + kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \ + pretyping/termops.cmx lib/util.cmx pretyping/evd.cmi pretyping/indrec.cmo: kernel/declarations.cmi kernel/entries.cmi \ kernel/environ.cmi library/global.cmi kernel/indtypes.cmi \ kernel/inductive.cmi pretyping/inductiveops.cmi library/libnames.cmi \ @@ -1430,13 +1453,13 @@ pretyping/matching.cmx: kernel/environ.cmx library/libnames.cmx \ pretyping/rawterm.cmx pretyping/reductionops.cmx kernel/term.cmx \ pretyping/termops.cmx lib/util.cmx pretyping/matching.cmi pretyping/pattern.cmo: kernel/environ.cmi library/libnames.cmi \ - library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ - lib/pp.cmi pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi \ - pretyping/pattern.cmi + kernel/mod_subst.cmi library/nameops.cmi kernel/names.cmi \ + library/nametab.cmi lib/options.cmi lib/pp.cmi pretyping/rawterm.cmi \ + kernel/term.cmi lib/util.cmi pretyping/pattern.cmi pretyping/pattern.cmx: kernel/environ.cmx library/libnames.cmx \ - library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ - lib/pp.cmx pretyping/rawterm.cmx kernel/term.cmx lib/util.cmx \ - pretyping/pattern.cmi + kernel/mod_subst.cmx library/nameops.cmx kernel/names.cmx \ + library/nametab.cmx lib/options.cmx lib/pp.cmx pretyping/rawterm.cmx \ + kernel/term.cmx lib/util.cmx pretyping/pattern.cmi pretyping/pretype_errors.cmo: kernel/environ.cmi pretyping/evd.cmi \ pretyping/inductiveops.cmi kernel/names.cmi library/nametab.cmi \ pretyping/rawterm.cmi kernel/reduction.cmi pretyping/reductionops.cmi \ @@ -1470,21 +1493,21 @@ pretyping/pretyping.cmx: pretyping/cases.cmx pretyping/classops.cmx \ pretyping/termops.cmx kernel/type_errors.cmx kernel/typeops.cmx \ lib/util.cmx pretyping/pretyping.cmi pretyping/rawterm.cmo: lib/dyn.cmi pretyping/evd.cmi library/libnames.cmi \ - kernel/names.cmi library/nametab.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/univ.cmi lib/util.cmi pretyping/rawterm.cmi + kernel/mod_subst.cmi kernel/names.cmi library/nametab.cmi kernel/sign.cmi \ + kernel/term.cmi kernel/univ.cmi lib/util.cmi pretyping/rawterm.cmi pretyping/rawterm.cmx: lib/dyn.cmx pretyping/evd.cmx library/libnames.cmx \ - kernel/names.cmx library/nametab.cmx kernel/sign.cmx kernel/term.cmx \ - kernel/univ.cmx lib/util.cmx pretyping/rawterm.cmi + kernel/mod_subst.cmx kernel/names.cmx library/nametab.cmx kernel/sign.cmx \ + kernel/term.cmx kernel/univ.cmx lib/util.cmx pretyping/rawterm.cmi pretyping/recordops.cmo: pretyping/classops.cmi library/lib.cmi \ library/libnames.cmi library/libobject.cmi library/library.cmi \ - kernel/names.cmi library/nametab.cmi lib/pp.cmi library/summary.cmi \ - kernel/term.cmi pretyping/termops.cmi kernel/typeops.cmi lib/util.cmi \ - pretyping/recordops.cmi + kernel/mod_subst.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ + library/summary.cmi kernel/term.cmi pretyping/termops.cmi \ + kernel/typeops.cmi lib/util.cmi pretyping/recordops.cmi pretyping/recordops.cmx: pretyping/classops.cmx library/lib.cmx \ library/libnames.cmx library/libobject.cmx library/library.cmx \ - kernel/names.cmx library/nametab.cmx lib/pp.cmx library/summary.cmx \ - kernel/term.cmx pretyping/termops.cmx kernel/typeops.cmx lib/util.cmx \ - pretyping/recordops.cmi + kernel/mod_subst.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ + library/summary.cmx kernel/term.cmx pretyping/termops.cmx \ + kernel/typeops.cmx lib/util.cmx pretyping/recordops.cmi pretyping/reductionops.cmo: kernel/closure.cmi kernel/declarations.cmi \ kernel/environ.cmi kernel/esubst.cmi pretyping/evd.cmi kernel/names.cmi \ lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \ @@ -1504,18 +1527,18 @@ pretyping/retyping.cmx: kernel/declarations.cmx kernel/environ.cmx \ kernel/names.cmx pretyping/reductionops.cmx kernel/term.cmx \ kernel/typeops.cmx kernel/univ.cmx lib/util.cmx pretyping/retyping.cmi pretyping/tacred.cmo: pretyping/cbv.cmi kernel/closure.cmi \ - kernel/conv_oracle.cmi kernel/declarations.cmi kernel/environ.cmi \ - pretyping/evd.cmi library/global.cmi kernel/inductive.cmi \ - library/libnames.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi lib/pp.cmi pretyping/rawterm.cmi \ + kernel/conv_oracle.cmi kernel/csymtable.cmi kernel/declarations.cmi \ + kernel/environ.cmi pretyping/evd.cmi library/global.cmi \ + kernel/inductive.cmi library/libnames.cmi library/nameops.cmi \ + kernel/names.cmi library/nametab.cmi lib/pp.cmi pretyping/rawterm.cmi \ pretyping/reductionops.cmi pretyping/retyping.cmi library/summary.cmi \ kernel/term.cmi pretyping/termops.cmi kernel/typeops.cmi \ pretyping/typing.cmi lib/util.cmi kernel/vconv.cmi pretyping/tacred.cmi pretyping/tacred.cmx: pretyping/cbv.cmx kernel/closure.cmx \ - kernel/conv_oracle.cmx kernel/declarations.cmx kernel/environ.cmx \ - pretyping/evd.cmx library/global.cmx kernel/inductive.cmx \ - library/libnames.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx lib/pp.cmx pretyping/rawterm.cmx \ + kernel/conv_oracle.cmx kernel/csymtable.cmx kernel/declarations.cmx \ + kernel/environ.cmx pretyping/evd.cmx library/global.cmx \ + kernel/inductive.cmx library/libnames.cmx library/nameops.cmx \ + kernel/names.cmx library/nametab.cmx lib/pp.cmx pretyping/rawterm.cmx \ pretyping/reductionops.cmx pretyping/retyping.cmx library/summary.cmx \ kernel/term.cmx pretyping/termops.cmx kernel/typeops.cmx \ pretyping/typing.cmx lib/util.cmx kernel/vconv.cmx pretyping/tacred.cmi @@ -1671,42 +1694,46 @@ tactics/auto.cmo: tactics/btermdn.cmi pretyping/clenv.cmi \ library/global.cmi tactics/hiddentac.cmi tactics/hipattern.cmi \ kernel/inductive.cmi library/lib.cmi library/libnames.cmi \ library/libobject.cmi library/library.cmi proofs/logic.cmi \ - pretyping/matching.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi lib/options.cmi pretyping/pattern.cmi \ - proofs/pfedit.cmi lib/pp.cmi parsing/pptactic.cmi parsing/printer.cmi \ - proofs/proof_type.cmi pretyping/rawterm.cmi kernel/reduction.cmi \ - proofs/refiner.cmi kernel/sign.cmi library/summary.cmi proofs/tacexpr.cmo \ - proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \ - tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi \ - pretyping/typing.cmi lib/util.cmi toplevel/vernacexpr.cmo \ - tactics/auto.cmi + pretyping/matching.cmi kernel/mod_subst.cmi library/nameops.cmi \ + kernel/names.cmi library/nametab.cmi lib/options.cmi \ + pretyping/pattern.cmi proofs/pfedit.cmi lib/pp.cmi parsing/pptactic.cmi \ + parsing/printer.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \ + kernel/reduction.cmi proofs/refiner.cmi kernel/sign.cmi \ + library/summary.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \ + pretyping/tacred.cmi tactics/tacticals.cmi tactics/tactics.cmi \ + kernel/term.cmi pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ + toplevel/vernacexpr.cmo tactics/auto.cmi tactics/auto.cmx: tactics/btermdn.cmx pretyping/clenv.cmx \ interp/constrintern.cmx kernel/declarations.cmx tactics/dhyp.cmx \ kernel/environ.cmx proofs/evar_refiner.cmx pretyping/evd.cmx \ library/global.cmx tactics/hiddentac.cmx tactics/hipattern.cmx \ kernel/inductive.cmx library/lib.cmx library/libnames.cmx \ library/libobject.cmx library/library.cmx proofs/logic.cmx \ - pretyping/matching.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx lib/options.cmx pretyping/pattern.cmx \ - proofs/pfedit.cmx lib/pp.cmx parsing/pptactic.cmx parsing/printer.cmx \ - proofs/proof_type.cmx pretyping/rawterm.cmx kernel/reduction.cmx \ - proofs/refiner.cmx kernel/sign.cmx library/summary.cmx proofs/tacexpr.cmx \ - proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \ - tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx \ - pretyping/typing.cmx lib/util.cmx toplevel/vernacexpr.cmx \ - tactics/auto.cmi + pretyping/matching.cmx kernel/mod_subst.cmx library/nameops.cmx \ + kernel/names.cmx library/nametab.cmx lib/options.cmx \ + pretyping/pattern.cmx proofs/pfedit.cmx lib/pp.cmx parsing/pptactic.cmx \ + parsing/printer.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \ + kernel/reduction.cmx proofs/refiner.cmx kernel/sign.cmx \ + library/summary.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \ + pretyping/tacred.cmx tactics/tacticals.cmx tactics/tactics.cmx \ + kernel/term.cmx pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ + toplevel/vernacexpr.cmx tactics/auto.cmi tactics/autorewrite.cmo: parsing/ast.cmi parsing/coqast.cmi \ - tactics/equality.cmi tactics/hipattern.cmi library/lib.cmi \ - library/libobject.cmi kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi \ + tactics/equality.cmi pretyping/evd.cmi library/global.cmi \ + tactics/hipattern.cmi library/lib.cmi library/libobject.cmi \ + kernel/mod_subst.cmi kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi \ library/summary.cmi proofs/tacexpr.cmo tactics/tacinterp.cmi \ - tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi lib/util.cmi \ - toplevel/vernacinterp.cmi tactics/autorewrite.cmi + tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ + pretyping/typing.cmi lib/util.cmi toplevel/vernacinterp.cmi \ + tactics/autorewrite.cmi tactics/autorewrite.cmx: parsing/ast.cmx parsing/coqast.cmx \ - tactics/equality.cmx tactics/hipattern.cmx library/lib.cmx \ - library/libobject.cmx kernel/names.cmx lib/pp.cmx proofs/proof_type.cmx \ + tactics/equality.cmx pretyping/evd.cmx library/global.cmx \ + tactics/hipattern.cmx library/lib.cmx library/libobject.cmx \ + kernel/mod_subst.cmx kernel/names.cmx lib/pp.cmx proofs/proof_type.cmx \ library/summary.cmx proofs/tacexpr.cmx tactics/tacinterp.cmx \ - tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx \ - toplevel/vernacinterp.cmx tactics/autorewrite.cmi + tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ + pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx \ + tactics/autorewrite.cmi tactics/btermdn.cmo: tactics/dn.cmi pretyping/pattern.cmi kernel/term.cmi \ tactics/termdn.cmi tactics/btermdn.cmi tactics/btermdn.cmx: tactics/dn.cmx pretyping/pattern.cmx kernel/term.cmx \ @@ -1914,22 +1941,22 @@ tactics/leminv.cmo: pretyping/clenv.cmi proofs/clenvtac.cmi \ library/declare.cmi kernel/entries.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi pretyping/evd.cmi library/global.cmi \ pretyping/inductiveops.cmi tactics/inv.cmi library/nameops.cmi \ - kernel/names.cmi proofs/pfedit.cmi lib/pp.cmi pretyping/pretyping.cmi \ - parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ - pretyping/reductionops.cmi kernel/safe_typing.cmi kernel/sign.cmi \ - proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \ - kernel/term.cmi pretyping/termops.cmi lib/util.cmi \ + kernel/names.cmi lib/options.cmi proofs/pfedit.cmi lib/pp.cmi \ + pretyping/pretyping.cmi parsing/printer.cmi proofs/proof_trees.cmi \ + proofs/proof_type.cmi pretyping/reductionops.cmi kernel/safe_typing.cmi \ + kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \ toplevel/vernacexpr.cmo tactics/leminv.cmi tactics/leminv.cmx: pretyping/clenv.cmx proofs/clenvtac.cmx \ interp/constrintern.cmx library/decl_kinds.cmx kernel/declarations.cmx \ library/declare.cmx kernel/entries.cmx kernel/environ.cmx \ proofs/evar_refiner.cmx pretyping/evd.cmx library/global.cmx \ pretyping/inductiveops.cmx tactics/inv.cmx library/nameops.cmx \ - kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx pretyping/pretyping.cmx \ - parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ - pretyping/reductionops.cmx kernel/safe_typing.cmx kernel/sign.cmx \ - proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ - kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ + kernel/names.cmx lib/options.cmx proofs/pfedit.cmx lib/pp.cmx \ + pretyping/pretyping.cmx parsing/printer.cmx proofs/proof_trees.cmx \ + proofs/proof_type.cmx pretyping/reductionops.cmx kernel/safe_typing.cmx \ + kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ + tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ toplevel/vernacexpr.cmx tactics/leminv.cmi tactics/nbtermdn.cmo: tactics/btermdn.cmi lib/gmap.cmi library/libobject.cmi \ library/library.cmi kernel/names.cmi pretyping/pattern.cmi \ @@ -1954,29 +1981,31 @@ tactics/setoid_replace.cmo: pretyping/clenv.cmi kernel/closure.cmi \ library/declare.cmi kernel/entries.cmi kernel/environ.cmi \ pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi lib/gmap.cmi \ library/lib.cmi library/libnames.cmi library/libobject.cmi \ - proofs/logic.cmi library/nameops.cmi kernel/names.cmi library/nametab.cmi \ - lib/options.cmi proofs/pfedit.cmi lib/pp.cmi translate/ppconstrnew.cmi \ - pretyping/pretype_errors.cmi parsing/printer.cmi proofs/proof_type.cmi \ - pretyping/rawterm.cmi kernel/reduction.cmi pretyping/reductionops.cmi \ - kernel/safe_typing.cmi kernel/sign.cmi library/summary.cmi \ - proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \ - tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi \ - interp/topconstr.cmi pretyping/typing.cmi pretyping/unification.cmi \ - lib/util.cmi toplevel/vernacexpr.cmo tactics/setoid_replace.cmi + proofs/logic.cmi kernel/mod_subst.cmi library/nameops.cmi \ + kernel/names.cmi library/nametab.cmi lib/options.cmi proofs/pfedit.cmi \ + lib/pp.cmi translate/ppconstrnew.cmi pretyping/pretype_errors.cmi \ + parsing/printer.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \ + kernel/reduction.cmi pretyping/reductionops.cmi kernel/safe_typing.cmi \ + kernel/sign.cmi library/summary.cmi proofs/tacmach.cmi \ + pretyping/tacred.cmi tactics/tacticals.cmi tactics/tactics.cmi \ + kernel/term.cmi pretyping/termops.cmi interp/topconstr.cmi \ + pretyping/typing.cmi pretyping/unification.cmi lib/util.cmi \ + toplevel/vernacexpr.cmo tactics/setoid_replace.cmi tactics/setoid_replace.cmx: pretyping/clenv.cmx kernel/closure.cmx \ interp/constrintern.cmx interp/coqlib.cmx library/decl_kinds.cmx \ library/declare.cmx kernel/entries.cmx kernel/environ.cmx \ pretyping/evarutil.cmx pretyping/evd.cmx library/global.cmx lib/gmap.cmx \ library/lib.cmx library/libnames.cmx library/libobject.cmx \ - proofs/logic.cmx library/nameops.cmx kernel/names.cmx library/nametab.cmx \ - lib/options.cmx proofs/pfedit.cmx lib/pp.cmx translate/ppconstrnew.cmx \ - pretyping/pretype_errors.cmx parsing/printer.cmx proofs/proof_type.cmx \ - pretyping/rawterm.cmx kernel/reduction.cmx pretyping/reductionops.cmx \ - kernel/safe_typing.cmx kernel/sign.cmx library/summary.cmx \ - proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \ - tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx \ - interp/topconstr.cmx pretyping/typing.cmx pretyping/unification.cmx \ - lib/util.cmx toplevel/vernacexpr.cmx tactics/setoid_replace.cmi + proofs/logic.cmx kernel/mod_subst.cmx library/nameops.cmx \ + kernel/names.cmx library/nametab.cmx lib/options.cmx proofs/pfedit.cmx \ + lib/pp.cmx translate/ppconstrnew.cmx pretyping/pretype_errors.cmx \ + parsing/printer.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \ + kernel/reduction.cmx pretyping/reductionops.cmx kernel/safe_typing.cmx \ + kernel/sign.cmx library/summary.cmx proofs/tacmach.cmx \ + pretyping/tacred.cmx tactics/tacticals.cmx tactics/tactics.cmx \ + kernel/term.cmx pretyping/termops.cmx interp/topconstr.cmx \ + pretyping/typing.cmx pretyping/unification.cmx lib/util.cmx \ + toplevel/vernacexpr.cmx tactics/setoid_replace.cmi tactics/tacinterp.cmo: parsing/ast.cmi tactics/auto.cmi kernel/closure.cmi \ interp/constrintern.cmi parsing/coqast.cmi library/decl_kinds.cmo \ kernel/declarations.cmi tactics/dhyp.cmi lib/dyn.cmi tactics/elim.cmi \ @@ -1984,16 +2013,16 @@ tactics/tacinterp.cmo: parsing/ast.cmi tactics/auto.cmi kernel/closure.cmi \ library/global.cmi lib/gmap.cmi tactics/hiddentac.cmi tactics/inv.cmi \ tactics/leminv.cmi library/lib.cmi library/libnames.cmi \ library/libobject.cmi proofs/logic.cmi pretyping/matching.cmi \ - library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ - pretyping/pattern.cmi proofs/pfedit.cmi lib/pp.cmi \ - pretyping/pretype_errors.cmi pretyping/pretyping.cmi parsing/printer.cmi \ - proofs/proof_type.cmi pretyping/rawterm.cmi proofs/refiner.cmi \ - pretyping/retyping.cmi kernel/safe_typing.cmi kernel/sign.cmi \ - library/summary.cmi interp/syntax_def.cmi proofs/tacexpr.cmo \ - proofs/tacmach.cmi pretyping/tacred.cmi proofs/tactic_debug.cmi \ - tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi \ - interp/topconstr.cmi pretyping/typing.cmi lib/util.cmi \ - tactics/tacinterp.cmi + kernel/mod_subst.cmi library/nameops.cmi kernel/names.cmi \ + library/nametab.cmi lib/options.cmi pretyping/pattern.cmi \ + proofs/pfedit.cmi lib/pp.cmi pretyping/pretype_errors.cmi \ + pretyping/pretyping.cmi parsing/printer.cmi proofs/proof_type.cmi \ + pretyping/rawterm.cmi proofs/refiner.cmi pretyping/retyping.cmi \ + kernel/safe_typing.cmi kernel/sign.cmi library/summary.cmi \ + interp/syntax_def.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \ + pretyping/tacred.cmi proofs/tactic_debug.cmi tactics/tactics.cmi \ + kernel/term.cmi pretyping/termops.cmi interp/topconstr.cmi \ + pretyping/typing.cmi lib/util.cmi tactics/tacinterp.cmi tactics/tacinterp.cmx: parsing/ast.cmx tactics/auto.cmx kernel/closure.cmx \ interp/constrintern.cmx parsing/coqast.cmx library/decl_kinds.cmx \ kernel/declarations.cmx tactics/dhyp.cmx lib/dyn.cmx tactics/elim.cmx \ @@ -2001,16 +2030,16 @@ tactics/tacinterp.cmx: parsing/ast.cmx tactics/auto.cmx kernel/closure.cmx \ library/global.cmx lib/gmap.cmx tactics/hiddentac.cmx tactics/inv.cmx \ tactics/leminv.cmx library/lib.cmx library/libnames.cmx \ library/libobject.cmx proofs/logic.cmx pretyping/matching.cmx \ - library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ - pretyping/pattern.cmx proofs/pfedit.cmx lib/pp.cmx \ - pretyping/pretype_errors.cmx pretyping/pretyping.cmx parsing/printer.cmx \ - proofs/proof_type.cmx pretyping/rawterm.cmx proofs/refiner.cmx \ - pretyping/retyping.cmx kernel/safe_typing.cmx kernel/sign.cmx \ - library/summary.cmx interp/syntax_def.cmx proofs/tacexpr.cmx \ - proofs/tacmach.cmx pretyping/tacred.cmx proofs/tactic_debug.cmx \ - tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx \ - interp/topconstr.cmx pretyping/typing.cmx lib/util.cmx \ - tactics/tacinterp.cmi + kernel/mod_subst.cmx library/nameops.cmx kernel/names.cmx \ + library/nametab.cmx lib/options.cmx pretyping/pattern.cmx \ + proofs/pfedit.cmx lib/pp.cmx pretyping/pretype_errors.cmx \ + pretyping/pretyping.cmx parsing/printer.cmx proofs/proof_type.cmx \ + pretyping/rawterm.cmx proofs/refiner.cmx pretyping/retyping.cmx \ + kernel/safe_typing.cmx kernel/sign.cmx library/summary.cmx \ + interp/syntax_def.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \ + pretyping/tacred.cmx proofs/tactic_debug.cmx tactics/tactics.cmx \ + kernel/term.cmx pretyping/termops.cmx interp/topconstr.cmx \ + pretyping/typing.cmx lib/util.cmx tactics/tacinterp.cmi tactics/tacticals.cmo: pretyping/clenv.cmi proofs/clenvtac.cmi \ kernel/declarations.cmi kernel/environ.cmi proofs/evar_refiner.cmi \ pretyping/evd.cmi interp/genarg.cmi library/global.cmi \ @@ -2287,20 +2316,6 @@ toplevel/toplevel.cmx: toplevel/cerrors.cmx library/lib.cmx \ toplevel/vernac.cmx toplevel/vernacexpr.cmx toplevel/toplevel.cmi toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi -toplevel/vernac.cmo: interp/constrextern.cmi interp/constrintern.cmi \ - parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi library/library.cmi \ - kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \ - lib/pp.cmi translate/ppvernacnew.cmi proofs/refiner.cmi \ - library/states.cmi lib/system.cmi tactics/tacinterp.cmi \ - proofs/tacmach.cmi lib/util.cmi toplevel/vernacentries.cmi \ - toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi -toplevel/vernac.cmx: interp/constrextern.cmx interp/constrintern.cmx \ - parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx library/library.cmx \ - kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \ - lib/pp.cmx translate/ppvernacnew.cmx proofs/refiner.cmx \ - library/states.cmx lib/system.cmx tactics/tacinterp.cmx \ - proofs/tacmach.cmx lib/util.cmx toplevel/vernacentries.cmx \ - toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi toplevel/vernacentries.cmo: tactics/auto.cmi toplevel/class.cmi \ pretyping/classops.cmi toplevel/command.cmi interp/constrextern.cmi \ interp/constrintern.cmi library/decl_kinds.cmo library/declaremods.cmi \ @@ -2365,6 +2380,20 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx \ kernel/names.cmx lib/options.cmx lib/pp.cmx proofs/proof_type.cmx \ proofs/tacexpr.cmx tactics/tacinterp.cmx lib/util.cmx \ toplevel/vernacexpr.cmx toplevel/vernacinterp.cmi +toplevel/vernac.cmo: interp/constrextern.cmi interp/constrintern.cmi \ + parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi library/library.cmi \ + kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \ + lib/pp.cmi translate/ppvernacnew.cmi proofs/refiner.cmi \ + library/states.cmi lib/system.cmi tactics/tacinterp.cmi \ + proofs/tacmach.cmi lib/util.cmi toplevel/vernacentries.cmi \ + toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi +toplevel/vernac.cmx: interp/constrextern.cmx interp/constrintern.cmx \ + parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx library/library.cmx \ + kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \ + lib/pp.cmx translate/ppvernacnew.cmx proofs/refiner.cmx \ + library/states.cmx lib/system.cmx tactics/tacinterp.cmx \ + proofs/tacmach.cmx lib/util.cmx toplevel/vernacentries.cmx \ + toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi translate/ppconstrnew.cmo: parsing/ast.cmi lib/bignat.cmi \ interp/constrextern.cmi interp/constrintern.cmi parsing/coqast.cmi \ pretyping/evd.cmi interp/genarg.cmi library/global.cmi library/lib.cmi \ @@ -2372,8 +2401,8 @@ translate/ppconstrnew.cmo: parsing/ast.cmi lib/bignat.cmi \ library/nametab.cmi lib/options.cmi pretyping/pattern.cmi lib/pp.cmi \ interp/ppextend.cmi pretyping/pretyping.cmi pretyping/rawterm.cmi \ pretyping/retyping.cmi interp/symbols.cmi interp/syntax_def.cmi \ - kernel/term.cmi pretyping/termops.cmi interp/topconstr.cmi lib/util.cmi \ - translate/ppconstrnew.cmi + kernel/term.cmi pretyping/termops.cmi interp/topconstr.cmi \ + kernel/univ.cmi lib/util.cmi translate/ppconstrnew.cmi translate/ppconstrnew.cmx: parsing/ast.cmx lib/bignat.cmx \ interp/constrextern.cmx interp/constrintern.cmx parsing/coqast.cmx \ pretyping/evd.cmx interp/genarg.cmx library/global.cmx library/lib.cmx \ @@ -2381,8 +2410,8 @@ translate/ppconstrnew.cmx: parsing/ast.cmx lib/bignat.cmx \ library/nametab.cmx lib/options.cmx pretyping/pattern.cmx lib/pp.cmx \ interp/ppextend.cmx pretyping/pretyping.cmx pretyping/rawterm.cmx \ pretyping/retyping.cmx interp/symbols.cmx interp/syntax_def.cmx \ - kernel/term.cmx pretyping/termops.cmx interp/topconstr.cmx lib/util.cmx \ - translate/ppconstrnew.cmi + kernel/term.cmx pretyping/termops.cmx interp/topconstr.cmx \ + kernel/univ.cmx lib/util.cmx translate/ppconstrnew.cmi translate/pptacticnew.cmo: kernel/closure.cmi interp/constrextern.cmi \ lib/dyn.cmi parsing/egrammar.cmi kernel/environ.cmi parsing/extend.cmi \ interp/genarg.cmi library/global.cmi library/libnames.cmi \ @@ -2453,6 +2482,12 @@ contrib/cc/cctac.cmx: contrib/cc/ccalgo.cmx contrib/cc/ccproof.cmx \ proofs/refiner.cmx kernel/sign.cmx proofs/tacexpr.cmx \ tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx +contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \ + kernel/sign.cmi kernel/term.cmi kernel/univ.cmi \ + contrib/correctness/pcicenv.cmi +contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \ + kernel/sign.cmx kernel/term.cmx kernel/univ.cmx \ + contrib/correctness/pcicenv.cmi contrib/correctness/pcic.cmo: kernel/declarations.cmi library/declare.cmi \ pretyping/detyping.cmi kernel/entries.cmi library/global.cmi \ kernel/indtypes.cmi library/libnames.cmi library/nameops.cmi \ @@ -2467,12 +2502,6 @@ contrib/correctness/pcic.cmx: kernel/declarations.cmx library/declare.cmx \ toplevel/record.cmx kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \ interp/topconstr.cmx kernel/typeops.cmx lib/util.cmx \ toplevel/vernacexpr.cmx contrib/correctness/pcic.cmi -contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \ - kernel/sign.cmi kernel/term.cmi kernel/univ.cmi \ - contrib/correctness/pcicenv.cmi -contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \ - kernel/sign.cmx kernel/term.cmx kernel/univ.cmx \ - contrib/correctness/pcicenv.cmi contrib/correctness/pdb.cmo: interp/constrintern.cmi library/global.cmi \ kernel/names.cmi library/nametab.cmi kernel/term.cmi \ pretyping/termops.cmi contrib/correctness/pdb.cmi @@ -2613,16 +2642,16 @@ contrib/extraction/extract_env.cmo: contrib/extraction/common.cmi \ kernel/declarations.cmi contrib/extraction/extraction.cmi \ library/global.cmi library/lib.cmi library/libnames.cmi \ library/libobject.cmi library/library.cmi contrib/extraction/miniml.cmi \ - kernel/modops.cmi contrib/extraction/modutil.cmi kernel/names.cmi \ - library/nametab.cmi lib/pp.cmi kernel/reduction.cmi \ + kernel/mod_subst.cmi kernel/modops.cmi contrib/extraction/modutil.cmi \ + kernel/names.cmi library/nametab.cmi lib/pp.cmi kernel/reduction.cmi \ contrib/extraction/table.cmi kernel/term.cmi lib/util.cmi \ contrib/extraction/extract_env.cmi contrib/extraction/extract_env.cmx: contrib/extraction/common.cmx \ kernel/declarations.cmx contrib/extraction/extraction.cmx \ library/global.cmx library/lib.cmx library/libnames.cmx \ library/libobject.cmx library/library.cmx contrib/extraction/miniml.cmi \ - kernel/modops.cmx contrib/extraction/modutil.cmx kernel/names.cmx \ - library/nametab.cmx lib/pp.cmx kernel/reduction.cmx \ + kernel/mod_subst.cmx kernel/modops.cmx contrib/extraction/modutil.cmx \ + kernel/names.cmx library/nametab.cmx lib/pp.cmx kernel/reduction.cmx \ contrib/extraction/table.cmx kernel/term.cmx lib/util.cmx \ contrib/extraction/extract_env.cmi contrib/extraction/extraction.cmo: kernel/declarations.cmi kernel/environ.cmi \ @@ -2675,12 +2704,14 @@ contrib/extraction/mlutil.cmx: library/libnames.cmx \ contrib/extraction/mlutil.cmi contrib/extraction/modutil.cmo: kernel/declarations.cmi kernel/environ.cmi \ library/libnames.cmi contrib/extraction/miniml.cmi \ - contrib/extraction/mlutil.cmi kernel/modops.cmi kernel/names.cmi \ - contrib/extraction/table.cmi lib/util.cmi contrib/extraction/modutil.cmi + contrib/extraction/mlutil.cmi kernel/mod_subst.cmi kernel/modops.cmi \ + kernel/names.cmi contrib/extraction/table.cmi lib/util.cmi \ + contrib/extraction/modutil.cmi contrib/extraction/modutil.cmx: kernel/declarations.cmx kernel/environ.cmx \ library/libnames.cmx contrib/extraction/miniml.cmi \ - contrib/extraction/mlutil.cmx kernel/modops.cmx kernel/names.cmx \ - contrib/extraction/table.cmx lib/util.cmx contrib/extraction/modutil.cmi + contrib/extraction/mlutil.cmx kernel/mod_subst.cmx kernel/modops.cmx \ + kernel/names.cmx contrib/extraction/table.cmx lib/util.cmx \ + contrib/extraction/modutil.cmi contrib/extraction/ocaml.cmo: library/libnames.cmi \ contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \ contrib/extraction/modutil.cmi library/nameops.cmi kernel/names.cmi \ @@ -2717,26 +2748,28 @@ contrib/field/field.cmo: toplevel/cerrors.cmi interp/constrintern.cmi \ interp/coqlib.cmi parsing/egrammar.cmi pretyping/evd.cmi \ parsing/extend.cmi interp/genarg.cmi library/global.cmi lib/gmap.cmi \ tactics/hipattern.cmi library/lib.cmi library/libnames.cmi \ - library/libobject.cmi library/library.cmi kernel/names.cmi \ - lib/options.cmi parsing/pcoq.cmi lib/pp.cmi translate/ppconstrnew.cmi \ - parsing/pptactic.cmi parsing/printer.cmi proofs/proof_type.cmi \ - contrib/ring/quote.cmo pretyping/reductionops.cmi proofs/refiner.cmi \ - contrib/ring/ring.cmo library/summary.cmi proofs/tacexpr.cmo \ - tactics/tacinterp.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ - kernel/term.cmi interp/topconstr.cmi pretyping/typing.cmi lib/util.cmi \ - toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi + library/libobject.cmi library/library.cmi kernel/mod_subst.cmi \ + kernel/names.cmi lib/options.cmi parsing/pcoq.cmi lib/pp.cmi \ + translate/ppconstrnew.cmi parsing/pptactic.cmi parsing/printer.cmi \ + proofs/proof_type.cmi contrib/ring/quote.cmo pretyping/reductionops.cmi \ + proofs/refiner.cmi contrib/ring/ring.cmo library/summary.cmi \ + proofs/tacexpr.cmo tactics/tacinterp.cmi proofs/tacmach.cmi \ + tactics/tacticals.cmi kernel/term.cmi interp/topconstr.cmi \ + pretyping/typing.cmi lib/util.cmi toplevel/vernacexpr.cmo \ + toplevel/vernacinterp.cmi contrib/field/field.cmx: toplevel/cerrors.cmx interp/constrintern.cmx \ interp/coqlib.cmx parsing/egrammar.cmx pretyping/evd.cmx \ parsing/extend.cmx interp/genarg.cmx library/global.cmx lib/gmap.cmx \ tactics/hipattern.cmx library/lib.cmx library/libnames.cmx \ - library/libobject.cmx library/library.cmx kernel/names.cmx \ - lib/options.cmx parsing/pcoq.cmx lib/pp.cmx translate/ppconstrnew.cmx \ - parsing/pptactic.cmx parsing/printer.cmx proofs/proof_type.cmx \ - contrib/ring/quote.cmx pretyping/reductionops.cmx proofs/refiner.cmx \ - contrib/ring/ring.cmx library/summary.cmx proofs/tacexpr.cmx \ - tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ - kernel/term.cmx interp/topconstr.cmx pretyping/typing.cmx lib/util.cmx \ - toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx + library/libobject.cmx library/library.cmx kernel/mod_subst.cmx \ + kernel/names.cmx lib/options.cmx parsing/pcoq.cmx lib/pp.cmx \ + translate/ppconstrnew.cmx parsing/pptactic.cmx parsing/printer.cmx \ + proofs/proof_type.cmx contrib/ring/quote.cmx pretyping/reductionops.cmx \ + proofs/refiner.cmx contrib/ring/ring.cmx library/summary.cmx \ + proofs/tacexpr.cmx tactics/tacinterp.cmx proofs/tacmach.cmx \ + tactics/tacticals.cmx kernel/term.cmx interp/topconstr.cmx \ + pretyping/typing.cmx lib/util.cmx toplevel/vernacexpr.cmx \ + toplevel/vernacinterp.cmx contrib/first-order/formula.cmo: kernel/closure.cmi kernel/declarations.cmi \ library/global.cmi tactics/hipattern.cmi kernel/inductive.cmi \ pretyping/inductiveops.cmi library/libnames.cmi kernel/names.cmi \ @@ -3055,6 +3088,14 @@ contrib/interface/pbp.cmx: interp/coqlib.cmx kernel/environ.cmx \ proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ kernel/term.cmx pretyping/termops.cmx interp/topconstr.cmx \ pretyping/typing.cmx lib/util.cmx contrib/interface/pbp.cmi +contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \ + parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \ + parsing/printer.cmi contrib/interface/translate.cmi \ + contrib/interface/vtp.cmi contrib/interface/xlate.cmi +contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \ + parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \ + parsing/printer.cmx contrib/interface/translate.cmx \ + contrib/interface/vtp.cmx contrib/interface/xlate.cmx contrib/interface/showproof.cmo: pretyping/clenv.cmi interp/constrintern.cmi \ parsing/coqast.cmi kernel/declarations.cmi kernel/environ.cmi \ pretyping/evd.cmi interp/genarg.cmi library/global.cmi \ @@ -3079,14 +3120,6 @@ contrib/interface/showproof.cmx: pretyping/clenv.cmx interp/constrintern.cmx \ pretyping/termops.cmx contrib/interface/translate.cmx \ pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx \ contrib/interface/showproof.cmi -contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \ - parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \ - parsing/printer.cmi contrib/interface/translate.cmi \ - contrib/interface/vtp.cmi contrib/interface/xlate.cmi -contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \ - parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \ - parsing/printer.cmx contrib/interface/translate.cmx \ - contrib/interface/vtp.cmx contrib/interface/xlate.cmx contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \ interp/constrextern.cmi contrib/interface/ctast.cmo kernel/environ.cmi \ pretyping/evarutil.cmi pretyping/evd.cmi library/libobject.cmi \ @@ -3225,26 +3258,26 @@ contrib/ring/ring.cmo: kernel/closure.cmi interp/constrintern.cmi \ interp/coqlib.cmi tactics/equality.cmi pretyping/evd.cmi \ library/global.cmi tactics/hiddentac.cmi tactics/hipattern.cmi \ library/lib.cmi library/libnames.cmi library/libobject.cmi \ - library/library.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi lib/options.cmi pretyping/pattern.cmi lib/pp.cmi \ - parsing/printer.cmi proofs/proof_trees.cmi contrib/ring/quote.cmo \ - pretyping/reductionops.cmi tactics/setoid_replace.cmi library/summary.cmi \ - proofs/tacexpr.cmo proofs/tacmach.cmi pretyping/tacred.cmi \ - tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ - pretyping/typing.cmi lib/util.cmi toplevel/vernacexpr.cmo \ - toplevel/vernacinterp.cmi + library/library.cmi kernel/mod_subst.cmi library/nameops.cmi \ + kernel/names.cmi library/nametab.cmi lib/options.cmi \ + pretyping/pattern.cmi lib/pp.cmi parsing/printer.cmi \ + proofs/proof_trees.cmi contrib/ring/quote.cmo pretyping/reductionops.cmi \ + tactics/setoid_replace.cmi library/summary.cmi proofs/tacexpr.cmo \ + proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ + toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi contrib/ring/ring.cmx: kernel/closure.cmx interp/constrintern.cmx \ interp/coqlib.cmx tactics/equality.cmx pretyping/evd.cmx \ library/global.cmx tactics/hiddentac.cmx tactics/hipattern.cmx \ library/lib.cmx library/libnames.cmx library/libobject.cmx \ - library/library.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx lib/options.cmx pretyping/pattern.cmx lib/pp.cmx \ - parsing/printer.cmx proofs/proof_trees.cmx contrib/ring/quote.cmx \ - pretyping/reductionops.cmx tactics/setoid_replace.cmx library/summary.cmx \ - proofs/tacexpr.cmx proofs/tacmach.cmx pretyping/tacred.cmx \ - tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ - pretyping/typing.cmx lib/util.cmx toplevel/vernacexpr.cmx \ - toplevel/vernacinterp.cmx + library/library.cmx kernel/mod_subst.cmx library/nameops.cmx \ + kernel/names.cmx library/nametab.cmx lib/options.cmx \ + pretyping/pattern.cmx lib/pp.cmx parsing/printer.cmx \ + proofs/proof_trees.cmx contrib/ring/quote.cmx pretyping/reductionops.cmx \ + tactics/setoid_replace.cmx library/summary.cmx proofs/tacexpr.cmx \ + proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \ + tactics/tactics.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ + toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx contrib/romega/const_omega.cmo: interp/coqlib.cmi library/global.cmi \ library/libnames.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ kernel/term.cmi lib/util.cmi @@ -3269,12 +3302,12 @@ contrib/romega/refl_omega.cmx: contrib/romega/const_omega.cmx \ proofs/logic.cmx kernel/names.cmx contrib/romega/omega2.cmx \ lib/options.cmx lib/pp.cmx parsing/printer.cmx proofs/tacmach.cmx \ tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx -contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi -contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx contrib/xml/acic2Xml.cmo: contrib/xml/acic.cmo contrib/xml/cic2acic.cmo \ kernel/names.cmi kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi contrib/xml/acic2Xml.cmx: contrib/xml/acic.cmx contrib/xml/cic2acic.cmx \ kernel/names.cmx kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx +contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi +contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx contrib/xml/cic2acic.cmo: contrib/xml/acic.cmo kernel/declarations.cmi \ library/declare.cmi library/dischargedhypsmap.cmi \ contrib/xml/doubleTypeInference.cmi kernel/environ.cmi pretyping/evd.cmi \ @@ -3335,8 +3368,6 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/acic.cmx contrib/xml/acic2Xml.cmx \ contrib/xml/unshare.cmx lib/util.cmx contrib/xml/xml.cmx contrib/xml/unshare.cmo: contrib/xml/unshare.cmi contrib/xml/unshare.cmx: contrib/xml/unshare.cmi -contrib/xml/xml.cmo: contrib/xml/xml.cmi -contrib/xml/xml.cmx: contrib/xml/xml.cmi contrib/xml/xmlcommand.cmo: contrib/xml/acic.cmo contrib/xml/acic2Xml.cmo \ contrib/xml/cic2acic.cmo config/coq_config.cmi library/decl_kinds.cmo \ kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \ @@ -3365,10 +3396,8 @@ contrib/xml/xmlentries.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \ contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \ parsing/extend.cmx interp/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \ lib/util.cmx toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx -ide/utils/configwin.cmo: ide/utils/configwin_ihm.cmo \ - ide/utils/configwin_types.cmo ide/utils/configwin.cmi -ide/utils/configwin.cmx: ide/utils/configwin_ihm.cmx \ - ide/utils/configwin_types.cmx ide/utils/configwin.cmi +contrib/xml/xml.cmo: contrib/xml/xml.cmi +contrib/xml/xml.cmx: contrib/xml/xml.cmi ide/utils/configwin_html_config.cmo: ide/utils/configwin_ihm.cmo \ ide/utils/configwin_messages.cmo ide/utils/configwin_types.cmo \ ide/utils/uoptions.cmi @@ -3379,6 +3408,10 @@ ide/utils/configwin_ihm.cmo: ide/utils/configwin_messages.cmo \ ide/utils/configwin_types.cmo ide/utils/okey.cmi ide/utils/uoptions.cmi ide/utils/configwin_ihm.cmx: ide/utils/configwin_messages.cmx \ ide/utils/configwin_types.cmx ide/utils/okey.cmx ide/utils/uoptions.cmx +ide/utils/configwin.cmo: ide/utils/configwin_ihm.cmo \ + ide/utils/configwin_types.cmo ide/utils/configwin.cmi +ide/utils/configwin.cmx: ide/utils/configwin_ihm.cmx \ + ide/utils/configwin_types.cmx ide/utils/configwin.cmi ide/utils/configwin_types.cmo: ide/utils/configwin_keys.cmo \ ide/utils/uoptions.cmi ide/utils/configwin_types.cmx: ide/utils/configwin_keys.cmx \ @@ -3504,50 +3537,80 @@ tools/coq_makefile.cmx: tools/coq-tex.cmo: tools/coq-tex.cmx: coq_fix_code.o: kernel/byterun/coq_fix_code.c \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/fail.h \ - /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_fix_code.h + /auto/demons/sacerdot/local/lib/ocaml/caml/config.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/compatibility.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/misc.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/mlvalues.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/fail.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/memory.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \ - /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/alloc.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h \ - kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h + /auto/demons/sacerdot/local/lib/ocaml/caml/mlvalues.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/compatibility.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/config.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/misc.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/alloc.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ + kernel/byterun/coq_memory.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/fail.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/memory.h \ + kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \ - /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/alloc.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h -coq_values.o: kernel/byterun/coq_values.c \ - kernel/byterun/coq_fix_code.h /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h \ - kernel/byterun/coq_values.h /usr/local/lib/ocaml/caml/alloc.h + /auto/demons/sacerdot/local/lib/ocaml/caml/mlvalues.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/compatibility.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/config.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/misc.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/alloc.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ + kernel/byterun/coq_memory.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/fail.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/memory.h +coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/mlvalues.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/compatibility.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/config.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/misc.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/fail.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/memory.h \ + kernel/byterun/coq_values.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/alloc.h coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/fail.h \ - /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_fix_code.h + /auto/demons/sacerdot/local/lib/ocaml/caml/config.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/compatibility.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/misc.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/mlvalues.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/fail.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/memory.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h coq_interp.d.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \ - /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/alloc.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h \ - kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h + /auto/demons/sacerdot/local/lib/ocaml/caml/mlvalues.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/compatibility.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/config.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/misc.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/alloc.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ + kernel/byterun/coq_memory.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/fail.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/memory.h \ + kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h coq_memory.d.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \ - /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - /usr/local/lib/ocaml/caml/alloc.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h -coq_values.d.o: kernel/byterun/coq_values.c \ - kernel/byterun/coq_fix_code.h /usr/local/lib/ocaml/caml/mlvalues.h \ - /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ - /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h \ - kernel/byterun/coq_values.h /usr/local/lib/ocaml/caml/alloc.h + /auto/demons/sacerdot/local/lib/ocaml/caml/mlvalues.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/compatibility.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/config.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/misc.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/alloc.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ + kernel/byterun/coq_memory.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/fail.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/memory.h +coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/mlvalues.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/compatibility.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/config.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/misc.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/fail.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/memory.h \ + kernel/byterun/coq_values.h \ + /auto/demons/sacerdot/local/lib/ocaml/caml/alloc.h @@ -126,7 +126,7 @@ BYTERUN=\ KERNEL=\ kernel/names.cmo kernel/univ.cmo \ - kernel/esubst.cmo kernel/term.cmo kernel/sign.cmo \ + kernel/esubst.cmo kernel/term.cmo kernel/mod_subst.cmo kernel/sign.cmo \ kernel/cbytecodes.cmo kernel/copcodes.cmo \ kernel/cemitcodes.cmo kernel/vm.cmo \ kernel/declarations.cmo kernel/environ.cmo kernel/conv_oracle.cmo \ @@ -1353,7 +1353,7 @@ GRAMMARNEEDEDCMO=\ lib/dyn.cmo lib/options.cmo lib/hashcons.cmo lib/predicate.cmo \ lib/rtree.cmo \ kernel/names.cmo kernel/univ.cmo \ - kernel/esubst.cmo kernel/term.cmo kernel/sign.cmo \ + kernel/esubst.cmo kernel/term.cmo kernel/mod_subst.cmo kernel/sign.cmo \ kernel/cbytecodes.cmo kernel/copcodes.cmo kernel/cemitcodes.cmo \ kernel/declarations.cmo kernel/environ.cmo kernel/conv_oracle.cmo \ kernel/closure.cmo kernel/reduction.cmo kernel/type_errors.cmo\ diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 78fb578e9..8c75f2df5 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -19,6 +19,7 @@ open Table open Extraction open Modutil open Common +open Mod_subst (*s Obtaining Coq environment. *) diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml index 1a40a8330..673c8e929 100644 --- a/contrib/extraction/modutil.ml +++ b/contrib/extraction/modutil.ml @@ -16,6 +16,7 @@ open Util open Miniml open Table open Mlutil +open Mod_subst (*S Functions upon modules missing in [Modops]. *) diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli index ec628b329..07425c30a 100644 --- a/contrib/extraction/modutil.mli +++ b/contrib/extraction/modutil.mli @@ -13,6 +13,7 @@ open Declarations open Environ open Libnames open Miniml +open Mod_subst (*s Functions upon modules missing in [Modops]. *) diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index 02393f1b7..94044cf20 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -21,6 +21,7 @@ open Util open Vernacinterp open Vernacexpr open Tacexpr +open Mod_subst (* Interpretation of constr's *) let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index bf4539798..1eb4783d1 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -34,6 +34,7 @@ open Pattern open Hiddentac open Nametab open Quote +open Mod_subst let mt_evd = Evd.empty let constr_of c = Constrintern.interp_constr mt_evd (Global.env()) c diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 8f9360e57..4ce07815e 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -16,6 +16,7 @@ open Nameops open Libnames open Rawterm open Term +open Mod_subst (*i*) (**********************************************************************) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 53182e34b..a3224128a 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -15,6 +15,7 @@ open Names open Libnames open Rawterm open Term +open Mod_subst (*i*) (*s This is the subtype of rawconstr allowed in syntactic extensions *) @@ -47,7 +48,7 @@ val rawconstr_of_aconstr_with_binders : loc -> (identifier -> 'a -> identifier * 'a) -> ('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr -val subst_aconstr : Names.substitution -> aconstr -> aconstr +val subst_aconstr : substitution -> aconstr -> aconstr val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 1b93dc4b6..f1c662207 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -2,6 +2,7 @@ open Names open Term open Cbytecodes open Copcodes +open Mod_subst (* Relocation information *) type reloc_info = diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index 438da15dd..ca6da65e1 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -8,7 +8,7 @@ type reloc_info = type patch = reloc_info * int (* A virer *) -val subst_patch : substitution -> patch -> patch +val subst_patch : Mod_subst.substitution -> patch -> patch type emitcodes @@ -18,7 +18,7 @@ val patch_int : emitcodes -> (*pos*)int -> int -> unit type to_patch = emitcodes * (patch list) * fv -val subst_to_patch : substitution -> to_patch -> to_patch +val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch type body_code = | BCdefined of bool*to_patch @@ -34,7 +34,7 @@ val force : to_patch_substituted -> body_code val is_boxed : to_patch_substituted -> bool -val subst_to_patch_subst : substitution -> to_patch_substituted -> to_patch_substituted +val subst_to_patch_subst : Mod_subst.substitution -> to_patch_substituted -> to_patch_substituted val to_memory : bytecodes * bytecodes * fv -> to_patch (* init code, fun code, fv *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index b5505bce3..72f37e226 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -14,6 +14,7 @@ open Names open Univ open Term open Sign +open Mod_subst (*i*) (* This module defines the types of global declarations. This includes @@ -109,7 +110,7 @@ type mutual_inductive_body = { let subst_const_body sub cb = { const_hyps = (assert (cb.const_hyps=[]); []); const_body = option_app (subst_constr_subst sub) cb.const_body; - const_type = type_app (Term.subst_mps sub) cb.const_type; + const_type = type_app (subst_mps sub) cb.const_type; const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code; (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*) const_constraints = cb.const_constraints; @@ -119,17 +120,17 @@ let subst_mind_packet sub mbp = { mind_consnames = mbp.mind_consnames; mind_typename = mbp.mind_typename; mind_nf_lc = - array_smartmap (type_app (Term.subst_mps sub)) mbp.mind_nf_lc; - mind_nf_arity = type_app (Term.subst_mps sub) mbp.mind_nf_arity; + array_smartmap (type_app (subst_mps sub)) mbp.mind_nf_lc; + mind_nf_arity = type_app (subst_mps sub) mbp.mind_nf_arity; mind_user_lc = - array_smartmap (type_app (Term.subst_mps sub)) mbp.mind_user_lc; - mind_user_arity = type_app (Term.subst_mps sub) mbp.mind_user_arity; + array_smartmap (type_app (subst_mps sub)) mbp.mind_user_lc; + mind_user_arity = type_app (subst_mps sub) mbp.mind_user_arity; mind_sort = mbp.mind_sort; mind_nrealargs = mbp.mind_nrealargs; mind_kelim = mbp.mind_kelim; mind_nparams = mbp.mind_nparams; mind_params_ctxt = - map_rel_context (Term.subst_mps sub) mbp.mind_params_ctxt; + map_rel_context (subst_mps sub) mbp.mind_params_ctxt; mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); mind_nb_constant = mbp.mind_nb_constant; mind_nb_args = mbp.mind_nb_args; diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 50c866014..30c0ffde0 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -14,6 +14,7 @@ open Univ open Term open Cemitcodes open Sign +open Mod_subst (*i*) (* This module defines the internal representation of global diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml new file mode 100644 index 000000000..ba186d06e --- /dev/null +++ b/kernel/mod_subst.ml @@ -0,0 +1,149 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +open Pp +open Util +open Names +open Term + +type substitution_domain = MSI of mod_self_id | MBI of mod_bound_id + +let string_of_subst_domain = function + MSI msid -> debug_string_of_msid msid + | MBI mbid -> debug_string_of_mbid mbid + +module Umap = Map.Make(struct + type t = substitution_domain + let compare = Pervasives.compare + end) + +(* this is correct under the condition that bound and struct + identifiers can never be identical (i.e. get the same stamp)! *) + +type substitution = module_path Umap.t + +let empty_subst = Umap.empty + +let add_msid sid = Umap.add (MSI sid) +let add_mbid bid = Umap.add (MBI bid) + +let map_msid msid mp = add_msid msid mp empty_subst +let map_mbid mbid mp = add_mbid mbid mp empty_subst + +let list_contents sub = + let one_pair uid mp l = + (string_of_subst_domain uid, string_of_mp mp)::l + in + Umap.fold one_pair sub [] + +let debug_string_of_subst sub = + let l = List.map (fun (s1,s2) -> s1^"|->"^s2) (list_contents sub) in + "{" ^ String.concat "; " l ^ "}" + +let debug_pr_subst sub = + let l = list_contents sub in + let f (s1,s2) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2) + in + str "{" ++ hov 2 (prlist_with_sep pr_coma f l) ++ str "}" + +let rec subst_mp sub mp = (* 's like subst *) + match mp with + | MPself sid -> + (try Umap.find (MSI sid) sub with Not_found -> mp) + | MPbound bid -> + (try Umap.find (MBI bid) sub with Not_found -> mp) + | MPdot (mp1,l) -> + let mp1' = subst_mp sub mp1 in + if mp1==mp1' then + mp + else + MPdot (mp1',l) + | _ -> mp + +let join subst1 subst2 = + let subst = Umap.map (subst_mp subst2) subst1 in + Umap.fold Umap.add subst2 subst + +let rec occur_in_path uid path = + match uid,path with + | MSI sid,MPself sid' -> sid = sid' + | MBI bid,MPbound bid' -> bid = bid' + | _,MPdot (mp1,_) -> occur_in_path uid mp1 + | _ -> false + +let occur_uid uid sub = + let check_one uid' mp = + if uid = uid' || occur_in_path uid mp then raise Exit + in + try + Umap.iter check_one sub; + false + with Exit -> true + +let occur_msid uid = occur_uid (MSI uid) +let occur_mbid uid = occur_uid (MBI uid) + +type 'a lazy_subst = + | LSval of 'a + | LSlazy of substitution * 'a + +type 'a substituted = 'a lazy_subst ref + +let from_val a = ref (LSval a) + +let force fsubst r = + match !r with + | LSval a -> a + | LSlazy(s,a) -> + let a' = fsubst s a in + r := LSval a'; + a' + +let subst_substituted s r = + match !r with + | LSval a -> ref (LSlazy(s,a)) + | LSlazy(s',a) -> + let s'' = join s' s in + ref (LSlazy(s'',a)) + +let subst_kn sub kn = + let mp,dir,l = repr_kn kn in + let mp' = subst_mp sub mp in + if mp==mp' then kn else make_kn mp' dir l + +let subst_con sub con = + let mp,dir,l = repr_con con in + let mp' = subst_mp sub mp in + if mp==mp' then con else make_con mp' dir l + +(* +map_kn : (kernel_name -> kernel_name) -> constr -> constr + +This should be rewritten to prevent duplication of constr's when not +necessary. +For now, it uses map_constr and is rather ineffective +*) + +let rec map_kn f f_con c = + let func = map_kn f f_con in + match kind_of_term c with + | Const kn -> + mkConst (f_con kn) + | Ind (kn,i) -> + mkInd (f kn,i) + | Construct ((kn,i),j) -> + mkConstruct ((f kn,i),j) + | Case (ci,p,c,l) -> + let ci' = { ci with ci_ind = let (kn,i) = ci.ci_ind in f kn, i } in + mkCase (ci', func p, func c, array_smartmap func l) + | _ -> map_constr func c + +let subst_mps sub = + map_kn (subst_kn sub) (subst_con sub) diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli new file mode 100644 index 000000000..fa37c2509 --- /dev/null +++ b/kernel/mod_subst.mli @@ -0,0 +1,61 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +open Names +open Term + +(*s Substitutions *) + +type substitution + +val empty_subst : substitution + +val add_msid : + mod_self_id -> module_path -> substitution -> substitution +val add_mbid : + mod_bound_id -> module_path -> substitution -> substitution + +val map_msid : mod_self_id -> module_path -> substitution +val map_mbid : mod_bound_id -> module_path -> substitution + +(* sequential composition: + [substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)] +*) +val join : substitution -> substitution -> substitution + +type 'a substituted +val from_val : 'a -> 'a substituted +val force : (substitution -> 'a -> 'a) -> 'a substituted -> 'a +val subst_substituted : substitution -> 'a substituted -> 'a substituted + +(*i debugging *) +val debug_string_of_subst : substitution -> string +val debug_pr_subst : substitution -> Pp.std_ppcmds +(*i*) + +(* [subst_mp sub mp] guarantees that whenever the result of the + substitution is structutally equal [mp], it is equal by pointers + as well [==] *) + +val subst_mp : + substitution -> module_path -> module_path + +(* [occur_*id id sub] returns true iff [id] occurs in [sub] + on either side *) + +val occur_msid : mod_self_id -> substitution -> bool +val occur_mbid : mod_bound_id -> substitution -> bool + +val subst_kn : substitution -> kernel_name -> kernel_name +val subst_con : substitution -> constant -> constant + +(* [subst_mps sub c] performs the substitution [sub] on all kernel + names appearing in [c] *) +val subst_mps : substitution -> constr -> constr diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 9f5a5e9a8..9ab200ad1 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -17,6 +17,7 @@ open Environ open Term_typing open Modops open Subtyping +open Mod_subst exception Not_path diff --git a/kernel/modops.ml b/kernel/modops.ml index aca663e7c..9aba4d560 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -17,6 +17,7 @@ open Term open Declarations open Environ open Entries +open Mod_subst (*i*) let error_existing_label l = diff --git a/kernel/modops.mli b/kernel/modops.mli index f92c6bf04..0e1d9cd34 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -15,6 +15,7 @@ open Univ open Environ open Declarations open Entries +open Mod_subst (*i*) (* Various operations on modules and module types *) diff --git a/kernel/names.ml b/kernel/names.ml index db1b1b6df..e15d4ab2f 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -138,95 +138,6 @@ end module MPset = Set.Make(MPord) module MPmap = Map.Make(MPord) - -(* this is correct under the condition that bound and struct - identifiers can never be identical (i.e. get the same stamp)! *) - -type substitution = module_path Umap.t - -let empty_subst = Umap.empty - -let add_msid = Umap.add -let add_mbid = Umap.add - -let map_msid msid mp = add_msid msid mp empty_subst -let map_mbid mbid mp = add_msid mbid mp empty_subst - -let list_contents sub = - let one_pair uid mp l = - (string_of_uid uid, string_of_mp mp)::l - in - Umap.fold one_pair sub [] - -let debug_string_of_subst sub = - let l = List.map (fun (s1,s2) -> s1^"|->"^s2) (list_contents sub) in - "{" ^ String.concat "; " l ^ "}" - -let debug_pr_subst sub = - let l = list_contents sub in - let f (s1,s2) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2) - in - str "{" ++ hov 2 (prlist_with_sep pr_coma f l) ++ str "}" - -let rec subst_mp sub mp = (* 's like subst *) - match mp with - | MPself sid -> - (try Umap.find sid sub with Not_found -> mp) - | MPbound bid -> - (try Umap.find bid sub with Not_found -> mp) - | MPdot (mp1,l) -> - let mp1' = subst_mp sub mp1 in - if mp1==mp1' then - mp - else - MPdot (mp1',l) - | _ -> mp - -let join subst1 subst2 = - let subst = Umap.map (subst_mp subst2) subst1 in - Umap.fold Umap.add subst2 subst - -let rec occur_in_path uid = function - | MPself sid -> sid = uid - | MPbound bid -> bid = uid - | MPdot (mp1,_) -> occur_in_path uid mp1 - | _ -> false - -let occur_uid uid sub = - let check_one uid' mp = - if uid = uid' || occur_in_path uid mp then raise Exit - in - try - Umap.iter check_one sub; - false - with Exit -> true - -let occur_msid = occur_uid -let occur_mbid = occur_uid - -type 'a lazy_subst = - | LSval of 'a - | LSlazy of substitution * 'a - -type 'a substituted = 'a lazy_subst ref - -let from_val a = ref (LSval a) - -let force fsubst r = - match !r with - | LSval a -> a - | LSlazy(s,a) -> - let a' = fsubst s a in - r := LSval a'; - a' - -let subst_substituted s r = - match !r with - | LSval a -> ref (LSlazy(s,a)) - | LSlazy(s',a) -> - let s'' = join s' s in - ref (LSlazy(s'',a)) - (* Kernel names *) type kernel_name = module_path * dir_path * label @@ -246,11 +157,6 @@ let string_of_kn (mp,dir,l) = let pr_kn kn = str (string_of_kn kn) -let subst_kn sub (mp,dir,l as kn) = - let mp' = subst_mp sub mp in - if mp==mp' then kn else (mp',dir,l) - - let kn_ord kn1 kn2 = let mp1,dir1,l1 = kn1 in let mp2,dir2,l2 = kn2 in @@ -298,7 +204,6 @@ let string_of_con = string_of_kn let con_label = label let pr_con = pr_kn let con_modpath = modpath -let subst_con = subst_kn let ith_mutual_inductive (kn,_) i = (kn,i) let ith_constructor_of_inductive ind i = (ind,i) diff --git a/kernel/names.mli b/kernel/names.mli index 8cda7d958..4350b231a 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -83,50 +83,6 @@ val string_of_mp : module_path -> string module MPset : Set.S with type elt = module_path module MPmap : Map.S with type key = module_path - -(*s Substitutions *) - -type substitution - -val empty_subst : substitution - -val add_msid : - mod_self_id -> module_path -> substitution -> substitution -val add_mbid : - mod_bound_id -> module_path -> substitution -> substitution - -val map_msid : mod_self_id -> module_path -> substitution -val map_mbid : mod_bound_id -> module_path -> substitution - -(* sequential composition: - [substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)] -*) -val join : substitution -> substitution -> substitution - -type 'a substituted -val from_val : 'a -> 'a substituted -val force : (substitution -> 'a -> 'a) -> 'a substituted -> 'a -val subst_substituted : substitution -> 'a substituted -> 'a substituted - -(*i debugging *) -val debug_string_of_subst : substitution -> string -val debug_pr_subst : substitution -> Pp.std_ppcmds -(*i*) - -(* [subst_mp sub mp] guarantees that whenever the result of the - substitution is structutally equal [mp], it is equal by pointers - as well [==] *) - -val subst_mp : - substitution -> module_path -> module_path - -(* [occur_*id id sub] returns true iff [id] occurs in [sub] - on either side *) - -val occur_msid : mod_self_id -> substitution -> bool -val occur_mbid : mod_bound_id -> substitution -> bool - - (* Name of the toplevel structure *) val initial_msid : mod_self_id val initial_path : module_path (* [= MPself initial_msid] *) @@ -147,7 +103,6 @@ val label : kernel_name -> label val string_of_kn : kernel_name -> string val pr_kn : kernel_name -> Pp.std_ppcmds -val subst_kn : substitution -> kernel_name -> kernel_name module KNset : Set.S with type elt = kernel_name @@ -176,7 +131,6 @@ val string_of_con : constant -> string val con_label : constant -> label val con_modpath : constant -> module_path val pr_con : constant -> Pp.std_ppcmds -val subst_con : substitution -> constant -> constant val ith_mutual_inductive : inductive -> int -> inductive val ith_constructor_of_inductive : inductive -> int -> constructor diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 2f39dc61a..383f7c2c9 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -18,6 +18,7 @@ open Environ open Reduction open Inductive open Modops +open Mod_subst (*i*) (* This local type is used to subtype a constant with a constructor or diff --git a/kernel/term.ml b/kernel/term.ml index 21ab2ea5d..65bf7a565 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -790,32 +790,6 @@ let substn_vars p vars = let subst_vars = substn_vars 1 -(* -map_kn : (kernel_name -> kernel_name) -> constr -> constr - -This should be rewritten to prevent duplication of constr's when not -necessary. -For now, it uses map_constr and is rather ineffective -*) - -let rec map_kn f f_con c = - let func = map_kn f f_con in - match kind_of_term c with - | Const kn -> - mkConst (f_con kn) - | Ind (kn,i) -> - mkInd (f kn,i) - | Construct ((kn,i),j) -> - mkConstruct ((f kn,i),j) - | Case (ci,p,c,l) -> - let ci' = { ci with ci_ind = let (kn,i) = ci.ci_ind in f kn, i } in - mkCase (ci', func p, func c, array_smartmap func l) - | _ -> map_constr func c - -let subst_mps sub = - map_kn (subst_kn sub) (subst_con sub) - - (*********************) (* Term constructors *) (*********************) diff --git a/kernel/term.mli b/kernel/term.mli index 2b84f79ba..c9ac9419c 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -460,11 +460,6 @@ val subst_vars : identifier list -> constr -> constr val substn_vars : int -> identifier list -> constr -> constr -(* [subst_mps sub c] performs the substitution [sub] on all kernel - names appearing in [c] *) -val subst_mps : substitution -> constr -> constr - - (*s Functionals working on the immediate subterm of a construction *) (* [fold_constr f acc c] folds [f] on the immediate subterms of [c] diff --git a/library/declaremods.ml b/library/declaremods.ml index fc11169e8..e1a27314f 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -17,6 +17,7 @@ open Libnames open Libobject open Lib open Nametab +open Mod_subst (* modules and components *) diff --git a/library/goptions.ml b/library/goptions.ml index cabd364ef..43c4da14a 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -17,6 +17,7 @@ open Names open Libnames open Term open Nametab +open Mod_subst (****************************************************************************) (* 0- Common things *) diff --git a/library/goptions.mli b/library/goptions.mli index 46c5bf2e2..4709fc1c8 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -59,6 +59,7 @@ open Names open Libnames open Term open Nametab +open Mod_subst (*i*) (*s Things common to tables and options. *) diff --git a/library/lib.mli b/library/lib.mli index 438754a38..4411bcbb6 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -14,6 +14,7 @@ open Names open Libnames open Libobject open Summary +open Mod_subst (*i*) (*s This module provides a general mechanism to keep a trace of all operations diff --git a/library/libnames.ml b/library/libnames.ml index 2fe8f724c..fd5bb2196 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -13,6 +13,7 @@ open Util open Names open Nameops open Term +open Mod_subst type global_reference = | VarRef of variable diff --git a/library/libnames.mli b/library/libnames.mli index 539aa0b96..b2c32f89b 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -13,6 +13,7 @@ open Pp open Util open Names open Term +open Mod_subst (*i*) (*s Global reference is a kernel side type for all references together *) diff --git a/library/libobject.ml b/library/libobject.ml index bd5ec7fb1..25d5a329f 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -11,6 +11,7 @@ open Util open Names open Libnames +open Mod_subst (* The relax flag is used to make it possible to load files while ignoring failures to incorporate some objects. This can be useful when one diff --git a/library/libobject.mli b/library/libobject.mli index 8b38911ea..562ba0ce4 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -11,6 +11,7 @@ (*i*) open Names open Libnames +open Mod_subst (*i*) (* [Libobject] declares persistent objects, given with methods: diff --git a/parsing/ast.mli b/parsing/ast.mli index 28e8e132f..b915c6552 100755 --- a/parsing/ast.mli +++ b/parsing/ast.mli @@ -16,6 +16,7 @@ open Libnames open Coqast open Topconstr open Genarg +open Mod_subst (*i*) (* Abstract syntax trees. *) @@ -120,4 +121,4 @@ val first_matchl : ('a -> patlist) -> env -> Coqast.t list -> 'a list -> val to_pat : entry_env -> Coqast.t -> (astpat * entry_env) (* Object substitution in modules *) -val subst_astpat : Names.substitution -> astpat -> astpat +val subst_astpat : substitution -> astpat -> astpat diff --git a/parsing/coqast.ml b/parsing/coqast.ml index 52681fe34..a80982f8a 100644 --- a/parsing/coqast.ml +++ b/parsing/coqast.ml @@ -12,6 +12,7 @@ open Util open Names open Libnames +open Mod_subst (*i*) type t = @@ -116,11 +117,11 @@ let rec subst_ast subst ast = match ast with if ast1' == ast1 then ast else Smetalam (l,s,ast1') | Path (loc,kn) -> - let kn' = Names.subst_kn subst kn in + let kn' = subst_kn subst kn in if kn' == kn then ast else Path(loc,kn') | ConPath (loc,kn) -> - let kn' = Names.subst_con subst kn in + let kn' = subst_con subst kn in if kn' == kn then ast else ConPath(loc,kn') | Nmeta _ diff --git a/parsing/coqast.mli b/parsing/coqast.mli index fcb029319..a769c66f9 100644 --- a/parsing/coqast.mli +++ b/parsing/coqast.mli @@ -12,6 +12,7 @@ open Util open Names open Libnames +open Mod_subst (*i*) (* Abstract syntax trees. *) @@ -42,7 +43,7 @@ val hcons_ast: * (kernel_name -> kernel_name) * (constant -> constant) -> (t -> t) * (loc -> loc) -val subst_ast: Names.substitution -> t -> t +val subst_ast: substitution -> t -> t (* val map_tactic_expr : (t -> t) -> (tactic_expr -> tactic_expr) -> tactic_expr -> tactic_expr diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index 58a889348..b6844e547 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -16,6 +16,7 @@ open Coqast open Vernacexpr open Extend open Rawterm +open Mod_subst (*i*) type all_grammar_command = @@ -48,7 +49,7 @@ val get_extend_vernac_grammars : val reset_extend_grammars_v8 : unit -> unit val subst_all_grammar_command : - Names.substitution -> all_grammar_command -> all_grammar_command + substitution -> all_grammar_command -> all_grammar_command val interp_entry_name : string -> string -> entry_type * Token.t Gramext.g_symbol diff --git a/parsing/extend.mli b/parsing/extend.mli index d8f0827db..c9558a970 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -17,6 +17,7 @@ open Coqast open Ppextend open Topconstr open Genarg +open Mod_subst (*i*) type entry_type = argument_type @@ -98,7 +99,7 @@ val rename_command_entry : string -> string val explicitize_entry : string -> string -> constr_entry val subst_grammar_command : - Names.substitution -> grammar_command -> grammar_command + substitution -> grammar_command -> grammar_command (* unparsing objects *) @@ -113,7 +114,7 @@ type 'pat unparsing_hunk = | UNP_SYMBOLIC of string option * string * 'pat unparsing_hunk (*val subst_unparsing_hunk : - Names.substitution -> (Names.substitution -> 'pat -> 'pat) -> + substitution -> (substitution -> 'pat -> 'pat) -> 'pat unparsing_hunk -> 'pat unparsing_hunk *) @@ -130,8 +131,8 @@ type 'pat syntax_entry = { syn_hunks : 'pat unparsing_hunk list } val subst_syntax_entry : - (Names.substitution -> 'pat -> 'pat) -> - Names.substitution -> 'pat syntax_entry -> 'pat syntax_entry + (substitution -> 'pat -> 'pat) -> + substitution -> 'pat syntax_entry -> 'pat syntax_entry type 'pat syntax_command = { @@ -139,8 +140,8 @@ type 'pat syntax_command = { sc_entries : 'pat syntax_entry list } val subst_syntax_command : - (Names.substitution -> 'pat -> 'pat) -> - Names.substitution -> 'pat syntax_command -> 'pat syntax_command + (substitution -> 'pat -> 'pat) -> + substitution -> 'pat syntax_command -> 'pat syntax_command type syntax_rule = string * Coqast.t * Coqast.t unparsing_hunk list type raw_syntax_entry = precedence * syntax_rule list diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 7fb1bb2cc..aef35cd7c 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -21,6 +21,7 @@ open Term open Termops open Rawterm open Decl_kinds +open Mod_subst (* usage qque peu general: utilise aussi dans record *) diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 0ce44b507..c1590f6a8 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -15,6 +15,7 @@ open Term open Evd open Environ open Nametab +open Mod_subst (*i*) (*s This is the type of class kinds *) diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 981692ebd..4b8ed1ed1 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -26,6 +26,7 @@ open Tacred open Pretype_errors open Evarutil open Unification +open Mod_subst (* *) let w_coerce env c ctyp target evd = diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 0c19a60f9..3208bd593 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -16,6 +16,7 @@ open Sign open Environ open Evd open Evarutil +open Mod_subst (*i*) (***************************************************************) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 26b646bdd..6a0ea0060 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -24,6 +24,7 @@ open Termops open Libnames open Nametab open Evd +open Mod_subst (****************************************************************************) (* Tools for printing of Cases *) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 5c0f42852..8bbf48d59 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -17,6 +17,7 @@ open Termops open Sign open Environ open Libnames +open Mod_subst (* The type of mappings for existential variables *) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 9f10d2dfe..fff6808d1 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -14,6 +14,7 @@ open Names open Term open Sign open Libnames +open Mod_subst (*i*) (* The type of mappings for existential variables. diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 5cb07e219..243da5cc1 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -17,6 +17,7 @@ open Rawterm open Environ open Nametab open Pp +open Mod_subst (* Metavariables *) diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index 3d2bd7214..398117303 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -17,6 +17,7 @@ open Environ open Libnames open Nametab open Rawterm +open Mod_subst (*i*) (* Pattern variables *) diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index d93a583c4..48b41444e 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -16,6 +16,7 @@ open Term open Libnames open Nametab open Evd +open Mod_subst (*i*) (* Untyped intermediate terms, after ASTs and before constr. *) diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 7e8b8b894..0a582ef7b 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -15,6 +15,7 @@ open Sign open Term open Libnames open Nametab +open Mod_subst (*i*) (* Untyped intermediate terms, after ASTs and before constr. *) @@ -99,7 +100,7 @@ val occur_rawconstr : identifier -> rawconstr -> bool val loc_of_rawconstr : rawconstr -> loc -val subst_raw : Names.substitution -> rawconstr -> rawconstr +val subst_raw : substitution -> rawconstr -> rawconstr type 'a raw_red_flag = { rBeta : bool; diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 6d7921f0d..64d99d49f 100755 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -19,6 +19,7 @@ open Typeops open Libobject open Library open Classops +open Mod_subst (*s Une structure S est un type inductif non récursif à un seul constructeur (de nom par défaut Build_S) *) diff --git a/tactics/auto.ml b/tactics/auto.ml index 45fc35d4b..9bf5cc741 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -39,6 +39,7 @@ open Library open Printer open Declarations open Tacexpr +open Mod_subst (****************************************************************************) (* The Type of Constructions Autotactic Hints *) @@ -291,21 +292,21 @@ let cache_autohint (_,(local,name,hintlist)) = add_hint name hintlist let recalc_hint ((_,data) as hint) = match data.code with | Res_pf (c,_) -> - let c' = Term.subst_mps subst c in + let c' = subst_mps subst c in if c==c' then hint else make_apply_entry env sigma (false,false) data.hname (c', type_of env sigma c') | ERes_pf (c,_) -> - let c' = Term.subst_mps subst c in + let c' = subst_mps subst c in if c==c' then hint else make_apply_entry env sigma (true,false) data.hname (c', type_of env sigma c') | Give_exact c -> - let c' = Term.subst_mps subst c in + let c' = subst_mps subst c in if c==c' then hint else make_exact_entry data.hname (c',type_of env sigma c') | Res_pf_THEN_trivial_fail (c,_) -> - let c' = Term.subst_mps subst c in + let c' = subst_mps subst c in if c==c' then hint else make_trivial env sigma (data.hname,c') | Unfold_nth ref -> @@ -335,19 +336,19 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) = let lab' = subst_label subst lab in let data' = match data.code with | Res_pf (c, clenv) -> - let c' = Term.subst_mps subst c in + let c' = subst_mps subst c in if c==c' then data else trans_data data (Res_pf (c', trans_clenv clenv)) | ERes_pf (c, clenv) -> - let c' = Term.subst_mps subst c in + let c' = subst_mps subst c in if c==c' then data else trans_data data (ERes_pf (c', trans_clenv clenv)) | Give_exact c -> - let c' = Term.subst_mps subst c in + let c' = subst_mps subst c in if c==c' then data else trans_data data (Give_exact c') | Res_pf_THEN_trivial_fail (c, clenv) -> - let c' = Term.subst_mps subst c in + let c' = subst_mps subst c in if c==c' then data else let code' = Res_pf_THEN_trivial_fail (c', trans_clenv clenv) in trans_data data code' diff --git a/tactics/auto.mli b/tactics/auto.mli index 950e272bc..68a8a3ba9 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -21,6 +21,7 @@ open Environ open Evd open Libnames open Vernacexpr +open Mod_subst (*i*) type auto_tactic = @@ -126,7 +127,7 @@ val set_extern_intern_tac : -> unit val set_extern_subst_tactic : - (Names.substitution -> Tacexpr.glob_tactic_expr -> Tacexpr.glob_tactic_expr) + (substitution -> Tacexpr.glob_tactic_expr -> Tacexpr.glob_tactic_expr) -> unit (* Create a Hint database from the pairs (name, constr). diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 6b6536ec4..addf30bc4 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -20,6 +20,7 @@ open Term open Util open Vernacinterp open Tacexpr +open Mod_subst (* Rewriting rules *) (* the type is the statement of the lemma constr. Used to elim duplicates. *) @@ -88,7 +89,7 @@ let export_hintrewrite x = Some x let subst_hintrewrite (_,subst,(rbase,list as node)) = let subst_first (cst,typ,b,t as pair) = - let cst' = Term.subst_mps subst cst in + let cst' = subst_mps subst cst in let typ' = (* here we do not have the environment and Global.env () is not the one where cst' lives in. Thus we can just put a dummy value and diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index e278ec243..f25687391 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -31,6 +31,7 @@ open Safe_typing open Nametab open Decl_kinds open Constrintern +open Mod_subst let replace = ref (fun _ _ -> assert false) let register_replace f = replace := f diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index d447a97e8..5a33f89f3 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -41,6 +41,7 @@ open Typing open Hiddentac open Genarg open Decl_kinds +open Mod_subst let strip_meta id = (* For Grammar v7 compatibility *) let s = string_of_id id in @@ -312,7 +313,7 @@ type interp_genarg_type = (glob_sign -> raw_generic_argument -> glob_generic_argument) * (interp_sign -> goal sigma -> glob_generic_argument -> closed_generic_argument) * - (Names.substitution -> glob_generic_argument -> glob_generic_argument) + (substitution -> glob_generic_argument -> glob_generic_argument) let extragenargtab = ref (Gmap.empty : (string,interp_genarg_type) Gmap.t) diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index f12960358..8d8d12fb4 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -19,6 +19,7 @@ open Term open Tacexpr open Genarg open Topconstr +open Mod_subst (*i*) (* Values for interpretation *) @@ -78,7 +79,7 @@ val add_interp_genarg : (glob_sign -> raw_generic_argument -> glob_generic_argument) * (interp_sign -> goal sigma -> glob_generic_argument -> closed_generic_argument) * - (Names.substitution -> glob_generic_argument -> glob_generic_argument) + (substitution -> glob_generic_argument -> glob_generic_argument) -> unit val interp_genarg : @@ -94,10 +95,10 @@ val intern_hyp : glob_sign -> identifier Util.located -> identifier Util.located val subst_genarg : - Names.substitution -> glob_generic_argument -> glob_generic_argument + substitution -> glob_generic_argument -> glob_generic_argument val subst_rawconstr : - Names.substitution -> rawconstr_and_expr -> rawconstr_and_expr + substitution -> rawconstr_and_expr -> rawconstr_and_expr (* Interprets any expression *) val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> value |