diff options
50 files changed, 1047 insertions, 845 deletions
@@ -15,10 +15,10 @@ 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/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 +kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \ + kernel/environ.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 @@ -37,17 +37,16 @@ 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 lib/pp.cmi: lib/pp_control.cmi -lib/rtree.cmi: lib/pp.cmi -lib/system.cmi: lib/pp.cmi -lib/util.cmi: lib/pp.cmi -library/declare.cmi: kernel/cooking.cmi kernel/declarations.cmi \ - kernel/entries.cmi kernel/indtypes.cmi library/libnames.cmi \ - library/libobject.cmi library/library.cmi kernel/names.cmi \ - library/nametab.cmi kernel/safe_typing.cmi kernel/sign.cmi \ - kernel/term.cmi kernel/univ.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 \ + library/library.cmi kernel/names.cmi library/nametab.cmi \ + kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi library/declaremods.cmi: kernel/entries.cmi kernel/environ.cmi \ library/lib.cmi library/libnames.cmi library/libobject.cmi \ kernel/names.cmi lib/pp.cmi kernel/safe_typing.cmi +library/dischargedhypsmap.cmi: kernel/environ.cmi library/libnames.cmi \ + library/nametab.cmi kernel/term.cmi 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 \ @@ -67,6 +66,9 @@ library/nameops.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ library/nametab.cmi: library/libnames.cmi kernel/names.cmi lib/pp.cmi \ kernel/sign.cmi lib/util.cmi library/summary.cmi: library/libnames.cmi kernel/names.cmi +lib/rtree.cmi: lib/pp.cmi +lib/system.cmi: lib/pp.cmi +lib/util.cmi: lib/pp.cmi parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi parsing/genarg.cmi \ library/libnames.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi parsing/astmod.cmi: parsing/coqast.cmi kernel/declarations.cmi \ @@ -86,15 +88,16 @@ parsing/esyntax.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \ parsing/genarg.cmi lib/pp.cmi parsing/symbols.cmi toplevel/vernacexpr.cmo parsing/extend.cmi: parsing/ast.cmi parsing/coqast.cmi kernel/names.cmi \ lib/pp.cmi -parsing/g_minicoq.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ - kernel/term.cmi -parsing/g_zsyntax.cmi: parsing/coqast.cmi parsing/genarg.cmi: kernel/closure.cmi parsing/coqast.cmi pretyping/evd.cmi \ library/libnames.cmi kernel/names.cmi pretyping/rawterm.cmi \ kernel/term.cmi lib/util.cmi -parsing/pcoq.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/genarg.cmi \ - library/libnames.cmi kernel/names.cmi pretyping/rawterm.cmi \ - proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmo +parsing/g_minicoq.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ + kernel/term.cmi +parsing/g_zsyntax.cmi: parsing/coqast.cmi +parsing/pcoq.cmi: parsing/ast.cmi parsing/coqast.cmi library/decl_kinds.cmo \ + parsing/genarg.cmi library/libnames.cmi kernel/names.cmi \ + pretyping/rawterm.cmi proofs/tacexpr.cmo lib/util.cmi \ + toplevel/vernacexpr.cmo parsing/ppconstr.cmi: parsing/coqast.cmi kernel/environ.cmi \ parsing/extend.cmi parsing/genarg.cmi library/libnames.cmi \ parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo \ @@ -125,9 +128,10 @@ pretyping/cases.cmi: kernel/environ.cmi pretyping/evarutil.cmi \ pretyping/rawterm.cmi kernel/term.cmi pretyping/cbv.cmi: kernel/closure.cmi kernel/environ.cmi kernel/esubst.cmi \ kernel/names.cmi kernel/term.cmi -pretyping/classops.cmi: library/declare.cmi kernel/environ.cmi \ - pretyping/evd.cmi library/libnames.cmi library/libobject.cmi \ - kernel/names.cmi library/nametab.cmi lib/pp.cmi kernel/term.cmi +pretyping/classops.cmi: library/decl_kinds.cmo library/declare.cmi \ + kernel/environ.cmi pretyping/evd.cmi library/libnames.cmi \ + library/libobject.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ + kernel/term.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 @@ -185,17 +189,17 @@ proofs/evar_refiner.cmi: parsing/coqast.cmi kernel/environ.cmi \ proofs/refiner.cmi kernel/sign.cmi kernel/term.cmi proofs/logic.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \ lib/pp.cmi proofs/proof_type.cmi kernel/sign.cmi kernel/term.cmi -proofs/pfedit.cmi: parsing/coqast.cmi kernel/entries.cmi kernel/environ.cmi \ - pretyping/evd.cmi library/libnames.cmi kernel/names.cmi \ - library/nametab.cmi lib/pp.cmi proofs/proof_type.cmi kernel/sign.cmi \ - proofs/tacmach.cmi kernel/term.cmi +proofs/pfedit.cmi: parsing/coqast.cmi library/decl_kinds.cmo \ + kernel/entries.cmi kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \ + lib/pp.cmi proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi \ + kernel/term.cmi proofs/proof_trees.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \ lib/pp.cmi proofs/proof_type.cmi kernel/sign.cmi kernel/term.cmi \ lib/util.cmi -proofs/proof_type.cmi: kernel/closure.cmi kernel/environ.cmi \ - pretyping/evd.cmi parsing/genarg.cmi library/libnames.cmi \ - kernel/names.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo kernel/term.cmi \ - lib/util.cmi +proofs/proof_type.cmi: kernel/closure.cmi library/decl_kinds.cmo \ + kernel/environ.cmi pretyping/evd.cmi parsing/genarg.cmi \ + library/libnames.cmi kernel/names.cmi pretyping/rawterm.cmi \ + proofs/tacexpr.cmo kernel/term.cmi lib/util.cmi proofs/refiner.cmi: pretyping/evd.cmi lib/pp.cmi proofs/proof_trees.cmi \ proofs/proof_type.cmi kernel/sign.cmi proofs/tacexpr.cmo kernel/term.cmi proofs/tacmach.cmi: kernel/closure.cmi parsing/coqast.cmi kernel/environ.cmi \ @@ -263,14 +267,14 @@ tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi pretyping/evd.cmi kernel/names.cmi \ proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi toplevel/cerrors.cmi: parsing/coqast.cmi lib/pp.cmi -toplevel/class.cmi: pretyping/classops.cmi library/declare.cmi \ - library/libnames.cmi kernel/names.cmi library/nametab.cmi \ - proofs/proof_type.cmi kernel/term.cmi -toplevel/command.cmi: parsing/coqast.cmi library/declare.cmi \ - kernel/entries.cmi kernel/environ.cmi pretyping/evd.cmi \ - library/libnames.cmi library/library.cmi kernel/names.cmi \ - library/nametab.cmi proofs/proof_type.cmi pretyping/tacred.cmi \ - kernel/term.cmi lib/util.cmi toplevel/vernacexpr.cmo +toplevel/class.cmi: pretyping/classops.cmi library/decl_kinds.cmo \ + library/declare.cmi library/libnames.cmi kernel/names.cmi \ + library/nametab.cmi proofs/proof_type.cmi kernel/term.cmi +toplevel/command.cmi: parsing/coqast.cmi library/decl_kinds.cmo \ + library/declare.cmi kernel/entries.cmi kernel/environ.cmi \ + pretyping/evd.cmi library/libnames.cmi library/library.cmi \ + kernel/names.cmi library/nametab.cmi proofs/proof_type.cmi \ + pretyping/tacred.cmi kernel/term.cmi lib/util.cmi toplevel/vernacexpr.cmo toplevel/coqinit.cmi: kernel/names.cmi toplevel/discharge.cmi: kernel/names.cmi toplevel/fhimsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ @@ -289,21 +293,21 @@ toplevel/recordobj.cmi: library/libnames.cmi proofs/proof_type.cmi toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \ kernel/term.cmi toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi -toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi \ - toplevel/vernacexpr.cmo toplevel/vernacentries.cmi: parsing/coqast.cmi kernel/environ.cmi \ pretyping/evd.cmi library/libnames.cmi kernel/names.cmi kernel/term.cmi \ lib/util.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernacinterp.cmi: proofs/tacexpr.cmo +toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi \ + toplevel/vernacexpr.cmo 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: parsing/coqast.cmi kernel/names.cmi \ contrib/correctness/ptype.cmi kernel/term.cmi -contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \ - pretyping/rawterm.cmi contrib/correctness/pcicenv.cmi: kernel/names.cmi \ contrib/correctness/penv.cmi contrib/correctness/prename.cmi \ kernel/sign.cmi kernel/term.cmi +contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \ + pretyping/rawterm.cmi contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/past.cmi \ contrib/correctness/ptype.cmi contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi @@ -392,8 +396,9 @@ contrib/jprover/jall.cmi: contrib/jprover/jlogic.cmi \ contrib/jprover/jterm.cmi contrib/jprover/opname.cmi contrib/jprover/jlogic.cmi: contrib/jprover/jterm.cmi contrib/jprover/jterm.cmi: contrib/jprover/opname.cmi -contrib/xml/xmlcommand.cmi: library/libnames.cmi kernel/names.cmi \ - lib/util.cmi +contrib/xml/doubleTypeInference.cmi: contrib/xml/acic.cmo kernel/environ.cmi \ + pretyping/evd.cmi kernel/term.cmi +contrib/xml/xmlcommand.cmi: library/libnames.cmi lib/util.cmi config/coq_config.cmo: config/coq_config.cmi config/coq_config.cmx: config/coq_config.cmi dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi @@ -454,6 +459,12 @@ 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/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \ + kernel/environ.cmi kernel/names.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 kernel/term.cmx kernel/univ.cmx \ + lib/util.cmx kernel/modops.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 \ @@ -462,12 +473,6 @@ 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 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 kernel/term.cmx kernel/univ.cmx \ - lib/util.cmx kernel/modops.cmi kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/predicate.cmi lib/util.cmi \ kernel/names.cmi kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/predicate.cmx lib/util.cmx \ @@ -550,47 +555,39 @@ 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 lib/hashcons.cmx: lib/hashcons.cmi lib/options.cmo: lib/util.cmi lib/options.cmi lib/options.cmx: lib/util.cmx lib/options.cmi -lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi -lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi lib/pp_control.cmo: lib/pp_control.cmi lib/pp_control.cmx: lib/pp_control.cmi +lib/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/pp.cmi lib/util.cmi -lib/util.cmx: lib/pp.cmx lib/util.cmi -library/declare.cmo: kernel/declarations.cmi kernel/entries.cmi \ - kernel/environ.cmi library/global.cmi library/impargs.cmi \ - kernel/indtypes.cmi kernel/inductive.cmi library/lib.cmi \ - library/libnames.cmi library/libobject.cmi library/library.cmi \ - library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.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 \ + kernel/inductive.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 lib/pp.cmi \ kernel/reduction.cmi kernel/safe_typing.cmi kernel/sign.cmi \ library/summary.cmi kernel/term.cmi kernel/type_errors.cmi \ kernel/typeops.cmi kernel/univ.cmi lib/util.cmi library/declare.cmi -library/declare.cmx: kernel/declarations.cmx kernel/entries.cmx \ - kernel/environ.cmx library/global.cmx library/impargs.cmx \ - kernel/indtypes.cmx kernel/inductive.cmx library/lib.cmx \ - library/libnames.cmx library/libobject.cmx library/library.cmx \ - library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ +library/declare.cmx: library/decl_kinds.cmx kernel/declarations.cmx \ + library/dischargedhypsmap.cmx kernel/entries.cmx kernel/environ.cmx \ + library/global.cmx library/impargs.cmx kernel/indtypes.cmx \ + kernel/inductive.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 lib/pp.cmx \ kernel/reduction.cmx kernel/safe_typing.cmx kernel/sign.cmx \ library/summary.cmx kernel/term.cmx kernel/type_errors.cmx \ kernel/typeops.cmx kernel/univ.cmx lib/util.cmx library/declare.cmi @@ -604,6 +601,16 @@ library/declaremods.cmx: kernel/declarations.cmx kernel/entries.cmx \ library/libnames.cmx library/libobject.cmx kernel/modops.cmx \ kernel/names.cmx library/nametab.cmx lib/pp.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 \ + kernel/reduction.cmi library/summary.cmi kernel/term.cmi lib/util.cmi \ + library/dischargedhypsmap.cmi +library/dischargedhypsmap.cmx: kernel/declarations.cmx kernel/environ.cmx \ + kernel/inductive.cmx library/lib.cmx library/libnames.cmx \ + library/libobject.cmx kernel/names.cmx library/nametab.cmx \ + kernel/reduction.cmx library/summary.cmx kernel/term.cmx lib/util.cmx \ + library/dischargedhypsmap.cmi library/global.cmo: kernel/environ.cmi kernel/inductive.cmi \ library/libnames.cmi kernel/names.cmi kernel/safe_typing.cmi \ kernel/sign.cmi library/summary.cmi kernel/term.cmi lib/util.cmi \ @@ -670,6 +677,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/pp.cmi lib/util.cmi +lib/util.cmx: lib/pp.cmx lib/util.cmi parsing/argextend.cmo: parsing/ast.cmi parsing/genarg.cmi parsing/pcoq.cmi \ parsing/q_coqast.cmo parsing/q_util.cmi lib/util.cmi \ toplevel/vernacexpr.cmo @@ -756,6 +773,12 @@ parsing/g_constr.cmo: parsing/ast.cmi parsing/coqast.cmi kernel/names.cmi \ parsing/pcoq.cmi parsing/g_constr.cmx: parsing/ast.cmx parsing/coqast.cmx kernel/names.cmx \ parsing/pcoq.cmx +parsing/genarg.cmo: parsing/coqast.cmi pretyping/evd.cmi kernel/names.cmi \ + library/nametab.cmi pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi \ + parsing/genarg.cmi +parsing/genarg.cmx: parsing/coqast.cmx pretyping/evd.cmx kernel/names.cmx \ + library/nametab.cmx pretyping/rawterm.cmx kernel/term.cmx lib/util.cmx \ + parsing/genarg.cmi parsing/g_ltac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/genarg.cmi \ kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi \ proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmo @@ -807,13 +830,13 @@ parsing/g_tactic.cmx: parsing/ast.cmx parsing/genarg.cmx kernel/names.cmx \ parsing/pcoq.cmx lib/pp.cmx pretyping/rawterm.cmx proofs/tacexpr.cmx \ lib/util.cmx parsing/g_vernac.cmo: parsing/ast.cmi toplevel/class.cmi parsing/coqast.cmi \ - library/declare.cmi parsing/genarg.cmi library/goptions.cmi \ - library/libnames.cmi lib/options.cmi parsing/pcoq.cmi lib/pp.cmi \ - toplevel/recordobj.cmi lib/util.cmi toplevel/vernacexpr.cmo + library/decl_kinds.cmo parsing/genarg.cmi library/goptions.cmi \ + lib/options.cmi parsing/pcoq.cmi lib/pp.cmi toplevel/recordobj.cmi \ + lib/util.cmi toplevel/vernacexpr.cmo parsing/g_vernac.cmx: parsing/ast.cmx toplevel/class.cmx parsing/coqast.cmx \ - library/declare.cmx parsing/genarg.cmx library/goptions.cmx \ - library/libnames.cmx lib/options.cmx parsing/pcoq.cmx lib/pp.cmx \ - toplevel/recordobj.cmx lib/util.cmx toplevel/vernacexpr.cmx + library/decl_kinds.cmx parsing/genarg.cmx library/goptions.cmx \ + lib/options.cmx parsing/pcoq.cmx lib/pp.cmx toplevel/recordobj.cmx \ + lib/util.cmx toplevel/vernacexpr.cmx parsing/g_zsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi lib/bignat.cmi \ parsing/coqast.cmi parsing/esyntax.cmi parsing/extend.cmi \ library/libnames.cmi library/library.cmi kernel/names.cmi \ @@ -824,20 +847,14 @@ parsing/g_zsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx lib/bignat.cmx \ library/libnames.cmx library/library.cmx kernel/names.cmx \ parsing/pcoq.cmx lib/pp.cmx pretyping/rawterm.cmx parsing/symbols.cmx \ lib/util.cmx parsing/g_zsyntax.cmi -parsing/genarg.cmo: parsing/coqast.cmi pretyping/evd.cmi kernel/names.cmi \ - library/nametab.cmi pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi \ - parsing/genarg.cmi -parsing/genarg.cmx: parsing/coqast.cmx pretyping/evd.cmx kernel/names.cmx \ - library/nametab.cmx pretyping/rawterm.cmx kernel/term.cmx lib/util.cmx \ - parsing/genarg.cmi parsing/lexer.cmo: parsing/lexer.cmi parsing/lexer.cmx: parsing/lexer.cmi -parsing/pcoq.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/genarg.cmi \ - parsing/lexer.cmi lib/options.cmi lib/pp.cmi proofs/tacexpr.cmo \ - lib/util.cmi toplevel/vernacexpr.cmo parsing/pcoq.cmi -parsing/pcoq.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/genarg.cmx \ - parsing/lexer.cmx lib/options.cmx lib/pp.cmx proofs/tacexpr.cmx \ - lib/util.cmx toplevel/vernacexpr.cmx parsing/pcoq.cmi +parsing/pcoq.cmo: parsing/ast.cmi parsing/coqast.cmi library/decl_kinds.cmo \ + parsing/genarg.cmi parsing/lexer.cmi lib/options.cmi lib/pp.cmi \ + proofs/tacexpr.cmo lib/util.cmi parsing/pcoq.cmi +parsing/pcoq.cmx: parsing/ast.cmx parsing/coqast.cmx library/decl_kinds.cmx \ + parsing/genarg.cmx parsing/lexer.cmx lib/options.cmx lib/pp.cmx \ + proofs/tacexpr.cmx lib/util.cmx parsing/pcoq.cmi parsing/ppconstr.cmo: parsing/ast.cmi parsing/coqast.cmi lib/dyn.cmi \ parsing/esyntax.cmi parsing/extend.cmi parsing/genarg.cmi \ library/libnames.cmi library/nameops.cmi kernel/names.cmi \ @@ -978,20 +995,20 @@ pretyping/cbv.cmo: kernel/closure.cmi kernel/environ.cmi kernel/esubst.cmi \ pretyping/cbv.cmx: kernel/closure.cmx kernel/environ.cmx kernel/esubst.cmx \ pretyping/evd.cmx pretyping/instantiate.cmx kernel/names.cmx lib/pp.cmx \ kernel/term.cmx kernel/univ.cmx lib/util.cmx pretyping/cbv.cmi -pretyping/classops.cmo: library/declare.cmi kernel/environ.cmi \ - pretyping/evd.cmi library/global.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 -pretyping/classops.cmx: library/declare.cmx kernel/environ.cmx \ - pretyping/evd.cmx library/global.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 +pretyping/classops.cmo: library/decl_kinds.cmo library/declare.cmi \ + kernel/environ.cmi pretyping/evd.cmi library/global.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 +pretyping/classops.cmx: library/decl_kinds.cmx library/declare.cmx \ + kernel/environ.cmx pretyping/evd.cmx library/global.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 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 \ @@ -1044,24 +1061,24 @@ pretyping/evd.cmo: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \ lib/util.cmi pretyping/evd.cmi pretyping/evd.cmx: kernel/names.cmx kernel/sign.cmx kernel/term.cmx \ lib/util.cmx pretyping/evd.cmi -pretyping/indrec.cmo: kernel/declarations.cmi library/declare.cmi \ - kernel/entries.cmi kernel/environ.cmi pretyping/evd.cmi \ - library/global.cmi kernel/indtypes.cmi kernel/inductive.cmi \ - pretyping/inductiveops.cmi pretyping/instantiate.cmi library/libnames.cmi \ - library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ - lib/pp.cmi kernel/reduction.cmi pretyping/reductionops.cmi \ - kernel/safe_typing.cmi kernel/term.cmi pretyping/termops.cmi \ - kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \ - pretyping/indrec.cmi -pretyping/indrec.cmx: kernel/declarations.cmx library/declare.cmx \ - kernel/entries.cmx kernel/environ.cmx pretyping/evd.cmx \ - library/global.cmx kernel/indtypes.cmx kernel/inductive.cmx \ - pretyping/inductiveops.cmx pretyping/instantiate.cmx library/libnames.cmx \ - library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ - lib/pp.cmx kernel/reduction.cmx pretyping/reductionops.cmx \ - kernel/safe_typing.cmx kernel/term.cmx pretyping/termops.cmx \ - kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \ - pretyping/indrec.cmi +pretyping/indrec.cmo: library/decl_kinds.cmo kernel/declarations.cmi \ + library/declare.cmi kernel/entries.cmi kernel/environ.cmi \ + pretyping/evd.cmi library/global.cmi kernel/indtypes.cmi \ + kernel/inductive.cmi pretyping/inductiveops.cmi pretyping/instantiate.cmi \ + library/libnames.cmi library/nameops.cmi kernel/names.cmi \ + library/nametab.cmi lib/options.cmi lib/pp.cmi kernel/reduction.cmi \ + pretyping/reductionops.cmi kernel/safe_typing.cmi kernel/term.cmi \ + pretyping/termops.cmi kernel/type_errors.cmi kernel/typeops.cmi \ + lib/util.cmi pretyping/indrec.cmi +pretyping/indrec.cmx: library/decl_kinds.cmx kernel/declarations.cmx \ + library/declare.cmx kernel/entries.cmx kernel/environ.cmx \ + pretyping/evd.cmx library/global.cmx kernel/indtypes.cmx \ + kernel/inductive.cmx pretyping/inductiveops.cmx pretyping/instantiate.cmx \ + library/libnames.cmx library/nameops.cmx kernel/names.cmx \ + library/nametab.cmx lib/options.cmx lib/pp.cmx kernel/reduction.cmx \ + pretyping/reductionops.cmx kernel/safe_typing.cmx kernel/term.cmx \ + pretyping/termops.cmx kernel/type_errors.cmx kernel/typeops.cmx \ + lib/util.cmx pretyping/indrec.cmi pretyping/inductiveops.cmo: kernel/declarations.cmi kernel/environ.cmi \ pretyping/evd.cmi library/global.cmi kernel/inductive.cmi \ kernel/names.cmi pretyping/reductionops.cmi kernel/sign.cmi \ @@ -1145,13 +1162,13 @@ pretyping/reductionops.cmx: kernel/closure.cmx kernel/declarations.cmx \ pretyping/termops.cmx kernel/univ.cmx lib/util.cmx \ pretyping/reductionops.cmi pretyping/retyping.cmo: kernel/declarations.cmi kernel/environ.cmi \ - kernel/inductive.cmi pretyping/instantiate.cmi kernel/names.cmi \ - pretyping/reductionops.cmi kernel/term.cmi kernel/typeops.cmi \ - kernel/univ.cmi lib/util.cmi pretyping/retyping.cmi + kernel/inductive.cmi pretyping/inductiveops.cmi pretyping/instantiate.cmi \ + kernel/names.cmi pretyping/reductionops.cmi kernel/term.cmi \ + kernel/typeops.cmi kernel/univ.cmi lib/util.cmi pretyping/retyping.cmi pretyping/retyping.cmx: kernel/declarations.cmx kernel/environ.cmx \ - kernel/inductive.cmx pretyping/instantiate.cmx kernel/names.cmx \ - pretyping/reductionops.cmx kernel/term.cmx kernel/typeops.cmx \ - kernel/univ.cmx lib/util.cmx pretyping/retyping.cmi + kernel/inductive.cmx pretyping/inductiveops.cmx pretyping/instantiate.cmx \ + kernel/names.cmx pretyping/reductionops.cmx kernel/term.cmx \ + kernel/typeops.cmx kernel/univ.cmx lib/util.cmx pretyping/retyping.cmi pretyping/syntax_def.cmo: library/lib.cmi library/libnames.cmi \ library/libobject.cmi library/nameops.cmi kernel/names.cmi \ library/nametab.cmi lib/pp.cmi pretyping/rawterm.cmi library/summary.cmi \ @@ -1236,20 +1253,20 @@ proofs/logic.cmx: parsing/coqast.cmx library/declare.cmx kernel/environ.cmx \ pretyping/retyping.cmx kernel/sign.cmx kernel/term.cmx \ pretyping/termops.cmx kernel/type_errors.cmx kernel/typeops.cmx \ pretyping/typing.cmx lib/util.cmx proofs/logic.cmi -proofs/pfedit.cmo: parsing/astterm.cmi kernel/declarations.cmi \ - library/declare.cmi lib/edit.cmi kernel/entries.cmi kernel/environ.cmi \ - proofs/evar_refiner.cmi pretyping/evd.cmi library/lib.cmi \ - library/libnames.cmi library/nameops.cmi kernel/names.cmi lib/pp.cmi \ - proofs/proof_trees.cmi proofs/proof_type.cmi kernel/safe_typing.cmi \ - kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi pretyping/typing.cmi \ - lib/util.cmi proofs/pfedit.cmi -proofs/pfedit.cmx: parsing/astterm.cmx kernel/declarations.cmx \ - library/declare.cmx lib/edit.cmx kernel/entries.cmx kernel/environ.cmx \ - proofs/evar_refiner.cmx pretyping/evd.cmx library/lib.cmx \ - library/libnames.cmx library/nameops.cmx kernel/names.cmx lib/pp.cmx \ - proofs/proof_trees.cmx proofs/proof_type.cmx kernel/safe_typing.cmx \ - kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx \ - lib/util.cmx proofs/pfedit.cmi +proofs/pfedit.cmo: parsing/astterm.cmi library/decl_kinds.cmo \ + kernel/declarations.cmi library/declare.cmi lib/edit.cmi \ + kernel/entries.cmi kernel/environ.cmi proofs/evar_refiner.cmi \ + pretyping/evd.cmi library/lib.cmi library/nameops.cmi kernel/names.cmi \ + lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ + kernel/safe_typing.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \ + pretyping/typing.cmi lib/util.cmi proofs/pfedit.cmi +proofs/pfedit.cmx: parsing/astterm.cmx library/decl_kinds.cmx \ + kernel/declarations.cmx library/declare.cmx lib/edit.cmx \ + kernel/entries.cmx kernel/environ.cmx proofs/evar_refiner.cmx \ + pretyping/evd.cmx library/lib.cmx library/nameops.cmx kernel/names.cmx \ + lib/pp.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ + kernel/safe_typing.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \ + pretyping/typing.cmx lib/util.cmx proofs/pfedit.cmi proofs/proof_trees.cmo: kernel/closure.cmi pretyping/detyping.cmi \ kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ library/global.cmi library/libnames.cmi library/nameops.cmi \ @@ -1264,14 +1281,14 @@ proofs/proof_trees.cmx: kernel/closure.cmx pretyping/detyping.cmx \ proofs/proof_type.cmx kernel/sign.cmx pretyping/tacred.cmx \ kernel/term.cmx pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ proofs/proof_trees.cmi -proofs/proof_type.cmo: kernel/closure.cmi kernel/environ.cmi \ - pretyping/evd.cmi parsing/genarg.cmi library/libnames.cmi \ - kernel/names.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo kernel/term.cmi \ - lib/util.cmi proofs/proof_type.cmi -proofs/proof_type.cmx: kernel/closure.cmx kernel/environ.cmx \ - pretyping/evd.cmx parsing/genarg.cmx library/libnames.cmx \ - kernel/names.cmx pretyping/rawterm.cmx proofs/tacexpr.cmx kernel/term.cmx \ - lib/util.cmx proofs/proof_type.cmi +proofs/proof_type.cmo: kernel/closure.cmi library/decl_kinds.cmo \ + kernel/environ.cmi pretyping/evd.cmi parsing/genarg.cmi \ + library/libnames.cmi kernel/names.cmi pretyping/rawterm.cmi \ + proofs/tacexpr.cmo kernel/term.cmi lib/util.cmi proofs/proof_type.cmi +proofs/proof_type.cmx: kernel/closure.cmx library/decl_kinds.cmx \ + kernel/environ.cmx pretyping/evd.cmx parsing/genarg.cmx \ + library/libnames.cmx kernel/names.cmx pretyping/rawterm.cmx \ + proofs/tacexpr.cmx kernel/term.cmx lib/util.cmx proofs/proof_type.cmi proofs/refiner.cmo: kernel/environ.cmi pretyping/evarutil.cmi \ pretyping/evd.cmi library/global.cmi pretyping/instantiate.cmi \ proofs/logic.cmi lib/pp.cmi parsing/pptactic.cmi parsing/printer.cmi \ @@ -1529,21 +1546,21 @@ tactics/inv.cmx: proofs/clenv.cmx parsing/coqlib.cmx tactics/elim.cmx \ tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx \ pretyping/typing.cmx lib/util.cmx tactics/wcclausenv.cmx tactics/inv.cmi tactics/leminv.cmo: parsing/astterm.cmi proofs/clenv.cmi \ - kernel/declarations.cmi library/declare.cmi kernel/entries.cmi \ - kernel/environ.cmi proofs/evar_refiner.cmi pretyping/evd.cmi \ - library/global.cmi pretyping/inductiveops.cmi tactics/inv.cmi \ - library/libnames.cmi library/nameops.cmi kernel/names.cmi \ - proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \ + library/decl_kinds.cmo kernel/declarations.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 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/wcclausenv.cmi tactics/leminv.cmi tactics/leminv.cmx: parsing/astterm.cmx proofs/clenv.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/libnames.cmx library/nameops.cmx kernel/names.cmx \ - proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.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 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 \ @@ -1567,33 +1584,33 @@ tactics/refine.cmx: proofs/clenv.cmx kernel/environ.cmx pretyping/evd.cmx \ pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ tactics/refine.cmi tactics/setoid_replace.cmo: parsing/astterm.cmi tactics/auto.cmi \ - toplevel/command.cmi library/declare.cmi kernel/entries.cmi \ - kernel/environ.cmi pretyping/evd.cmi library/global.cmi lib/gmap.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 parsing/printer.cmi proofs/proof_type.cmi \ - pretyping/reductionops.cmi kernel/safe_typing.cmi library/summary.cmi \ - proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \ - kernel/term.cmi parsing/termast.cmi pretyping/termops.cmi \ - pretyping/typing.cmi lib/util.cmi toplevel/vernacentries.cmi \ - toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi \ - tactics/setoid_replace.cmi + toplevel/command.cmi library/decl_kinds.cmo library/declare.cmi \ + kernel/entries.cmi kernel/environ.cmi pretyping/evd.cmi \ + library/global.cmi lib/gmap.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 parsing/printer.cmi \ + proofs/proof_type.cmi pretyping/reductionops.cmi kernel/safe_typing.cmi \ + library/summary.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi parsing/termast.cmi \ + pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ + toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \ + toplevel/vernacinterp.cmi tactics/setoid_replace.cmi tactics/setoid_replace.cmx: parsing/astterm.cmx tactics/auto.cmx \ - toplevel/command.cmx library/declare.cmx kernel/entries.cmx \ - kernel/environ.cmx pretyping/evd.cmx library/global.cmx lib/gmap.cmx \ - library/lib.cmx library/libnames.cmx library/libobject.cmx \ - library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ - lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx \ - pretyping/reductionops.cmx kernel/safe_typing.cmx library/summary.cmx \ - proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ - kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx \ - pretyping/typing.cmx lib/util.cmx toplevel/vernacentries.cmx \ - toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx \ - tactics/setoid_replace.cmi + toplevel/command.cmx library/decl_kinds.cmx library/declare.cmx \ + kernel/entries.cmx kernel/environ.cmx pretyping/evd.cmx \ + library/global.cmx lib/gmap.cmx library/lib.cmx library/libnames.cmx \ + library/libobject.cmx library/nameops.cmx kernel/names.cmx \ + library/nametab.cmx lib/options.cmx lib/pp.cmx parsing/printer.cmx \ + proofs/proof_type.cmx pretyping/reductionops.cmx kernel/safe_typing.cmx \ + library/summary.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ + tactics/tactics.cmx kernel/term.cmx parsing/termast.cmx \ + pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ + toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \ + toplevel/vernacinterp.cmx tactics/setoid_replace.cmi tactics/tacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi tactics/auto.cmi \ - kernel/closure.cmi parsing/coqast.cmi kernel/declarations.cmi \ - library/declare.cmi tactics/dhyp.cmi lib/dyn.cmi tactics/elim.cmi \ - kernel/entries.cmi kernel/environ.cmi pretyping/evd.cmi \ + kernel/closure.cmi parsing/coqast.cmi library/decl_kinds.cmo \ + kernel/declarations.cmi library/declare.cmi tactics/dhyp.cmi lib/dyn.cmi \ + tactics/elim.cmi kernel/entries.cmi kernel/environ.cmi pretyping/evd.cmi \ parsing/genarg.cmi library/global.cmi lib/gmap.cmi tactics/hiddentac.cmi \ library/lib.cmi library/libnames.cmi library/libobject.cmi \ proofs/logic.cmi library/nameops.cmi kernel/names.cmi library/nametab.cmi \ @@ -1606,9 +1623,9 @@ tactics/tacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi tactics/auto.cmi \ kernel/term.cmi parsing/termast.cmi pretyping/termops.cmi \ pretyping/typing.cmi lib/util.cmi tactics/tacinterp.cmi tactics/tacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx tactics/auto.cmx \ - kernel/closure.cmx parsing/coqast.cmx kernel/declarations.cmx \ - library/declare.cmx tactics/dhyp.cmx lib/dyn.cmx tactics/elim.cmx \ - kernel/entries.cmx kernel/environ.cmx pretyping/evd.cmx \ + kernel/closure.cmx parsing/coqast.cmx library/decl_kinds.cmx \ + kernel/declarations.cmx library/declare.cmx tactics/dhyp.cmx lib/dyn.cmx \ + tactics/elim.cmx kernel/entries.cmx kernel/environ.cmx pretyping/evd.cmx \ parsing/genarg.cmx library/global.cmx lib/gmap.cmx tactics/hiddentac.cmx \ library/lib.cmx library/libnames.cmx library/libobject.cmx \ proofs/logic.cmx library/nameops.cmx kernel/names.cmx library/nametab.cmx \ @@ -1635,25 +1652,25 @@ tactics/tacticals.cmx: proofs/clenv.cmx kernel/declarations.cmx \ proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ tactics/wcclausenv.cmx tactics/tacticals.cmi tactics/tactics.cmo: parsing/astterm.cmi proofs/clenv.cmi kernel/closure.cmi \ - parsing/coqlib.cmi kernel/declarations.cmi library/declare.cmi \ - kernel/entries.cmi kernel/environ.cmi proofs/evar_refiner.cmi \ - pretyping/evd.cmi library/global.cmi tactics/hipattern.cmi \ - pretyping/indrec.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \ - library/libnames.cmi proofs/logic.cmi library/nameops.cmi \ - kernel/names.cmi library/nametab.cmi lib/options.cmi proofs/pfedit.cmi \ - lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ + parsing/coqlib.cmi library/decl_kinds.cmo kernel/declarations.cmi \ + library/declare.cmi kernel/entries.cmi kernel/environ.cmi \ + proofs/evar_refiner.cmi pretyping/evd.cmi library/global.cmi \ + tactics/hipattern.cmi pretyping/indrec.cmi kernel/inductive.cmi \ + pretyping/inductiveops.cmi library/libnames.cmi proofs/logic.cmi \ + library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ + proofs/pfedit.cmi lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ pretyping/rawterm.cmi pretyping/reductionops.cmi proofs/refiner.cmi \ kernel/sign.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \ pretyping/tacred.cmi tactics/tacticals.cmi kernel/term.cmi \ pretyping/termops.cmi lib/util.cmi tactics/tactics.cmi tactics/tactics.cmx: parsing/astterm.cmx proofs/clenv.cmx kernel/closure.cmx \ - parsing/coqlib.cmx kernel/declarations.cmx library/declare.cmx \ - kernel/entries.cmx kernel/environ.cmx proofs/evar_refiner.cmx \ - pretyping/evd.cmx library/global.cmx tactics/hipattern.cmx \ - pretyping/indrec.cmx kernel/inductive.cmx pretyping/inductiveops.cmx \ - library/libnames.cmx proofs/logic.cmx library/nameops.cmx \ - kernel/names.cmx library/nametab.cmx lib/options.cmx proofs/pfedit.cmx \ - lib/pp.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ + parsing/coqlib.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 \ + tactics/hipattern.cmx pretyping/indrec.cmx kernel/inductive.cmx \ + pretyping/inductiveops.cmx library/libnames.cmx proofs/logic.cmx \ + library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ + proofs/pfedit.cmx lib/pp.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ pretyping/rawterm.cmx pretyping/reductionops.cmx proofs/refiner.cmx \ kernel/sign.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \ pretyping/tacred.cmx tactics/tacticals.cmx kernel/term.cmx \ @@ -1688,10 +1705,10 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \ proofs/proof_trees.cmx pretyping/reductionops.cmx proofs/refiner.cmx \ kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx \ lib/util.cmx tactics/wcclausenv.cmi -tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi -tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx +tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi +tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx tools/gallina.cmo: tools/gallina_lexer.cmo tools/gallina.cmx: tools/gallina_lexer.cmx toplevel/cerrors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \ @@ -1704,49 +1721,51 @@ toplevel/cerrors.cmx: parsing/ast.cmx pretyping/cases.cmx toplevel/himsg.cmx \ proofs/logic.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \ pretyping/pretype_errors.cmx proofs/refiner.cmx kernel/type_errors.cmx \ kernel/univ.cmx lib/util.cmx toplevel/cerrors.cmi -toplevel/class.cmo: pretyping/classops.cmi kernel/declarations.cmi \ - library/declare.cmi kernel/entries.cmi kernel/environ.cmi \ - pretyping/evd.cmi library/global.cmi kernel/inductive.cmi library/lib.cmi \ - library/libnames.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi lib/options.cmi lib/pp.cmi parsing/printer.cmi \ - pretyping/reductionops.cmi pretyping/retyping.cmi kernel/safe_typing.cmi \ - kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi \ - pretyping/typing.cmi lib/util.cmi toplevel/class.cmi -toplevel/class.cmx: pretyping/classops.cmx kernel/declarations.cmx \ - library/declare.cmx kernel/entries.cmx kernel/environ.cmx \ - pretyping/evd.cmx library/global.cmx kernel/inductive.cmx library/lib.cmx \ - library/libnames.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx lib/options.cmx lib/pp.cmx parsing/printer.cmx \ - pretyping/reductionops.cmx pretyping/retyping.cmx kernel/safe_typing.cmx \ - kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \ - pretyping/typing.cmx lib/util.cmx toplevel/class.cmi -toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi toplevel/class.cmi \ - parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \ - kernel/entries.cmi kernel/environ.cmi pretyping/evarutil.cmi \ - pretyping/evd.cmi library/global.cmi tactics/hiddentac.cmi \ - library/impargs.cmi pretyping/indrec.cmi kernel/indtypes.cmi \ +toplevel/class.cmo: pretyping/classops.cmi library/decl_kinds.cmo \ + kernel/declarations.cmi library/declare.cmi kernel/entries.cmi \ + kernel/environ.cmi pretyping/evd.cmi library/global.cmi \ kernel/inductive.cmi library/lib.cmi library/libnames.cmi \ - library/libobject.cmi library/library.cmi proofs/logic.cmi \ library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ - proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi \ - kernel/reduction.cmi proofs/refiner.cmi pretyping/retyping.cmi \ - kernel/safe_typing.cmi library/states.cmi pretyping/syntax_def.cmi \ - proofs/tacmach.cmi pretyping/tacred.cmi kernel/term.cmi \ - pretyping/termops.cmi kernel/typeops.cmi lib/util.cmi \ - toplevel/vernacexpr.cmo toplevel/command.cmi -toplevel/command.cmx: parsing/ast.cmx parsing/astterm.cmx toplevel/class.cmx \ - parsing/coqast.cmx kernel/declarations.cmx library/declare.cmx \ - kernel/entries.cmx kernel/environ.cmx pretyping/evarutil.cmx \ - pretyping/evd.cmx library/global.cmx tactics/hiddentac.cmx \ - library/impargs.cmx pretyping/indrec.cmx kernel/indtypes.cmx \ + lib/pp.cmi parsing/printer.cmi pretyping/reductionops.cmi \ + pretyping/retyping.cmi kernel/safe_typing.cmi kernel/sign.cmi \ + kernel/term.cmi pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ + toplevel/class.cmi +toplevel/class.cmx: pretyping/classops.cmx library/decl_kinds.cmx \ + kernel/declarations.cmx library/declare.cmx kernel/entries.cmx \ + kernel/environ.cmx pretyping/evd.cmx library/global.cmx \ kernel/inductive.cmx library/lib.cmx library/libnames.cmx \ - library/libobject.cmx library/library.cmx proofs/logic.cmx \ library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ - proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx \ - kernel/reduction.cmx proofs/refiner.cmx pretyping/retyping.cmx \ - kernel/safe_typing.cmx library/states.cmx pretyping/syntax_def.cmx \ - proofs/tacmach.cmx pretyping/tacred.cmx kernel/term.cmx \ - pretyping/termops.cmx kernel/typeops.cmx lib/util.cmx \ + lib/pp.cmx parsing/printer.cmx pretyping/reductionops.cmx \ + pretyping/retyping.cmx kernel/safe_typing.cmx kernel/sign.cmx \ + kernel/term.cmx pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ + toplevel/class.cmi +toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi toplevel/class.cmi \ + parsing/coqast.cmi library/decl_kinds.cmo kernel/declarations.cmi \ + library/declare.cmi kernel/entries.cmi kernel/environ.cmi \ + pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \ + tactics/hiddentac.cmi library/impargs.cmi pretyping/indrec.cmi \ + kernel/indtypes.cmi kernel/inductive.cmi library/lib.cmi \ + library/libnames.cmi library/libobject.cmi library/library.cmi \ + proofs/logic.cmi library/nameops.cmi kernel/names.cmi library/nametab.cmi \ + lib/options.cmi proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi \ + proofs/proof_type.cmi kernel/reduction.cmi proofs/refiner.cmi \ + pretyping/retyping.cmi kernel/safe_typing.cmi library/states.cmi \ + pretyping/syntax_def.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ + kernel/term.cmi pretyping/termops.cmi kernel/typeops.cmi lib/util.cmi \ + toplevel/vernacexpr.cmo toplevel/command.cmi +toplevel/command.cmx: parsing/ast.cmx parsing/astterm.cmx toplevel/class.cmx \ + parsing/coqast.cmx library/decl_kinds.cmx kernel/declarations.cmx \ + library/declare.cmx kernel/entries.cmx kernel/environ.cmx \ + pretyping/evarutil.cmx pretyping/evd.cmx library/global.cmx \ + tactics/hiddentac.cmx library/impargs.cmx pretyping/indrec.cmx \ + kernel/indtypes.cmx kernel/inductive.cmx library/lib.cmx \ + library/libnames.cmx library/libobject.cmx library/library.cmx \ + proofs/logic.cmx library/nameops.cmx kernel/names.cmx library/nametab.cmx \ + lib/options.cmx proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx \ + proofs/proof_type.cmx kernel/reduction.cmx proofs/refiner.cmx \ + pretyping/retyping.cmx kernel/safe_typing.cmx library/states.cmx \ + pretyping/syntax_def.cmx proofs/tacmach.cmx pretyping/tacred.cmx \ + kernel/term.cmx pretyping/termops.cmx kernel/typeops.cmx lib/util.cmx \ toplevel/vernacexpr.cmx toplevel/command.cmi toplevel/coqinit.cmo: config/coq_config.cmi toplevel/mltop.cmi \ library/nameops.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \ @@ -1769,25 +1788,27 @@ toplevel/coqtop.cmx: toplevel/cerrors.cmx config/coq_config.cmx \ library/states.cmx lib/system.cmx toplevel/toplevel.cmx \ toplevel/usage.cmx lib/util.cmx toplevel/vernac.cmx toplevel/coqtop.cmi toplevel/discharge.cmo: toplevel/class.cmi pretyping/classops.cmi \ - kernel/cooking.cmi kernel/declarations.cmi library/declare.cmi \ - kernel/entries.cmi kernel/environ.cmi library/global.cmi \ - library/impargs.cmi kernel/indtypes.cmi kernel/inductive.cmi \ - pretyping/instantiate.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 lib/pp.cmi \ - toplevel/recordobj.cmi pretyping/recordops.cmi kernel/reduction.cmi \ - kernel/sign.cmi library/summary.cmi kernel/term.cmi kernel/typeops.cmi \ - kernel/univ.cmi lib/util.cmi toplevel/discharge.cmi + kernel/cooking.cmi library/decl_kinds.cmo kernel/declarations.cmi \ + library/declare.cmi library/dischargedhypsmap.cmi kernel/entries.cmi \ + kernel/environ.cmi library/global.cmi library/impargs.cmi \ + kernel/indtypes.cmi kernel/inductive.cmi pretyping/instantiate.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 lib/pp.cmi toplevel/recordobj.cmi \ + pretyping/recordops.cmi kernel/reduction.cmi kernel/sign.cmi \ + library/summary.cmi kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi \ + lib/util.cmi toplevel/discharge.cmi toplevel/discharge.cmx: toplevel/class.cmx pretyping/classops.cmx \ - kernel/cooking.cmx kernel/declarations.cmx library/declare.cmx \ - kernel/entries.cmx kernel/environ.cmx library/global.cmx \ - library/impargs.cmx kernel/indtypes.cmx kernel/inductive.cmx \ - pretyping/instantiate.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 lib/pp.cmx \ - toplevel/recordobj.cmx pretyping/recordops.cmx kernel/reduction.cmx \ - kernel/sign.cmx library/summary.cmx kernel/term.cmx kernel/typeops.cmx \ - kernel/univ.cmx lib/util.cmx toplevel/discharge.cmi + kernel/cooking.cmx library/decl_kinds.cmx kernel/declarations.cmx \ + library/declare.cmx library/dischargedhypsmap.cmx kernel/entries.cmx \ + kernel/environ.cmx library/global.cmx library/impargs.cmx \ + kernel/indtypes.cmx kernel/inductive.cmx pretyping/instantiate.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 lib/pp.cmx toplevel/recordobj.cmx \ + pretyping/recordops.cmx kernel/reduction.cmx kernel/sign.cmx \ + library/summary.cmx kernel/term.cmx kernel/typeops.cmx kernel/univ.cmx \ + lib/util.cmx toplevel/discharge.cmi toplevel/fhimsg.cmo: kernel/environ.cmi parsing/g_minicoq.cmi \ kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \ kernel/term.cmi kernel/type_errors.cmi lib/util.cmi toplevel/fhimsg.cmi @@ -1849,25 +1870,25 @@ toplevel/protectedtoplevel.cmx: toplevel/cerrors.cmx \ toplevel/vernac.cmx toplevel/vernacexpr.cmx \ toplevel/protectedtoplevel.cmi toplevel/record.cmo: parsing/ast.cmi parsing/astterm.cmi toplevel/class.cmi \ - toplevel/command.cmi parsing/coqast.cmi kernel/declarations.cmi \ - library/declare.cmi kernel/entries.cmi kernel/environ.cmi \ - pretyping/evd.cmi library/global.cmi kernel/indtypes.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 parsing/printer.cmi pretyping/recordops.cmi \ - kernel/safe_typing.cmi kernel/term.cmi pretyping/termops.cmi \ - kernel/type_errors.cmi lib/util.cmi toplevel/vernacexpr.cmo \ - toplevel/record.cmi + toplevel/command.cmi parsing/coqast.cmi library/decl_kinds.cmo \ + kernel/declarations.cmi library/declare.cmi kernel/entries.cmi \ + kernel/environ.cmi pretyping/evd.cmi library/global.cmi \ + kernel/indtypes.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 parsing/printer.cmi \ + pretyping/recordops.cmi kernel/safe_typing.cmi kernel/term.cmi \ + pretyping/termops.cmi kernel/type_errors.cmi lib/util.cmi \ + toplevel/vernacexpr.cmo toplevel/record.cmi toplevel/record.cmx: parsing/ast.cmx parsing/astterm.cmx toplevel/class.cmx \ - toplevel/command.cmx parsing/coqast.cmx kernel/declarations.cmx \ - library/declare.cmx kernel/entries.cmx kernel/environ.cmx \ - pretyping/evd.cmx library/global.cmx kernel/indtypes.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 parsing/printer.cmx pretyping/recordops.cmx \ - kernel/safe_typing.cmx kernel/term.cmx pretyping/termops.cmx \ - kernel/type_errors.cmx lib/util.cmx toplevel/vernacexpr.cmx \ - toplevel/record.cmi + toplevel/command.cmx parsing/coqast.cmx library/decl_kinds.cmx \ + kernel/declarations.cmx library/declare.cmx kernel/entries.cmx \ + kernel/environ.cmx pretyping/evd.cmx library/global.cmx \ + kernel/indtypes.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 parsing/printer.cmx \ + pretyping/recordops.cmx kernel/safe_typing.cmx kernel/term.cmx \ + pretyping/termops.cmx kernel/type_errors.cmx lib/util.cmx \ + toplevel/vernacexpr.cmx toplevel/record.cmi toplevel/recordobj.cmo: pretyping/classops.cmi library/declare.cmi \ kernel/environ.cmi library/global.cmi pretyping/instantiate.cmi \ library/lib.cmi library/libnames.cmi library/nameops.cmi kernel/names.cmi \ @@ -1888,20 +1909,10 @@ toplevel/toplevel.cmx: parsing/ast.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: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \ - library/library.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \ - lib/pp.cmi library/states.cmi lib/system.cmi lib/util.cmi \ - toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \ - toplevel/vernacinterp.cmi toplevel/vernac.cmi -toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ - library/library.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \ - lib/pp.cmx library/states.cmx lib/system.cmx lib/util.cmx \ - toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \ - toplevel/vernacinterp.cmx toplevel/vernac.cmi toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astmod.cmi \ parsing/astterm.cmi tactics/auto.cmi toplevel/class.cmi \ pretyping/classops.cmi toplevel/command.cmi parsing/coqast.cmi \ - library/declare.cmi library/declaremods.cmi tactics/dhyp.cmi \ + library/decl_kinds.cmo library/declaremods.cmi tactics/dhyp.cmi \ toplevel/discharge.cmi kernel/entries.cmi kernel/environ.cmi \ pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \ library/goptions.cmi library/impargs.cmi pretyping/inductiveops.cmi \ @@ -1920,7 +1931,7 @@ toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astmod.cmi \ toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astmod.cmx \ parsing/astterm.cmx tactics/auto.cmx toplevel/class.cmx \ pretyping/classops.cmx toplevel/command.cmx parsing/coqast.cmx \ - library/declare.cmx library/declaremods.cmx tactics/dhyp.cmx \ + library/decl_kinds.cmx library/declaremods.cmx tactics/dhyp.cmx \ toplevel/discharge.cmx kernel/entries.cmx kernel/environ.cmx \ pretyping/evarutil.cmx pretyping/evd.cmx library/global.cmx \ library/goptions.cmx library/impargs.cmx pretyping/inductiveops.cmx \ @@ -1937,13 +1948,15 @@ toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astmod.cmx \ kernel/typeops.cmx kernel/univ.cmx lib/util.cmx toplevel/vernacexpr.cmx \ toplevel/vernacinterp.cmx toplevel/vernacentries.cmi toplevel/vernacexpr.cmo: parsing/ast.cmi parsing/coqast.cmi \ - parsing/extend.cmi parsing/genarg.cmi library/goptions.cmi \ - library/libnames.cmi kernel/names.cmi library/nametab.cmi \ - proofs/proof_type.cmi parsing/symbols.cmi proofs/tacexpr.cmo lib/util.cmi + library/decl_kinds.cmo parsing/extend.cmi parsing/genarg.cmi \ + library/goptions.cmi library/libnames.cmi kernel/names.cmi \ + library/nametab.cmi proofs/proof_type.cmi parsing/symbols.cmi \ + proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmx: parsing/ast.cmx parsing/coqast.cmx \ - parsing/extend.cmx parsing/genarg.cmx library/goptions.cmx \ - library/libnames.cmx kernel/names.cmx library/nametab.cmx \ - proofs/proof_type.cmx parsing/symbols.cmx proofs/tacexpr.cmx lib/util.cmx + library/decl_kinds.cmx parsing/extend.cmx parsing/genarg.cmx \ + library/goptions.cmx library/libnames.cmx kernel/names.cmx \ + library/nametab.cmx proofs/proof_type.cmx parsing/symbols.cmx \ + proofs/tacexpr.cmx lib/util.cmx toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/coqast.cmi \ parsing/extend.cmi toplevel/himsg.cmi library/libnames.cmi \ kernel/names.cmi lib/options.cmi lib/pp.cmi proofs/proof_type.cmi \ @@ -1954,6 +1967,16 @@ 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: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \ + library/library.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \ + lib/pp.cmi library/states.cmi lib/system.cmi lib/util.cmi \ + toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \ + toplevel/vernacinterp.cmi toplevel/vernac.cmi +toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ + library/library.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \ + lib/pp.cmx library/states.cmx lib/system.cmx lib/util.cmx \ + toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \ + toplevel/vernacinterp.cmx toplevel/vernac.cmi contrib/cc/ccalgo.cmo: kernel/names.cmi kernel/term.cmi contrib/cc/ccalgo.cmi contrib/cc/ccalgo.cmx: kernel/names.cmx kernel/term.cmx contrib/cc/ccalgo.cmi contrib/cc/ccproof.cmo: contrib/cc/ccalgo.cmi kernel/names.cmi \ @@ -1976,6 +1999,18 @@ contrib/cc/cctac.cmx: contrib/cc/ccalgo.cmx contrib/cc/ccproof.cmx \ proofs/proof_type.cmx proofs/refiner.cmx tactics/tacinterp.cmx \ proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ kernel/term.cmx lib/util.cmx +contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \ + contrib/correctness/past.cmi contrib/correctness/penv.cmi \ + contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \ + contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \ + contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \ + kernel/univ.cmi contrib/correctness/pcicenv.cmi +contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \ + contrib/correctness/past.cmi contrib/correctness/penv.cmx \ + contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \ + contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \ + contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \ + kernel/univ.cmx contrib/correctness/pcicenv.cmi contrib/correctness/pcic.cmo: parsing/ast.cmi kernel/declarations.cmi \ library/declare.cmi pretyping/detyping.cmi kernel/entries.cmi \ library/global.cmi kernel/indtypes.cmi library/libnames.cmi \ @@ -1990,18 +2025,6 @@ contrib/correctness/pcic.cmx: parsing/ast.cmx kernel/declarations.cmx \ contrib/correctness/pmisc.cmx pretyping/rawterm.cmx toplevel/record.cmx \ kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx kernel/typeops.cmx \ lib/util.cmx toplevel/vernacexpr.cmx contrib/correctness/pcic.cmi -contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \ - contrib/correctness/past.cmi contrib/correctness/penv.cmi \ - contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \ - contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \ - contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/univ.cmi contrib/correctness/pcicenv.cmi -contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \ - contrib/correctness/past.cmi contrib/correctness/penv.cmx \ - contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \ - contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \ - contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \ - kernel/univ.cmx contrib/correctness/pcicenv.cmi contrib/correctness/pdb.cmo: library/declare.cmi library/global.cmi \ kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \ contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \ @@ -2111,10 +2134,10 @@ contrib/correctness/prename.cmx: toplevel/himsg.cmx library/nameops.cmx \ kernel/names.cmx contrib/correctness/pmisc.cmx lib/pp.cmx lib/util.cmx \ contrib/correctness/prename.cmi contrib/correctness/psyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \ - parsing/coqast.cmi library/declare.cmi kernel/entries.cmi \ - pretyping/evd.cmi parsing/extend.cmi parsing/g_zsyntax.cmi \ - parsing/genarg.cmi library/global.cmi toplevel/himsg.cmi \ - library/libnames.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \ + parsing/coqast.cmi library/decl_kinds.cmo library/declare.cmi \ + kernel/entries.cmi pretyping/evd.cmi parsing/extend.cmi \ + parsing/g_zsyntax.cmi parsing/genarg.cmi library/global.cmi \ + toplevel/himsg.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \ contrib/correctness/past.cmi contrib/correctness/pcicenv.cmi \ parsing/pcoq.cmi contrib/correctness/pdb.cmi \ contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \ @@ -2126,10 +2149,10 @@ contrib/correctness/psyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \ toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \ toplevel/vernacinterp.cmi contrib/correctness/psyntax.cmi contrib/correctness/psyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \ - parsing/coqast.cmx library/declare.cmx kernel/entries.cmx \ - pretyping/evd.cmx parsing/extend.cmx parsing/g_zsyntax.cmx \ - parsing/genarg.cmx library/global.cmx toplevel/himsg.cmx \ - library/libnames.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \ + parsing/coqast.cmx library/decl_kinds.cmx library/declare.cmx \ + kernel/entries.cmx pretyping/evd.cmx parsing/extend.cmx \ + parsing/g_zsyntax.cmx parsing/genarg.cmx library/global.cmx \ + toplevel/himsg.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \ contrib/correctness/past.cmi contrib/correctness/pcicenv.cmx \ parsing/pcoq.cmx contrib/correctness/pdb.cmx \ contrib/correctness/peffect.cmx contrib/correctness/penv.cmx \ @@ -2140,36 +2163,38 @@ contrib/correctness/psyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \ kernel/term.cmx parsing/termast.cmx lib/util.cmx toplevel/vernac.cmx \ toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \ toplevel/vernacinterp.cmx contrib/correctness/psyntax.cmi -contrib/correctness/ptactic.cmo: tactics/equality.cmi pretyping/evd.cmi \ - tactics/extratactics.cmi library/global.cmi library/libnames.cmi \ - library/library.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ - contrib/correctness/past.cmi pretyping/pattern.cmi \ - contrib/correctness/pcic.cmi contrib/correctness/pdb.cmi \ - contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \ - contrib/correctness/perror.cmi proofs/pfedit.cmi \ - contrib/correctness/pmisc.cmi contrib/correctness/pmlize.cmi \ - contrib/correctness/pmonad.cmi lib/pp.cmi contrib/correctness/pred.cmi \ - contrib/correctness/prename.cmi pretyping/pretyping.cmi \ - parsing/printer.cmi contrib/correctness/ptyping.cmi \ - contrib/correctness/putil.cmi contrib/correctness/pwp.cmi \ - kernel/reduction.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ - tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \ - toplevel/vernacentries.cmi contrib/correctness/ptactic.cmi -contrib/correctness/ptactic.cmx: tactics/equality.cmx pretyping/evd.cmx \ - tactics/extratactics.cmx library/global.cmx library/libnames.cmx \ - library/library.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ - contrib/correctness/past.cmi pretyping/pattern.cmx \ - contrib/correctness/pcic.cmx contrib/correctness/pdb.cmx \ - contrib/correctness/peffect.cmx contrib/correctness/penv.cmx \ - contrib/correctness/perror.cmx proofs/pfedit.cmx \ - contrib/correctness/pmisc.cmx contrib/correctness/pmlize.cmx \ - contrib/correctness/pmonad.cmx lib/pp.cmx contrib/correctness/pred.cmx \ - contrib/correctness/prename.cmx pretyping/pretyping.cmx \ - parsing/printer.cmx contrib/correctness/ptyping.cmx \ - contrib/correctness/putil.cmx contrib/correctness/pwp.cmx \ - kernel/reduction.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ - tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ - toplevel/vernacentries.cmx contrib/correctness/ptactic.cmi +contrib/correctness/ptactic.cmo: library/decl_kinds.cmo tactics/equality.cmi \ + pretyping/evd.cmi tactics/extratactics.cmi library/global.cmi \ + library/libnames.cmi library/library.cmi kernel/names.cmi \ + library/nametab.cmi lib/options.cmi contrib/correctness/past.cmi \ + pretyping/pattern.cmi contrib/correctness/pcic.cmi \ + contrib/correctness/pdb.cmi contrib/correctness/peffect.cmi \ + contrib/correctness/penv.cmi contrib/correctness/perror.cmi \ + proofs/pfedit.cmi contrib/correctness/pmisc.cmi \ + contrib/correctness/pmlize.cmi contrib/correctness/pmonad.cmi lib/pp.cmi \ + contrib/correctness/pred.cmi contrib/correctness/prename.cmi \ + pretyping/pretyping.cmi parsing/printer.cmi \ + contrib/correctness/ptyping.cmi contrib/correctness/putil.cmi \ + contrib/correctness/pwp.cmi kernel/reduction.cmi proofs/tacmach.cmi \ + tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ + pretyping/termops.cmi lib/util.cmi toplevel/vernacentries.cmi \ + contrib/correctness/ptactic.cmi +contrib/correctness/ptactic.cmx: library/decl_kinds.cmx tactics/equality.cmx \ + pretyping/evd.cmx tactics/extratactics.cmx library/global.cmx \ + library/libnames.cmx library/library.cmx kernel/names.cmx \ + library/nametab.cmx lib/options.cmx contrib/correctness/past.cmi \ + pretyping/pattern.cmx contrib/correctness/pcic.cmx \ + contrib/correctness/pdb.cmx contrib/correctness/peffect.cmx \ + contrib/correctness/penv.cmx contrib/correctness/perror.cmx \ + proofs/pfedit.cmx contrib/correctness/pmisc.cmx \ + contrib/correctness/pmlize.cmx contrib/correctness/pmonad.cmx lib/pp.cmx \ + contrib/correctness/pred.cmx contrib/correctness/prename.cmx \ + pretyping/pretyping.cmx parsing/printer.cmx \ + contrib/correctness/ptyping.cmx contrib/correctness/putil.cmx \ + contrib/correctness/pwp.cmx kernel/reduction.cmx proofs/tacmach.cmx \ + tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ + pretyping/termops.cmx lib/util.cmx toplevel/vernacentries.cmx \ + contrib/correctness/ptactic.cmi contrib/correctness/ptyping.cmo: parsing/ast.cmi parsing/astterm.cmi \ kernel/environ.cmi pretyping/evd.cmi library/global.cmi \ toplevel/himsg.cmi kernel/names.cmi contrib/correctness/past.cmi \ @@ -2485,21 +2510,21 @@ contrib/interface/history.cmx: contrib/interface/paths.cmx \ contrib/interface/line_parser.cmo: contrib/interface/line_parser.cmi contrib/interface/line_parser.cmx: contrib/interface/line_parser.cmi contrib/interface/name_to_ast.cmo: parsing/ast.cmi pretyping/classops.cmi \ - parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \ - kernel/environ.cmi library/global.cmi library/impargs.cmi \ - kernel/inductive.cmi library/lib.cmi library/libnames.cmi \ - library/libobject.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi lib/pp.cmi parsing/prettyp.cmi kernel/reduction.cmi \ - kernel/sign.cmi kernel/term.cmi parsing/termast.cmi lib/util.cmi \ - toplevel/vernacexpr.cmo contrib/interface/name_to_ast.cmi + parsing/coqast.cmi library/decl_kinds.cmo kernel/declarations.cmi \ + library/declare.cmi kernel/environ.cmi library/global.cmi \ + library/impargs.cmi kernel/inductive.cmi library/lib.cmi \ + library/libnames.cmi library/libobject.cmi library/nameops.cmi \ + kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/prettyp.cmi \ + kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi parsing/termast.cmi \ + lib/util.cmi toplevel/vernacexpr.cmo contrib/interface/name_to_ast.cmi contrib/interface/name_to_ast.cmx: parsing/ast.cmx pretyping/classops.cmx \ - parsing/coqast.cmx kernel/declarations.cmx library/declare.cmx \ - kernel/environ.cmx library/global.cmx library/impargs.cmx \ - kernel/inductive.cmx library/lib.cmx library/libnames.cmx \ - library/libobject.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx lib/pp.cmx parsing/prettyp.cmx kernel/reduction.cmx \ - kernel/sign.cmx kernel/term.cmx parsing/termast.cmx lib/util.cmx \ - toplevel/vernacexpr.cmx contrib/interface/name_to_ast.cmi + parsing/coqast.cmx library/decl_kinds.cmx kernel/declarations.cmx \ + library/declare.cmx kernel/environ.cmx library/global.cmx \ + library/impargs.cmx kernel/inductive.cmx library/lib.cmx \ + library/libnames.cmx library/libobject.cmx library/nameops.cmx \ + kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/prettyp.cmx \ + kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx parsing/termast.cmx \ + lib/util.cmx toplevel/vernacexpr.cmx contrib/interface/name_to_ast.cmi contrib/interface/parse.cmo: contrib/interface/ascent.cmi \ toplevel/cerrors.cmi config/coq_config.cmi contrib/interface/ctast.cmo \ library/declaremods.cmi parsing/esyntax.cmi library/libnames.cmi \ @@ -2538,6 +2563,14 @@ contrib/interface/pbp.cmx: parsing/astterm.cmx parsing/coqast.cmx \ tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ tactics/tactics.cmx kernel/term.cmx parsing/termast.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: parsing/ast.cmi parsing/astterm.cmi \ proofs/clenv.cmi parsing/coqast.cmi kernel/declarations.cmi \ kernel/environ.cmi pretyping/evd.cmi parsing/genarg.cmi \ @@ -2562,14 +2595,6 @@ contrib/interface/showproof.cmx: parsing/ast.cmx parsing/astterm.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 \ contrib/interface/ctast.cmo kernel/environ.cmi pretyping/evarutil.cmi \ pretyping/evd.cmi library/libobject.cmi library/library.cmi \ @@ -2590,16 +2615,16 @@ contrib/interface/vtp.cmx: contrib/interface/ascent.cmi \ contrib/interface/vtp.cmi contrib/interface/xlate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \ parsing/astterm.cmi parsing/coqast.cmi contrib/interface/ctast.cmo \ - tactics/eauto.cmo tactics/extraargs.cmi parsing/genarg.cmi \ - library/libnames.cmi kernel/names.cmi pretyping/rawterm.cmi \ - proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmo \ - contrib/interface/xlate.cmi + library/decl_kinds.cmo tactics/eauto.cmo tactics/extraargs.cmi \ + parsing/genarg.cmi library/libnames.cmi kernel/names.cmi \ + pretyping/rawterm.cmi proofs/tacexpr.cmo lib/util.cmi \ + toplevel/vernacexpr.cmo contrib/interface/xlate.cmi contrib/interface/xlate.cmx: contrib/interface/ascent.cmi parsing/ast.cmx \ parsing/astterm.cmx parsing/coqast.cmx contrib/interface/ctast.cmx \ - tactics/eauto.cmx tactics/extraargs.cmx parsing/genarg.cmx \ - library/libnames.cmx kernel/names.cmx pretyping/rawterm.cmx \ - proofs/tacexpr.cmx lib/util.cmx toplevel/vernacexpr.cmx \ - contrib/interface/xlate.cmi + library/decl_kinds.cmx tactics/eauto.cmx tactics/extraargs.cmx \ + parsing/genarg.cmx library/libnames.cmx kernel/names.cmx \ + pretyping/rawterm.cmx proofs/tacexpr.cmx lib/util.cmx \ + toplevel/vernacexpr.cmx contrib/interface/xlate.cmi contrib/jprover/jall.cmo: contrib/jprover/jlogic.cmi \ contrib/jprover/jterm.cmi contrib/jprover/jtunify.cmi \ contrib/jprover/opname.cmi contrib/jprover/jall.cmi @@ -2738,26 +2763,84 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \ proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \ proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ kernel/term.cmx lib/util.cmx -contrib/xml/xml.cmo: contrib/xml/xml.cmi -contrib/xml/xml.cmx: contrib/xml/xml.cmi -contrib/xml/xmlcommand.cmo: kernel/declarations.cmi library/declare.cmi \ - library/declaremods.cmi kernel/environ.cmi pretyping/evd.cmi \ +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 library/declare.cmi \ + library/dischargedhypsmap.cmi contrib/xml/doubleTypeInference.cmi \ + kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ library/global.cmi library/lib.cmi library/libnames.cmi \ - library/libobject.cmi library/library.cmi library/nameops.cmi \ - kernel/names.cmi library/nametab.cmi proofs/pfedit.cmi \ - proofs/proof_trees.cmi kernel/reduction.cmi pretyping/retyping.cmi \ - kernel/safe_typing.cmi kernel/sign.cmi lib/system.cmi proofs/tacmach.cmi \ - kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi \ - contrib/xml/xmlcommand.cmi -contrib/xml/xmlcommand.cmx: kernel/declarations.cmx library/declare.cmx \ - library/declaremods.cmx kernel/environ.cmx pretyping/evd.cmx \ + library/library.cmi library/nameops.cmi kernel/names.cmi \ + library/nametab.cmi lib/pp.cmi parsing/printer.cmi \ + pretyping/reductionops.cmi pretyping/retyping.cmi kernel/term.cmi \ + pretyping/termops.cmi contrib/xml/unshare.cmi lib/util.cmi +contrib/xml/cic2acic.cmx: contrib/xml/acic.cmx library/declare.cmx \ + library/dischargedhypsmap.cmx contrib/xml/doubleTypeInference.cmx \ + kernel/environ.cmx pretyping/evarutil.cmx pretyping/evd.cmx \ library/global.cmx library/lib.cmx library/libnames.cmx \ - library/libobject.cmx library/library.cmx library/nameops.cmx \ - kernel/names.cmx library/nametab.cmx proofs/pfedit.cmx \ - proofs/proof_trees.cmx kernel/reduction.cmx pretyping/retyping.cmx \ - kernel/safe_typing.cmx kernel/sign.cmx lib/system.cmx proofs/tacmach.cmx \ - kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx \ - contrib/xml/xmlcommand.cmi + library/library.cmx library/nameops.cmx kernel/names.cmx \ + library/nametab.cmx lib/pp.cmx parsing/printer.cmx \ + pretyping/reductionops.cmx pretyping/retyping.cmx kernel/term.cmx \ + pretyping/termops.cmx contrib/xml/unshare.cmx lib/util.cmx +contrib/xml/doubleTypeInference.cmo: contrib/xml/acic.cmo kernel/environ.cmi \ + pretyping/evarutil.cmi pretyping/evd.cmi kernel/inductive.cmi \ + pretyping/instantiate.cmi lib/pp.cmi parsing/printer.cmi \ + kernel/reduction.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \ + kernel/term.cmi pretyping/termops.cmi kernel/typeops.cmi \ + contrib/xml/unshare.cmi lib/util.cmi contrib/xml/doubleTypeInference.cmi +contrib/xml/doubleTypeInference.cmx: contrib/xml/acic.cmx kernel/environ.cmx \ + pretyping/evarutil.cmx pretyping/evd.cmx kernel/inductive.cmx \ + pretyping/instantiate.cmx lib/pp.cmx parsing/printer.cmx \ + kernel/reduction.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \ + kernel/term.cmx pretyping/termops.cmx kernel/typeops.cmx \ + contrib/xml/unshare.cmx lib/util.cmx contrib/xml/doubleTypeInference.cmi +contrib/xml/proof2aproof.cmo: pretyping/evarutil.cmi pretyping/evd.cmi \ + library/global.cmi pretyping/instantiate.cmi proofs/logic.cmi lib/pp.cmi \ + proofs/proof_type.cmi proofs/refiner.cmi kernel/sign.cmi \ + proofs/tacmach.cmi kernel/term.cmi pretyping/termops.cmi \ + contrib/xml/unshare.cmi lib/util.cmi +contrib/xml/proof2aproof.cmx: pretyping/evarutil.cmx pretyping/evd.cmx \ + library/global.cmx pretyping/instantiate.cmx proofs/logic.cmx lib/pp.cmx \ + proofs/proof_type.cmx proofs/refiner.cmx kernel/sign.cmx \ + proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx \ + contrib/xml/unshare.cmx lib/util.cmx +contrib/xml/proofTree2Xml.cmo: contrib/xml/acic.cmo contrib/xml/acic2Xml.cmo \ + contrib/xml/cic2acic.cmo kernel/environ.cmi pretyping/evd.cmi \ + library/global.cmi proofs/logic.cmi kernel/names.cmi lib/pp.cmi \ + parsing/pptactic.cmi parsing/printer.cmi contrib/xml/proof2aproof.cmo \ + proofs/proof_trees.cmi proofs/proof_type.cmi kernel/sign.cmi \ + proofs/tacexpr.cmo kernel/term.cmi contrib/xml/unshare.cmi lib/util.cmi \ + contrib/xml/xml.cmi +contrib/xml/proofTree2Xml.cmx: contrib/xml/acic.cmx contrib/xml/acic2Xml.cmx \ + contrib/xml/cic2acic.cmx kernel/environ.cmx pretyping/evd.cmx \ + library/global.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \ + parsing/pptactic.cmx parsing/printer.cmx contrib/xml/proof2aproof.cmx \ + proofs/proof_trees.cmx proofs/proof_type.cmx kernel/sign.cmx \ + proofs/tacexpr.cmx kernel/term.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/xmlcommand.cmo: contrib/xml/acic.cmo contrib/xml/acic2Xml.cmo \ + contrib/xml/cic2acic.cmo library/decl_kinds.cmo kernel/declarations.cmi \ + library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \ + library/global.cmi kernel/inductive.cmi library/lib.cmi \ + library/libnames.cmi library/libobject.cmi kernel/names.cmi \ + library/nametab.cmi proofs/pfedit.cmi contrib/xml/proof2aproof.cmo \ + contrib/xml/proofTree2Xml.cmo proofs/proof_trees.cmi kernel/sign.cmi \ + proofs/tacmach.cmi kernel/term.cmi contrib/xml/unshare.cmi lib/util.cmi \ + contrib/xml/xml.cmi contrib/xml/xmlcommand.cmi +contrib/xml/xmlcommand.cmx: contrib/xml/acic.cmx contrib/xml/acic2Xml.cmx \ + contrib/xml/cic2acic.cmx library/decl_kinds.cmx kernel/declarations.cmx \ + library/declare.cmx kernel/environ.cmx pretyping/evd.cmx \ + library/global.cmx kernel/inductive.cmx library/lib.cmx \ + library/libnames.cmx library/libobject.cmx kernel/names.cmx \ + library/nametab.cmx proofs/pfedit.cmx contrib/xml/proof2aproof.cmx \ + contrib/xml/proofTree2Xml.cmx proofs/proof_trees.cmx kernel/sign.cmx \ + proofs/tacmach.cmx kernel/term.cmx contrib/xml/unshare.cmx lib/util.cmx \ + contrib/xml/xml.cmx contrib/xml/xmlcommand.cmi contrib/xml/xmlentries.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \ parsing/extend.cmi parsing/genarg.cmi parsing/pcoq.cmi lib/pp.cmi \ parsing/pptactic.cmi tactics/tacinterp.cmi lib/util.cmi \ @@ -2766,6 +2849,8 @@ contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \ parsing/extend.cmx parsing/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \ parsing/pptactic.cmx tactics/tacinterp.cmx lib/util.cmx \ toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx +contrib/xml/xml.cmo: contrib/xml/xml.cmi +contrib/xml/xml.cmx: contrib/xml/xml.cmi tactics/tauto.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo tactics/tauto.cmx: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo tactics/eqdecide.cmo: parsing/grammar.cma @@ -2842,8 +2927,10 @@ lib/pp.cmo: lib/pp.cmx: contrib/xml/xml.cmo: contrib/xml/xml.cmx: -contrib/xml/xmlcommand.cmo: -contrib/xml/xmlcommand.cmx: +contrib/xml/acic2Xml.cmo: +contrib/xml/acic2Xml.cmx: +contrib/xml/proofTree2Xml.cmo: +contrib/xml/proofTree2Xml.cmx: contrib/interface/line_parser.cmo: contrib/interface/line_parser.cmx: tools/coq_makefile.cmo: diff --git a/.depend.camlp4 b/.depend.camlp4 index bccd1a4b1..6b741f752 100644 --- a/.depend.camlp4 +++ b/.depend.camlp4 @@ -36,7 +36,8 @@ parsing/vernacextend.ml: toplevel/mltop.ml: lib/pp.ml: contrib/xml/xml.ml: -contrib/xml/xmlcommand.ml: +contrib/xml/acic2Xml.ml: +contrib/xml/proofTree2Xml.ml: contrib/interface/line_parser.ml: tools/coq_makefile.ml: tools/coq-tex.ml: @@ -60,7 +60,7 @@ CAMLP4DEPS=sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$$|\1|p' COQINCLUDES= # coqtop includes itself the needed paths GLOB= # is "-dump-glob file" when making the doc -BOOTCOQTOP=$(BESTCOQTOP) -boot -$(BEST) $(COQINCLUDES) $(GLOB) +BOOTCOQTOP=$(BESTCOQTOP) -boot -$(BEST) $(COQINCLUDES) $(GLOB) $(COQ_XML) ########################################################################### # Objects files @@ -91,7 +91,9 @@ LIBRARY=library/libnames.cmo library/nameops.cmo library/libobject.cmo \ library/summary.cmo \ library/nametab.cmo library/global.cmo library/lib.cmo \ library/declaremods.cmo library/library.cmo library/states.cmo \ - library/impargs.cmo library/declare.cmo library/goptions.cmo + library/impargs.cmo library/decl_kinds.cmo \ + library/dischargedhypsmap.cmo library/declare.cmo \ + library/goptions.cmo PRETYPING=pretyping/termops.cmo \ pretyping/evd.cmo pretyping/instantiate.cmo \ @@ -195,15 +197,15 @@ PARSERREQUIRES=config/coq_config.cmo lib/pp_control.cmo lib/pp.cmo \ library/nametab.cmo library/lib.cmo library/global.cmo \ library/declaremods.cmo \ library/library.cmo lib/options.cmo library/impargs.cmo \ - library/goptions.cmo \ + library/dischargedhypsmap.cmo library/goptions.cmo \ pretyping/evd.cmo pretyping/instantiate.cmo \ - pretyping/termops.cmo \ - pretyping/reductionops.cmo pretyping/retyping.cmo library/declare.cmo \ + pretyping/termops.cmo pretyping/reductionops.cmo \ + pretyping/inductiveops.cmo pretyping/retyping.cmo library/declare.cmo \ pretyping/cbv.cmo pretyping/tacred.cmo pretyping/classops.cmo \ pretyping/rawterm.cmo \ pretyping/pattern.cmo pretyping/pretype_errors.cmo \ pretyping/evarutil.cmo pretyping/recordops.cmo pretyping/evarconv.cmo \ - pretyping/coercion.cmo pretyping/inductiveops.cmo pretyping/cases.cmo \ + pretyping/coercion.cmo pretyping/cases.cmo \ pretyping/indrec.cmo \ pretyping/pretyping.cmo pretyping/syntax_def.cmo \ parsing/lexer.cmo parsing/coqast.cmo parsing/genarg.cmo \ @@ -248,7 +250,10 @@ RINGCMO=contrib/ring/quote.cmo contrib/ring/g_quote.cmo \ FIELDCMO=contrib/field/field.cmo -XMLCMO=contrib/xml/xml.cmo \ +XMLCMO=contrib/xml/unshare.cmo contrib/xml/xml.cmo contrib/xml/acic.cmo \ + contrib/xml/doubleTypeInference.cmo \ + contrib/xml/cic2acic.cmo contrib/xml/acic2Xml.cmo \ + contrib/xml/proof2aproof.cmo contrib/xml/proofTree2Xml.cmo \ contrib/xml/xmlcommand.cmo contrib/xml/xmlentries.cmo FOURIERCMO=contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo \ @@ -291,7 +296,8 @@ CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) CMO=$(CONFIG) $(LIBREP) $(KERNEL) $(LIBRARY) $(PRETYPING) \ - $(PROOFS) $(TACTICS) $(PARSING) $(TOPLEVEL) $(HIGHPARSING) $(HIGHTACTICS) $(CONTRIB) + $(PROOFS) $(TACTICS) $(PARSING) $(TOPLEVEL) \ + $(HIGHPARSING) $(HIGHTACTICS) $(CONTRIB) CMX=$(CMO:.cmo=.cmx) ########################################################################### @@ -848,11 +854,10 @@ GRAMMARCMO=lib/pp_control.cmo lib/pp.cmo lib/util.cmo lib/bignat.cmo \ lib/dyn.cmo lib/options.cmo \ lib/hashcons.cmo lib/predicate.cmo lib/rtree.cmo \ $(KERNEL) \ - library/libnames.cmo \ - library/summary.cmo library/nameops.cmo \ - library/nametab.cmo \ - library/libobject.cmo library/lib.cmo library/goptions.cmo \ - pretyping/rawterm.cmo pretyping/evd.cmo \ + library/libnames.cmo library/summary.cmo library/nameops.cmo \ + library/nametab.cmo library/libobject.cmo library/lib.cmo \ + library/goptions.cmo library/decl_kinds.cmo \ + pretyping/rawterm.cmo pretyping/evd.cmo \ parsing/coqast.cmo parsing/genarg.cmo \ proofs/tacexpr.cmo proofs/proof_type.cmo parsing/ast.cmo \ parsing/lexer.cmo parsing/q_util.cmo parsing/extend.cmo \ @@ -918,7 +923,8 @@ library/nametab.cmx: library/nametab.ml ML4FILES += lib/pp.ml4 \ contrib/xml/xml.ml4 \ - contrib/xml/xmlcommand.ml4 \ + contrib/xml/acic2Xml.ml4 \ + contrib/xml/proofTree2Xml.ml4 \ contrib/interface/line_parser.ml4 \ tools/coq_makefile.ml4 \ tools/coq-tex.ml4 @@ -365,10 +365,15 @@ chmod a-w $COQTOP/config/Makefile if test "$coq_debug_flag" = "-g" ; then rm -f $COQTOP/dev/ocamldebug-v7 + if [ "$CAMLP4LIB" = "+camlp4" ] ; then + CAMLP4LIBFORCAMLDEBUG=$CAMLLIB/camlp4 + else + CAMLP4LIBFORCAMLDEBUG=$CAMLP4LIB + fi sed -e "s|COQTOPDIRECTORY|$COQTOP|" \ -e "s|COQLIBDIRECTORY|$LIBDIR|" \ -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \ - -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIB|" \ + -e "s|CAMLP4LIBDIRECTORY|$CAMLP4LIBFORCAMLDEBUG|" \ $COQTOP/dev/ocamldebug-v7.template > $COQTOP/dev/ocamldebug-v7 chmod a-w,a+x $COQTOP/dev/ocamldebug-v7 fi diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index 59a32bafb..591076bdd 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -548,7 +548,7 @@ let _ = if not (is_mutable v) then begin let c = Entries.ParameterEntry (trad_ml_type_v ren env v), - Libnames.NeverDischarge in + Decl_kinds.IsAssumption Decl_kinds.Definitional in List.iter (fun id -> ignore (Declare.declare_constant id c)) ids; if_verbose (is_assumed false) ids diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml index aac393690..c24baea80 100644 --- a/contrib/correctness/ptactic.ml +++ b/contrib/correctness/ptactic.ml @@ -17,6 +17,7 @@ open Libnames open Term open Pretyping open Pfedit +open Decl_kinds open Vernacentries open Pmisc @@ -27,7 +28,6 @@ open Prename open Peffect open Pmonad - (* [coqast_of_prog: program -> constr * constr] * Traduction d'un programme impératif en un but (second constr) * et un terme de preuve partiel pour ce but (premier constr) @@ -239,7 +239,7 @@ let correctness s p opttac = let sigma = Evd.empty in let cty = Reduction.nf_betaiota cty in let id = id_of_string s in - start_proof id (false, NeverDischarge) sign cty correctness_hook; + start_proof id (IsGlobal (Proof Lemma)) sign cty correctness_hook; Penv.new_edited id (v,p); if !debug then show_open_subgoals(); deb_mess (str"Pred.red_cci: Reduction..." ++ fnl ()); diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index b1602655f..b917f24d4 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -417,7 +417,7 @@ let inspect n = oname, Lib.Leaf lobj -> (match oname, object_tag lobj with (sp,_), "VARIABLE" -> - let ((_, _, v), _) = get_variable (basename sp) in + let (_, _, v) = get_variable (basename sp) in add_search2 (Nametab.locate (qualid_of_sp sp)) v | (sp,kn), ("CONSTANT"|"PARAMETER") -> let {const_type=typ} = Global.lookup_constant kn in diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index ef232d0dc..ec600d21d 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -19,6 +19,7 @@ open Pp;; open Declare;; open Nametab open Vernacexpr;; +open Decl_kinds;; (* This function converts the parameter binders of an inductive definition, in particular you have to be careful to handle each element in the @@ -150,7 +151,7 @@ let make_variable_ast name typ implicits = *) let make_variable_ast name typ implicits = (VernacAssumption - (AssumptionVariable, [false,(name, constr_to_ast (body_of_type typ))])) + ((Local,Definitional), [false,(name, constr_to_ast (body_of_type typ))])) ::(implicits_to_ast_list implicits);; (* @@ -165,7 +166,7 @@ let make_definition_ast name c typ implicits = (implicits_to_ast_list implicits);; *) let make_definition_ast name c typ implicits = - VernacDefinition (Definition, name, DefineBody ([], None, + VernacDefinition (Global, name, DefineBody ([], None, (constr_to_ast c), Some (constr_to_ast (body_of_type typ))), (fun _ _ -> ())) ::(implicits_to_ast_list implicits);; @@ -183,7 +184,7 @@ let constant_to_ast_list kn = make_definition_ast (id_of_label (label kn)) (Declarations.force c1) typ l) let variable_to_ast_list sp = - let ((id, c, v), _) = get_variable sp in + let (id, c, v) = get_variable sp in let l = implicits_of_var sp in (match c with None -> diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 7142f1e6d..92a35b892 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -12,6 +12,7 @@ open Genarg;; open Rawterm;; open Tacexpr;; open Vernacexpr;; +open Decl_kinds;; let in_coq_ref = ref false;; @@ -1467,27 +1468,18 @@ let xlate_thm x = CT_thm (match x with | Theorem -> "Theorem" | Remark -> "Remark" | Lemma -> "Lemma" - | Fact -> "Fact" - | Decl -> "Decl") + | Fact -> "Fact") let xlate_defn x = CT_defn (match x with - | LocalDefinition -> "Local" - | Definition -> "Definition") - - -let xlate_defn_or_thm = - function - (* Unable to decide if a fact in one section or at toplevel, a remark - at toplevel or a theorem or a Definition *) - | StartTheoremProof k -> CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k) - | StartDefinitionBody k -> CT_coerce_DEFN_to_DEFN_OR_THM (xlate_defn k);; + | Local -> "Local" + | Global -> "Definition") let xlate_var x = CT_var (match x with - | AssumptionParameter -> "Parameter" - | AssumptionAxiom -> "Axiom" - | AssumptionVariable -> "Variable" - | AssumptionHypothesis -> "Hypothesis");; + | (Global,Definitional) -> "Parameter" + | (Global,Logical) -> "Axiom" + | (Local,Definitional) -> "Variable" + | (Local,Logical) -> "Hypothesis");; let xlate_dep = @@ -1915,8 +1907,7 @@ let xlate_vernac = | VernacNotation _ -> xlate_error "TODO: Notation" - | VernacInfix (str_assoc, n, str, id, sc) -> - (* TODO: handle scopes *) + | VernacInfix (str_assoc, n, str, id, None) -> CT_infix ( (match str_assoc with | Some Gramext.LeftA -> CT_lefta @@ -1924,15 +1915,15 @@ let xlate_vernac = | Some Gramext.NonA -> CT_nona | None -> CT_coerce_NONE_to_ASSOC CT_none), CT_int n, CT_string str, loc_qualid_to_ct_ID id) + | VernacInfix _ -> xlate_error "TODO: handle scopes" | VernacGrammar _ -> xlate_error "GRAMMAR not implemented" | VernacCoercion (s, id1, id2, id3) -> let id_opt = CT_coerce_NONE_to_IDENTITY_OPT CT_none in let local_opt = match s with (* Cannot decide whether it is a global or a Local but at toplevel *) - | Libnames.NeverDischarge -> CT_coerce_NONE_to_LOCAL_OPT CT_none - | Libnames.DischargeAt _ -> CT_local - | Libnames.NotDeclare -> assert false in + | Global -> CT_coerce_NONE_to_LOCAL_OPT CT_none + | Local -> CT_local in CT_coercion (local_opt, id_opt, loc_qualid_to_ct_ID id1, xlate_class id2, xlate_class id3) @@ -1941,9 +1932,8 @@ let xlate_vernac = let local_opt = match s with (* Cannot decide whether it is a global or a Local but at toplevel *) - | Libnames.NeverDischarge -> CT_coerce_NONE_to_LOCAL_OPT CT_none - | Libnames.DischargeAt _ -> CT_local - | Libnames.NotDeclare -> assert false in + | Global -> CT_coerce_NONE_to_LOCAL_OPT CT_none + | Local -> CT_local in CT_coercion (local_opt, id_opt, xlate_ident id1, xlate_class id2, xlate_class id3) | VernacResetName id -> CT_reset (xlate_ident id) diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml new file mode 100644 index 000000000..566da65d6 --- /dev/null +++ b/library/decl_kinds.ml @@ -0,0 +1,67 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +(* Informal mathematical status of declarations *) + +(* Kinds used at parsing time *) + +type theorem_kind = + | Theorem + | Lemma + | Fact + | Remark + +type locality_flag = (*bool (* local = true; global = false *)*) + | Local + | Global + +type strength = locality_flag (* For compatibility *) + +type type_as_formula_kind = Definitional | Logical + +(* [assumption_kind] + + | Local | Global + ------------------------------------ + Definitional | Variable | Parameter + Logical | Hypothesis | Axiom +*) +type assumption_kind = locality_flag * type_as_formula_kind + +type definition_kind = locality_flag + +(* Kinds used in proofs *) + +type global_goal_kind = + | DefinitionBody + | Proof of theorem_kind + +type goal_kind = + | IsGlobal of global_goal_kind + | IsLocal + +(* Kinds used in library *) + +type local_theorem_kind = LocalStatement + +type 'a mathematical_kind = + | IsAssumption of type_as_formula_kind + | IsDefinition + | IsProof of 'a + +type global_kind = theorem_kind mathematical_kind +type local_kind = local_theorem_kind mathematical_kind + +(* Utils *) + +let theorem_kind_of_goal_kind = function + | DefinitionBody -> IsDefinition + | Proof s -> IsProof s + diff --git a/library/declare.ml b/library/declare.ml index b338277d3..b67dbc6e2 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -28,6 +28,7 @@ open Impargs open Nametab open Library open Safe_typing +open Decl_kinds (**********************************************) @@ -39,38 +40,23 @@ open Safe_typing open Nametab -let depth_of_strength = function - | DischargeAt (sp',n) -> n - | NeverDischarge -> 0 - | NotDeclare -> assert false - -let make_strength_0 () = - let depth = Lib.sections_depth () in - let cwd = Lib.cwd() in - if depth > 0 then DischargeAt (cwd, depth) else NeverDischarge - -let make_strength_1 () = - let depth = Lib.sections_depth () in - let cwd = Lib.cwd() in - if depth > 1 then DischargeAt (extract_dirpath_prefix 1 cwd, depth-1) - else NeverDischarge - -let make_strength_2 () = - let depth = Lib.sections_depth () in - let cwd = Lib.cwd() in - if depth > 2 then DischargeAt (extract_dirpath_prefix 2 cwd, depth-2) - else NeverDischarge - -let is_less_persistent_strength = function - | (NeverDischarge,_) -> false - | (NotDeclare,_) -> false - | (_,NeverDischarge) -> true - | (_,NotDeclare) -> true - | (DischargeAt (sp1,_),DischargeAt (sp2,_)) -> - is_dirpath_prefix_of sp1 sp2 - let strength_min (stre1,stre2) = - if is_less_persistent_strength (stre1,stre2) then stre1 else stre2 + if stre1 = Local or stre2 = Local then Local else Global + +let string_of_strength = function + | Local -> "(local)" + | Global -> "(global)" + +(* XML output hooks *) +let xml_declare_variable = ref (fun sp -> ()) +let xml_declare_constant = ref (fun sp -> ()) +let xml_declare_inductive = ref (fun sp -> ()) + +let if_xml f x = if !Options.xml_export then f x else () + +let set_xml_declare_variable f = xml_declare_variable := if_xml f +let set_xml_declare_constant f = xml_declare_constant := if_xml f +let set_xml_declare_inductive f = xml_declare_inductive := if_xml f (* Section variables. *) @@ -78,14 +64,13 @@ type section_variable_entry = | SectionLocalDef of constr * types option * bool (* opacity *) | SectionLocalAssum of types -type variable_declaration = dir_path * section_variable_entry * strength +type variable_declaration = dir_path * section_variable_entry * local_kind type checked_section_variable = | CheckedSectionLocalDef of constr * types * Univ.constraints * bool | CheckedSectionLocalAssum of types * Univ.constraints -type checked_variable_declaration = - dir_path * checked_section_variable * strength +type checked_variable_declaration = dir_path * checked_section_variable let vartab = ref (Idmap.empty : checked_variable_declaration Idmap.t) @@ -95,7 +80,7 @@ let _ = Summary.declare_summary "VARIABLE" Summary.init_function = (fun () -> vartab := Idmap.empty); Summary.survive_section = false } -let cache_variable ((sp,_),(id,(p,d,strength))) = +let cache_variable ((sp,_),(id,(p,d,mk))) = (* Constr raisonne sur les noms courts *) if Idmap.mem id !vartab then errorlabstrm "cache_variable" (pr_id id ++ str " already exists"); @@ -109,23 +94,35 @@ let cache_variable ((sp,_),(id,(p,d,strength))) = let (_,bd,ty) = Global.lookup_named id in CheckedSectionLocalDef (out_some bd,ty,cst,opaq) in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); - vartab := Idmap.add id (p,vd,strength) !vartab + vartab := Idmap.add id (p,vd) !vartab let (in_variable, out_variable) = declare_object { (default_object "VARIABLE") with cache_function = cache_variable; classify_function = (fun _ -> Dispose) } -let declare_variable id obj = - let sp = add_leaf id (in_variable (id,obj)) in +let declare_variable_common id obj = + let oname = add_leaf id (in_variable (id,obj)) in if is_implicit_args() then declare_var_implicits id; - sp + oname + +(* for initial declaration *) +let declare_variable id obj = + let (_,kn as oname) = declare_variable_common id obj in + !xml_declare_variable kn; + Dischargedhypsmap.set_discharged_hyps (fst oname) []; + oname + +(* when coming from discharge: no xml output *) +let redeclare_variable id discharged_hyps obj = + let oname = declare_variable_common id obj in + Dischargedhypsmap.set_discharged_hyps (fst oname) discharged_hyps (* Globals: constants and parameters *) -type constant_declaration = constant_entry * strength +type constant_declaration = constant_entry * global_kind -let csttab = ref (Spmap.empty : strength Spmap.t) +let csttab = ref (Spmap.empty : global_kind Spmap.t) let _ = Summary.declare_summary "CONSTANT" { Summary.freeze_function = (fun () -> !csttab); @@ -133,7 +130,7 @@ let _ = Summary.declare_summary "CONSTANT" Summary.init_function = (fun () -> csttab := Spmap.empty); Summary.survive_section = false } -let cache_constant ((sp,kn),(cdt,stre)) = +let cache_constant ((sp,kn),(cdt,kind)) = (if Idmap.mem (basename sp) !vartab then errorlabstrm "cache_constant" (pr_id (basename sp) ++ str " already exists")); @@ -144,35 +141,26 @@ let cache_constant ((sp,kn),(cdt,stre)) = let kn' = Global.add_constant dir (basename sp) cdt in if kn' <> kn then anomaly "Kernel and Library names do not match"; - (match stre with - | DischargeAt (dp,n) when not (is_dirpath_prefix_of dp (Lib.cwd ())) -> - (* Only qualifications including the sections segment from the current - section to the discharge section is available for Remark & Fact *) - Nametab.push (Nametab.Until ((*n-Lib.sections_depth()+*)1)) sp (ConstRef kn) - | (NeverDischarge| DischargeAt _) -> - (* All qualifications of Theorem, Lemma & Definition are visible *) - Nametab.push (Nametab.Until 1) sp (ConstRef kn) - | NotDeclare -> assert false); - csttab := Spmap.add sp stre !csttab + Nametab.push (Nametab.Until 1) sp (ConstRef kn); + csttab := Spmap.add sp kind !csttab (* At load-time, the segment starting from the module name to the discharge *) (* section (if Remark or Fact) is needed to access a construction *) -let load_constant i ((sp,kn),(ce,stre)) = +let load_constant i ((sp,kn),(_,kind)) = (if Nametab.exists_cci sp then let (_,id) = repr_path sp in errorlabstrm "cache_constant" (pr_id id ++ str " already exists")); - csttab := Spmap.add sp stre !csttab; - Nametab.push (Nametab.Until ((*depth_of_strength stre + *)i)) sp (ConstRef kn) + csttab := Spmap.add sp kind !csttab; + Nametab.push (Nametab.Until i) sp (ConstRef kn) (* Opening means making the name without its module qualification available *) -let open_constant i ((sp,kn),(_,stre)) = - let n = depth_of_strength stre in - Nametab.push (Nametab.Exactly (i(*+n*))) sp (ConstRef kn) +let open_constant i ((sp,kn),_) = + Nametab.push (Nametab.Exactly i) sp (ConstRef kn) (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant_entry = ConstantEntry (ParameterEntry mkProp) -let dummy_constant (ce,stre) = dummy_constant_entry,stre +let dummy_constant (ce,mk) = dummy_constant_entry,mk let export_constant cst = Some (dummy_constant cst) @@ -195,15 +183,19 @@ let hcons_constant_declaration = function const_entry_opaque = ce.const_entry_opaque }, stre) | cd -> cd -let declare_constant id (cd,stre) = +let declare_constant id (cd,kind) = (* let cd = hcons_constant_declaration cd in *) - let oname = add_leaf id (in_constant (ConstantEntry cd,stre)) in - if is_implicit_args() then declare_constant_implicits (snd oname); + let (_,kn as oname) = add_leaf id (in_constant (ConstantEntry cd,kind)) in + if is_implicit_args() then declare_constant_implicits kn; + Dischargedhypsmap.set_discharged_hyps (fst oname) [] ; + !xml_declare_constant kn; oname -let redeclare_constant id (cd,stre) = - let _,kn = add_leaf id (in_constant (GlobalRecipe cd,stre)) in - if is_implicit_args() then declare_constant_implicits kn +(* when coming from discharge *) +let redeclare_constant id discharged_hyps (cd,kind) = + let _,kn as oname = add_leaf id (in_constant (GlobalRecipe cd,kind)) in + if is_implicit_args() then declare_constant_implicits kn; + Dischargedhypsmap.set_discharged_hyps (fst oname) discharged_hyps (* Inductives. *) @@ -282,7 +274,7 @@ let (in_inductive, out_inductive) = subst_function = ident_subst_function; export_function = export_inductive } -let declare_mind mie = +let declare_inductive_common mie = let id = match mie.mind_entry_inds with | ind::_ -> ind.mind_entry_typename | [] -> anomaly "cannot declare an empty list of inductives" @@ -291,35 +283,46 @@ let declare_mind mie = if is_implicit_args() then declare_mib_implicits (snd oname); oname +(* for initial declaration *) +let declare_mind mie = + let (_,kn as oname) = declare_inductive_common mie in + Dischargedhypsmap.set_discharged_hyps (fst oname) [] ; + !xml_declare_inductive kn; + oname + +(* when coming from discharge: no xml output *) +let redeclare_inductive discharged_hyps mie = + let oname = declare_inductive_common mie in + Dischargedhypsmap.set_discharged_hyps (fst oname) discharged_hyps ; + oname (*s Test and access functions. *) let is_constant sp = try let _ = Spmap.find sp !csttab in true with Not_found -> false -let constant_strength sp = Spmap.find sp !csttab +let constant_strength sp = Global +let constant_kind sp = Spmap.find sp !csttab let get_variable id = - let (p,x,str) = Idmap.find id !vartab in - let d = match x with + let (p,x) = Idmap.find id !vartab in + match x with | CheckedSectionLocalDef (c,ty,cst,opaq) -> (id,Some c,ty) - | CheckedSectionLocalAssum (ty,cst) -> (id,None,ty) in - (d,str) + | CheckedSectionLocalAssum (ty,cst) -> (id,None,ty) let get_variable_with_constraints id = - let (p,x,str) = Idmap.find id !vartab in + let (p,x) = Idmap.find id !vartab in match x with - | CheckedSectionLocalDef (c,ty,cst,opaq) -> ((id,Some c,ty),cst,str) - | CheckedSectionLocalAssum (ty,cst) -> ((id,None,ty),cst,str) + | CheckedSectionLocalDef (c,ty,cst,opaq) -> ((id,Some c,ty),cst) + | CheckedSectionLocalAssum (ty,cst) -> ((id,None,ty),cst) -let variable_strength id = - let (_,_,str) = Idmap.find id !vartab in str +let variable_strength _ = Local let find_section_variable id = - let (p,_,_) = Idmap.find id !vartab in Libnames.make_path p id + let (p,_) = Idmap.find id !vartab in Libnames.make_path p id let variable_opacity id = - let (_,x,_) = Idmap.find id !vartab in + let (_,x) = Idmap.find id !vartab in match x with | CheckedSectionLocalDef (c,ty,cst,opaq) -> opaq | CheckedSectionLocalAssum (ty,cst) -> false (* any.. *) @@ -369,7 +372,7 @@ let last_section_hyps dir = fold_named_context (fun (id,_,_) sec_ids -> try - let (p,_,_) = Idmap.find id !vartab in + let (p,_) = Idmap.find id !vartab in if dir=p then id::sec_ids else sec_ids with Not_found -> sec_ids) (Environ.named_context (Global.env())) @@ -436,23 +439,21 @@ let is_global id = with Not_found -> false -let strength_of_global ref = match ref with - | ConstRef kn -> constant_strength (sp_of_global None ref) - | VarRef id -> variable_strength id - | IndRef _ | ConstructRef _ -> NeverDischarge +let strength_of_global = function + | VarRef _ -> Local + | IndRef _ | ConstructRef _ | ConstRef _ -> Global let library_part ref = let sp = Nametab.sp_of_global None ref in let dir,_ = repr_path sp in match strength_of_global ref with - | DischargeAt (dp,n) -> - extract_dirpath_prefix n dp - | NeverDischarge -> + | Local -> + anomaly "TODO"; + extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()) + | Global -> if is_dirpath_prefix_of dir (Lib.cwd ()) then - (* Theorem/Lemma not yet (fully) discharged *) - extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()) + (* Not yet (fully) discharged *) + extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()) else (* Theorem/Lemma outside its outer section of definition *) dir - | NotDeclare -> assert false - diff --git a/library/declare.mli b/library/declare.mli index c9d7cc574..3c04ddf57 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -19,6 +19,7 @@ open Indtypes open Safe_typing open Library open Nametab +open Decl_kinds (*i*) (* This module provides the official functions to declare new variables, @@ -30,50 +31,59 @@ open Nametab open Nametab +(* Declaration of local constructions (Variable/Hypothesis/Local) *) + type section_variable_entry = | SectionLocalDef of constr * types option * bool (* opacity *) | SectionLocalAssum of types -type variable_declaration = dir_path * section_variable_entry * strength +type variable_declaration = dir_path * section_variable_entry * local_kind val declare_variable : variable -> variable_declaration -> object_name -type constant_declaration = constant_entry * strength +(* Declaration from Discharge *) +val redeclare_variable : + variable -> Dischargedhypsmap.discharged_hyps -> variable_declaration -> unit + +(* Declaration of global constructions *) +(* i.e. Definition/Theorem/Axiom/Parameter/... *) + +type constant_declaration = constant_entry * global_kind (* [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns the full path of the declaration *) val declare_constant : identifier -> constant_declaration -> object_name -val redeclare_constant : identifier -> Cooking.recipe * strength -> unit - -(* -val declare_parameter : identifier -> constr -> constant -*) +val redeclare_constant : + identifier -> Dischargedhypsmap.discharged_hyps -> + Cooking.recipe * global_kind -> unit (* [declare_mind me] declares a block of inductive types with their constructors in the current section; it returns the path of the whole block *) val declare_mind : mutual_inductive_entry -> object_name +(* Declaration from Discharge *) +val redeclare_inductive : + Dischargedhypsmap.discharged_hyps -> mutual_inductive_entry -> object_name + val out_inductive : Libobject.obj -> mutual_inductive_entry -val make_strength_0 : unit -> strength -val make_strength_1 : unit -> strength -val make_strength_2 : unit -> strength -val is_less_persistent_strength : strength * strength -> bool val strength_min : strength * strength -> strength +val string_of_strength : strength -> string (*s Corresponding test and access functions. *) val is_constant : section_path -> bool val constant_strength : section_path -> strength +val constant_kind : section_path -> global_kind val out_variable : Libobject.obj -> identifier * variable_declaration -val get_variable : variable -> named_declaration * strength +val get_variable : variable -> named_declaration val get_variable_with_constraints : - variable -> named_declaration * Univ.constraints * strength -val variable_strength : variable -> strength + variable -> named_declaration * Univ.constraints +val variable_strength : variable -> strength val find_section_variable : variable -> section_path val last_section_hyps : dir_path -> identifier list val clear_proofs : named_context -> named_context @@ -108,3 +118,8 @@ val is_global : identifier -> bool val strength_of_global : global_reference -> strength val library_part : global_reference -> dir_path + +(* hooks for XML output *) +val set_xml_declare_variable : (kernel_name -> unit) -> unit +val set_xml_declare_constant : (kernel_name -> unit) -> unit +val set_xml_declare_inductive : (kernel_name -> unit) -> unit diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml new file mode 100644 index 000000000..5241bf035 --- /dev/null +++ b/library/dischargedhypsmap.ml @@ -0,0 +1,59 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +open Util +open Libnames +open Names +open Term +open Reduction +open Declarations +open Environ +open Inductive +open Libobject +open Lib +open Nametab + +type discharged_hyps = section_path list + +let discharged_hyps_map = ref Spmap.empty + +let cache_discharged_hyps_map (_,(sp,hyps)) = + discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map + +let (in_discharged_hyps_map, _) = + declare_object { (default_object "DISCHARGED-HYPS-MAP") with + cache_function = cache_discharged_hyps_map; + load_function = (fun _ -> cache_discharged_hyps_map); + export_function = (fun x -> Some x) } + +let set_discharged_hyps sp hyps = + add_anonymous_leaf (in_discharged_hyps_map (sp,hyps)) + +let get_discharged_hyps sp = + try + Spmap.find sp !discharged_hyps_map + with Not_found -> + anomaly ("No discharged hypothesis for object " ^ string_of_path sp) + +(*s Registration as global tables and rollback. *) + +let init () = + discharged_hyps_map := Spmap.empty + +let freeze () = !discharged_hyps_map + +let unfreeze dhm = discharged_hyps_map := dhm + +let _ = + Summary.declare_summary "discharged_hypothesis" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; + Summary.survive_section = true } diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli new file mode 100644 index 000000000..cb3af4d47 --- /dev/null +++ b/library/dischargedhypsmap.mli @@ -0,0 +1,24 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +(*i*) +open Libnames +open Term +open Environ +open Nametab +(*i*) + +type discharged_hyps = section_path list + +(*s Discharged hypothesis. Here we store the discharged hypothesis of each *) +(* constant or inductive type declaration. *) + +val set_discharged_hyps : section_path -> discharged_hyps -> unit +val get_discharged_hyps : section_path -> discharged_hyps diff --git a/library/lib.mli b/library/lib.mli index 075be2890..56e79b661 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -119,6 +119,7 @@ val is_section_p : dir_path -> bool val start_compilation : dir_path -> module_path -> unit val end_compilation : dir_path -> object_prefix * library_segment +(* The function [module_dp] returns the [dir_path] of the current module *) val module_dp : unit -> dir_path (*s Modules and module types *) diff --git a/library/libnames.ml b/library/libnames.ml index d5e9c8dc7..19e7d2833 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -205,8 +205,3 @@ type global_dir_reference = let kn' = subst_kernel_name subst kn in if kn==kn' then ref else ModTypeRef kn' *) - -type strength = - | NotDeclare - | DischargeAt of dir_path * int - | NeverDischarge diff --git a/library/libnames.mli b/library/libnames.mli index 915cdf3d2..04e552f4d 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -111,8 +111,3 @@ type global_dir_reference = | DirModule of object_prefix | DirClosedSection of dir_path (* this won't last long I hope! *) - -type strength = - | NotDeclare - | DischargeAt of dir_path * int - | NeverDischarge diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index c3afc0956..a7eae13ee 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -19,6 +19,7 @@ open Util open Constr open Vernac_ open Prim +open Decl_kinds (* Dans join_binders, s'il y a un "?", on perd l'info qu'il est partagé *) let join_binders (idl,c) = List.map (fun id -> (id,c)) idl @@ -97,26 +98,24 @@ GEXTEND Gram [ [ "Theorem" -> Theorem | IDENT "Lemma" -> Lemma | IDENT "Fact" -> Fact - | IDENT "Remark" -> Remark - | IDENT "Decl" -> Decl ] ] + | IDENT "Remark" -> Remark ] ] ; def_token: - [ [ "Definition" -> (fun _ _ -> ()), Definition - | IDENT "Local" -> (fun _ _ -> ()), LocalDefinition - | IDENT "SubClass" -> Class.add_subclass_hook, Definition - | IDENT "Local"; IDENT "SubClass" -> - Class.add_subclass_hook, LocalDefinition ] ] + [ [ "Definition" -> (fun _ _ -> ()), Global + | IDENT "Local" -> (fun _ _ -> ()), Local + | IDENT "SubClass" -> Class.add_subclass_hook, Global + | IDENT "Local"; IDENT "SubClass" -> Class.add_subclass_hook, Local ] ] ; assumption_token: - [ [ "Hypothesis" -> AssumptionHypothesis - | "Variable" -> AssumptionVariable - | "Axiom" -> AssumptionAxiom - | "Parameter" -> AssumptionParameter ] ] + [ [ "Hypothesis" -> (Local, Logical) + | "Variable" -> (Local, Definitional) + | "Axiom" -> (Global, Logical) + | "Parameter" -> (Global, Definitional) ] ] ; assumptions_token: - [ [ IDENT "Hypotheses" -> AssumptionHypothesis - | IDENT "Variables" -> AssumptionVariable - | IDENT "Parameters" -> AssumptionParameter ] ] + [ [ IDENT "Hypotheses" -> (Local, Logical) + | IDENT "Variables" -> (Local, Definitional) + | IDENT "Parameters" -> (Global, Definitional) ] ] ; of_type_with_opt_coercion: [ [ ":>" -> true @@ -357,35 +356,29 @@ ident_comma_list_tail: VernacCanonical qid | IDENT "Canonical"; IDENT "Structure"; qid = qualid; d = def_body -> let s = Ast.coerce_qualid_to_id qid in - VernacDefinition (Definition,s,d,Recordobj.add_object_hook) -(* - VernacDefinition (Definition,s,None,c,t,Recordobj.add_object_hook) -*) + VernacDefinition (Global,s,d,Recordobj.add_object_hook) (* Rem: LOBJECT, OBJCOERCION, LOBJCOERCION have been removed (they were unused and undocumented) *) (* Coercions *) | IDENT "Coercion"; qid = qualid; d = def_body -> let s = Ast.coerce_qualid_to_id qid in -(* - VernacDefinition (Definition,s,None,c,t,Class.add_coercion_hook) -*) - VernacDefinition (Definition,s,d,Class.add_coercion_hook) + VernacDefinition (Global,s,d,Class.add_coercion_hook) | IDENT "Coercion"; IDENT "Local"; qid = qualid; d = def_body -> let s = Ast.coerce_qualid_to_id qid in - VernacDefinition (LocalDefinition,s,d,Class.add_coercion_hook) + VernacDefinition (Local,s,d,Class.add_coercion_hook) | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = Prim.ident; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacIdentityCoercion (Declare.make_strength_0 (), f, s, t) + VernacIdentityCoercion (Local, f, s, t) | IDENT "Identity"; IDENT "Coercion"; f = Prim.ident; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacIdentityCoercion (Libnames.NeverDischarge, f, s, t) + VernacIdentityCoercion (Global, f, s, t) | IDENT "Coercion"; IDENT "Local"; qid = qualid; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (Declare.make_strength_0 (), qid, s, t) + VernacCoercion (Local, qid, s, t) | IDENT "Coercion"; qid = qualid; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (Libnames.NeverDischarge, qid, s, t) + VernacCoercion (Global, qid, s, t) | IDENT "Class"; IDENT "Local"; c = qualid -> Pp.warning "Class is obsolete"; VernacNop | IDENT "Class"; c = qualid -> diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index d72a06f2a..67322863a 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -13,7 +13,6 @@ open Util open Ast open Genarg open Tacexpr -open Vernacexpr (* The lexer of Coq *) @@ -75,6 +74,7 @@ type typed_entry = entry_type Gramobj.entry module type Gramtypes = sig + open Decl_kinds val inAstListType : Coqast.t list G.Entry.e -> typed_entry val inTacticAtomAstType : raw_atomic_tactic_expr G.Entry.e -> typed_entry val inThmTokenAstType : theorem_kind G.Entry.e -> typed_entry diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index eb49b403c..b4a5bc9a7 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -175,8 +175,7 @@ module Tactic : module Vernac_ : sig - open Util - open Libnames + open Decl_kinds val thm_token : theorem_kind Gram.Entry.e val class_rawexpr : class_rawexpr Gram.Entry.e val gallina : vernac_expr Gram.Entry.e @@ -185,7 +184,4 @@ module Vernac_ : val syntax : vernac_expr Gram.Entry.e val vernac : vernac_expr Gram.Entry.e val vernac_eoi : vernac_expr Gram.Entry.e -(* - val reduce : Coqast.t list Gram.Entry.e -*) end diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 55611ec28..0f1157f1d 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -263,7 +263,7 @@ let print_mutual sp = implicit_args_msg sp mipv)) *) let print_section_variable sp = - let (d,_) = get_variable sp in + let d = get_variable sp in let l = implicits_of_var sp in (print_named_decl d ++ print_impl_args l) @@ -489,7 +489,7 @@ let print_local_context () = | [] -> (mt ()) | (oname,Lib.Leaf lobj)::rest -> if "VARIABLE" = object_tag lobj then - let (d,_) = get_variable (basename (fst oname)) in + let d = get_variable (basename (fst oname)) in (print_var_rec rest ++ print_named_decl d) else @@ -547,11 +547,6 @@ let inspect depth = open Classops -let string_of_strength = function - | NotDeclare -> "(temp)" - | NeverDischarge -> "(global)" - | DischargeAt (sp,_) -> "(disch@"^(string_of_dirpath sp) - let print_coercion_value v = prterm (get_coercion_value v) let print_index_coercion c = diff --git a/parsing/search.ml b/parsing/search.ml index 78e549e13..e1723a1d1 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -56,7 +56,7 @@ let crible (fn : global_reference -> env -> constr -> unit) ref = match object_tag lobj with | "VARIABLE" -> (try - let ((idc,_,typ),_) = get_variable (basename sp) in + let (idc,_,typ) = get_variable (basename sp) in if (head_const typ) = const then fn (VarRef idc) env typ with Not_found -> (* we are in a section *) ()) | "CONSTANT" diff --git a/pretyping/classops.ml b/pretyping/classops.ml index bc3b1310a..2b452ecbb 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -21,7 +21,7 @@ open Declare open Term open Termops open Rawterm -open Nametab +open Decl_kinds (* usage qque peu general: utilise aussi dans record *) @@ -100,8 +100,8 @@ let add_new_path x = let init () = class_tab:= []; - add_new_class (CL_FUN, { cl_param = 0; cl_strength = NeverDischarge }); - add_new_class (CL_SORT, { cl_param = 0; cl_strength = NeverDischarge }); + add_new_class (CL_FUN, { cl_param = 0; cl_strength = Global }); + add_new_class (CL_SORT, { cl_param = 0; cl_strength = Global }); coercion_tab:= []; inheritance_graph:= [] @@ -257,7 +257,7 @@ let class_args_of c = snd (decompose_app c) let strength_of_cl = function | CL_CONST kn -> constant_strength (sp_of_global None (ConstRef kn)) | CL_SECVAR sp -> variable_strength sp - | _ -> NeverDischarge + | _ -> Global let string_of_class = function | CL_FUN -> "FUNCLASS" diff --git a/pretyping/classops.mli b/pretyping/classops.mli index d37588d06..50af9840c 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -10,8 +10,7 @@ (*i*) open Names -open Libnames -open Nametab +open Decl_kinds open Term open Evd open Environ diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 4fce79be2..9ba82bf1f 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -57,6 +57,10 @@ val ise_try : evar_defs -> (unit -> bool) list -> bool val ise_undefined : evar_defs -> constr -> bool val has_undefined_isevars : evar_defs -> constr -> bool +val new_isevar_sign : + Environ.env -> Evd.evar_map -> Term.constr -> Term.constr list -> + Evd.evar_map * Term.constr + val new_isevar : evar_defs -> env -> loc * hole_kind -> constr -> constr val is_eliminator : constr -> bool diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index bcb0b5499..44398099c 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -507,7 +507,7 @@ let declare_one_elimination ind = { const_entry_body = c; const_entry_type = t; const_entry_opaque = false }, - NeverDischarge) in + Decl_kinds.IsDefinition) in Options.if_verbose ppnl (str na ++ str " is defined"); kn in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index eb798ee44..a2e484f53 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -540,6 +540,22 @@ let whd_meta metamap c = match kind_of_term c with let plain_instance s c = let rec irec u = match kind_of_term u with | Meta p -> (try List.assoc p s with Not_found -> u) + | App (f,l) when isCast f -> + let (f,t) = destCast f in + let l' = Array.map irec l in + (match kind_of_term f with + | Meta p -> + (* Don't flatten application nodes: this is used to extract a + proof-term from a proof-tree and we want to keep the structure + of the proof-tree *) + (try let g = List.assoc p s in + match kind_of_term g with + | App _ -> + let h = id_of_string "H" in + mkLetIn (Name h,g,t,mkApp(mkRel 1,Array.map (lift 1) l')) + | _ -> mkApp (g,l') + with Not_found -> mkApp (f,l')) + | _ -> mkApp (irec f,l')) | Cast (m,_) when isMeta m -> (try List.assoc (destMeta m) s with Not_found -> u) | _ -> map_constr irec u diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 3c746b49d..aa5d27d20 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -67,13 +67,13 @@ let typeur sigma metamap = | Ind ind -> body_of_type (type_of_inductive env ind) | Construct cstr -> body_of_type (type_of_constructor env cstr) | Case (_,p,c,lf) -> - (* TODO: could avoid computing the type of branches *) - let i = - try find_rectype env (type_of env c) + let Inductiveops.IndType(_,realargs) = + try Inductiveops.find_rectype env sigma (type_of env c) with Not_found -> anomaly "type_of: Bad recursive type" in - let pj = { uj_val = p; uj_type = type_of env p } in - let (_,ty,_) = type_case_branches env i pj c in - ty + let t = whd_beta (applist (p, realargs)) in + (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with + | Prod _ -> whd_beta (applist (t, [c])) + | _ -> t) | Lambda (name,c1,c2) -> mkProd (name, c1, type_of (push_rel (name,None,c1) env) c2) | LetIn (name,b,c1,c2) -> @@ -101,7 +101,7 @@ let typeur sigma metamap = | _ -> outsort env sigma (type_of env t) and sort_family_of env t = - match kind_of_term (whd_betadeltaiota env sigma t) with + match kind_of_term t with | Cast (c,s) when isSort s -> family_of_sort (destSort s) | Sort (Prop c) -> InType | Sort (Type u) -> InType diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 8b47ced02..a3e18f150 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -35,7 +35,7 @@ open Safe_typing type proof_topstate = { top_hyps : named_context * named_context; top_goal : goal; - top_strength : bool * Libnames.strength; + top_strength : Decl_kinds.goal_kind; top_hook : declaration_hook } let proof_edits = diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index beeb56959..4ddcc5c8d 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -14,7 +14,7 @@ open Names open Term open Sign open Environ -open Nametab +open Decl_kinds open Proof_type open Tacmach (*i*) @@ -67,7 +67,7 @@ val get_undo : unit -> int option declare the built constructions as a coercion or a setoid morphism) *) val start_proof : - identifier -> bool * Libnames.strength -> named_context -> constr + identifier -> goal_kind -> named_context -> constr -> declaration_hook -> unit (* [restart_proof ()] restarts the current focused proof from the beginning @@ -91,12 +91,11 @@ val resume_proof : identifier -> unit val suspend_proof : unit -> unit (*s [cook_proof opacity] turns the current proof (assumed completed) into - a constant with its name, strength and possible hook (see [start_proof]); + a constant with its name, kind and possible hook (see [start_proof]); it fails if there is no current proof of if it is not completed *) val cook_proof : unit -> - identifier * - (Entries.definition_entry * (bool * Libnames.strength) * declaration_hook) + identifier * (Entries.definition_entry * goal_kind * declaration_hook) (* To export completed proofs to xml *) val set_xml_cook_proof : (pftreestate -> unit) -> unit diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index a05464b00..86ec64c76 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -176,7 +176,7 @@ let prgl gl = (str"[" ++ pgl ++ str"]" ++ spc ()) let pr_evgl gl = - let phyps = pr_idl (ids_of_named_context gl.evar_hyps) in + let phyps = pr_idl (List.rev (ids_of_named_context gl.evar_hyps)) in let pc = prterm gl.evar_concl in hov 0 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pc ++ str"]") diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 3d599cc48..e3d52c5b3 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -100,4 +100,4 @@ type closed_generic_argument = type 'a closed_abstract_argument_type = ('a,constr,raw_tactic_expr) abstract_argument_type -type declaration_hook = Libnames.strength -> global_reference -> unit +type declaration_hook = Decl_kinds.strength -> global_reference -> unit diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 6f86fbe3a..95bf5d3a2 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -128,4 +128,4 @@ type closed_generic_argument = type 'a closed_abstract_argument_type = ('a,constr,raw_tactic_expr) abstract_argument_type -type declaration_hook = Libnames.strength -> global_reference -> unit +type declaration_hook = Decl_kinds.strength -> global_reference -> unit diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 071f14330..16b13ac9e 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -232,7 +232,12 @@ let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it Their proof should be completed in order to complete the initial proof *) let extract_open_proof sigma pf = - let meta_cnt = ref 0 in + let next_meta = + let meta_cnt = ref 0 in + let rec f () = + incr meta_cnt; if in_dom sigma !meta_cnt then f () else !meta_cnt + in f + in let open_obligations = ref [] in let rec proof_extractor vl = function | {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf @@ -259,10 +264,9 @@ let extract_open_proof sigma pf = let (_,c,ty) = Sign.lookup_named id goal.evar_hyps in mkNamedProd_or_LetIn (id,c,ty) concl) sorted_rels goal.evar_concl in - incr meta_cnt; - open_obligations := (!meta_cnt,abs_concl):: !open_obligations; - applist - (mkMeta !meta_cnt, List.map (fun (n,_) -> mkRel n) sorted_rels) + let meta = next_meta () in + open_obligations := (meta,abs_concl):: !open_obligations; + applist (mkMeta meta, List.map (fun (n,_) -> mkRel n) sorted_rels) | _ -> anomaly "Bug : a case has been forgotten in proof_extractor" in diff --git a/scripts/coqc.ml b/scripts/coqc.ml index cd1898f15..fc1e57d78 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -136,7 +136,7 @@ let parse_args () = | "-R" as o :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem | ("-notactics"|"-debug"|"-db"|"-debugger"|"-nolib"|"-batch"|"-nois" |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" - |"-silent"|"-m" as o) :: rem -> + |"-silent"|"-m"|"-xml" as o) :: rem -> parse (cfiles,o::args) rem | ("-v"|"--version") :: _ -> Usage.version () diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 36e0fa23f..adc2054fe 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -35,6 +35,7 @@ open Tactics open Inv open Vernacexpr open Safe_typing +open Decl_kinds let not_work_message = "tactic fails to build the inversion lemma, may be because the predicate has arguments that depend on other arguments" @@ -248,7 +249,7 @@ let add_inversion_lemma name env sigma t sort dep inv_op = (DefinitionEntry { const_entry_body = invProof; const_entry_type = None; const_entry_opaque = false }, - Libnames.NeverDischarge) + IsProof Lemma) in () (* open Pfedit *) diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 8c2077f46..3a4ae8e13 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -30,6 +30,7 @@ open Tacticals open Vernacexpr open Safe_typing open Nametab +open Decl_kinds type setoid = { set_a : constr; @@ -297,12 +298,12 @@ let add_setoid a aeq th = ((DefinitionEntry {const_entry_body = eq_morph; const_entry_type = Some eq_morph_typ; const_entry_opaque = true}), - Libnames.NeverDischarge) in + IsProof Lemma) in let _ = Declare.declare_constant eq_ext_name2 ((DefinitionEntry {const_entry_body = eq_morph2; const_entry_type = Some eq_morph2_typ; const_entry_opaque = true}), - Libnames.NeverDischarge) in + IsProof Lemma) in let eqmorph = (current_constant eq_ext_name) in let eqmorph2 = (current_constant eq_ext_name2) in (Lib.add_anonymous_leaf @@ -415,8 +416,7 @@ let new_morphism m id hook = let lem = (gen_compat_lemma env m body args_t poss) in let lemast = (ast_of_constr true env lem) in new_edited id m poss; - start_proof_com (Some id) (false,Libnames.NeverDischarge) - ([],lemast) hook; + start_proof_com (Some id) (IsGlobal DefinitionBody) ([],lemast) hook; (Options.if_verbose Vernacentries.show_open_subgoals ())) let rec sub_bool l1 n = function @@ -511,7 +511,7 @@ let add_morphism lem_name (m,profil) = ((DefinitionEntry {const_entry_body = lem_2; const_entry_type = None; const_entry_opaque = true}), - Libnames.NeverDischarge) in + IsProof Lemma) in let lem2 = (current_constant lem2_name) in (Lib.add_anonymous_leaf (morphism_to_obj (m, diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 568ffd021..efa497b95 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -40,6 +40,7 @@ open Safe_typing open Typing open Hiddentac open Genarg +open Decl_kinds let err_msg_tactic_not_found macro_loc macro = user_err_loc @@ -1277,7 +1278,7 @@ and letin_interp ist = function (match ist.goalopt with | None -> Global.named_context () | Some g -> pf_hyps g) in - start_proof id (true,NeverDischarge) ndc typ (fun _ _ -> ()); + start_proof id IsLocal ndc typ (fun _ _ -> ()); by t; let (_,({const_entry_body = pft; const_entry_type = _},_,_)) = cook_proof () in @@ -1324,7 +1325,7 @@ and letcut_interp ist = function | _ -> (try let t = tactic_of_value tac in - start_proof id (false,NeverDischarge) ndc typ (fun _ _ -> ()); + start_proof id IsLocal ndc typ (fun _ _ -> ()); by t; let (_,({const_entry_body = pft; const_entry_type = _},_,_)) = cook_proof () in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index bca15185c..5978e1070 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -38,6 +38,7 @@ open Hipattern open Coqlib open Nametab open Tacexpr +open Decl_kinds exception Bound @@ -1622,8 +1623,8 @@ let abstract_subproof name tac gls = in if occur_existential concl then error "Abstract cannot handle existentials"; let lemme = - start_proof na (false,NeverDischarge) current_sign concl (fun _ _ -> ()); - let _,(const,(_,strength),_) = + start_proof na (IsGlobal (Proof Lemma)) current_sign concl (fun _ _ -> ()); + let _,(const,kind,_) = try by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)); let r = cook_proof () in @@ -1632,7 +1633,7 @@ let abstract_subproof name tac gls = (delete_current_proof(); raise e) in (* Faudrait un peu fonctionnaliser cela *) let cd = Entries.DefinitionEntry const in - let sp = Declare.declare_constant na (cd,strength) in + let sp = Declare.declare_constant na (cd,IsProof Lemma) in let newenv = Global.env() in Declare.constr_of_reference (ConstRef (snd sp)) in diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index d9b7aaa8d..aec2f82f9 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -181,7 +181,7 @@ let variables l = print "override OPT=-byte\n" else print "OPT=\n"; - print "COQFLAGS=-q $(OPT) $(COQLIBS)\n"; + print "COQFLAGS=-q $(OPT) $(COQLIBS) $(COQ_XML)\n"; print "COQC=$(COQBIN)coqc\n"; print "GALLINA=gallina\n"; print "COQDOC=coqdoc\n"; diff --git a/tools/coq_vo2xml.ml b/tools/coq_vo2xml.ml index 9b47fed03..5f71fca39 100644 --- a/tools/coq_vo2xml.ml +++ b/tools/coq_vo2xml.ml @@ -65,7 +65,6 @@ let compile command args file = Unix.stdin in let oc = open_out tmpfile in - Printf.fprintf oc "Require Xml.\n" ; Printf.fprintf oc "Require %s.\n" modulename; Printf.fprintf oc "Print XML Module Disk \"%s\" %s.\n" !xml_library_root modulename; diff --git a/toplevel/class.ml b/toplevel/class.ml index d3acbe66b..1a252dc13 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -24,6 +24,7 @@ open Classops open Declare open Libnames open Nametab +open Decl_kinds open Safe_typing let strength_min4 stre1 stre2 stre3 stre4 = @@ -37,7 +38,7 @@ let id_of_varid c = match kind_of_term c with lc liste des variable dont depend la classe source *) let rec stre_unif_cond = function - | ([],[]) -> NeverDischarge + | ([],[]) -> Global | (v::l,[]) -> variable_strength v | ([],v::l) -> variable_strength v | (v1::l1,v2::l2) -> @@ -213,7 +214,7 @@ let get_strength stre ref cls clt = (* 01/00: Supprimé la prise en compte de la force des variables locales. Sens ? let streunif = stre_unif_cond (s_vardep,f_vardep) in *) - let streunif = NeverDischarge in + let streunif = Global in let stre' = strength_min4 stres stret stref streunif in strength_min (stre,stre') @@ -265,7 +266,7 @@ let build_id_coercion idf_opt source = { const_entry_body = mkCast (val_f, typ_f); const_entry_type = Some typ_f; const_entry_opaque = false } in - let (_,kn) = declare_constant idf (constr_entry,NeverDischarge) in + let (_,kn) = declare_constant idf (constr_entry,Decl_kinds.IsDefinition) in ConstRef kn (* diff --git a/toplevel/class.mli b/toplevel/class.mli index 8e9bcc3c3..671219c3c 100644 --- a/toplevel/class.mli +++ b/toplevel/class.mli @@ -14,6 +14,7 @@ open Term open Classops open Declare open Libnames +open Decl_kinds open Nametab (*i*) diff --git a/toplevel/command.ml b/toplevel/command.ml index fd2041d31..29edcc866 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -36,6 +36,7 @@ open Nametab open Typeops open Indtypes open Vernacexpr +open Decl_kinds let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b)) let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b)) @@ -92,36 +93,34 @@ let red_constant_entry ce = function { ce with const_entry_body = reduction_of_redexp red (Global.env()) Evd.empty body } -let declare_global_definition ident ce n local = - let (_,kn) = declare_constant ident (DefinitionEntry ce,n) in - if local then +let declare_global_definition ident ce local = + let (_,kn) = declare_constant ident (DefinitionEntry ce,IsDefinition) in + if local = Local then msg_warning (pr_id ident ++ str" is declared as a global definition"); if_verbose message ((string_of_id ident) ^ " is defined"); ConstRef kn -let declare_definition ident (local,n) bl red_option c typopt = +let declare_definition ident local bl red_option c typopt = let ce = constant_entry_of_com (bl,c,typopt,false) in if bl<>[] && red_option <> None then error "Evaluation under a local context not supported"; let ce' = red_constant_entry ce red_option in - match n with - | NeverDischarge -> declare_global_definition ident ce' n local - | DischargeAt (disch_sp,_) -> - if Lib.is_section_p disch_sp then begin - let c = + match local with + | Global -> + declare_global_definition ident ce' Global + | Local -> + if Lib.is_section_p (Lib.cwd ()) then begin + let c = SectionLocalDef(ce'.const_entry_body,ce'.const_entry_type,false) in - let _ = declare_variable ident (Lib.cwd(), c, n) in - if_verbose message ((string_of_id ident) ^ " is defined"); + let _ = declare_variable ident (Lib.cwd(), c, IsDefinition) in + if_verbose message ((string_of_id ident) ^ " is defined"); if Pfedit.refining () then msgerrnl (str"Warning: Local definition " ++ pr_id ident ++ - str" is not visible from current goals"); - VarRef ident + str" is not visible from current goals"); + VarRef ident end - else - declare_global_definition ident ce' n true - | NotDeclare -> - anomalylabstrm "Command.definition_body_red" - (str "Strength NotDeclare not for Definition, only for Let") + else + declare_global_definition ident ce' Local let syntax_definition ident c = let c = interp_rawconstr Evd.empty (Global.env()) c in @@ -133,33 +132,34 @@ let syntax_definition ident c = let assumption_message id = if_verbose message ((string_of_id id) ^ " is assumed") -let declare_assumption ident n bl c = +let declare_assumption ident (local,kind) bl c = let c = prod_rawconstr c bl in let c = interp_type Evd.empty (Global.env()) c in - match n with - | NeverDischarge -> - let (_,kn) = declare_constant ident (ParameterEntry c, NeverDischarge) in - assumption_message ident; - ConstRef kn - | DischargeAt (disch_sp,_) -> - if Lib.is_section_p disch_sp then begin - let r = declare_variable ident (Lib.cwd(),SectionLocalAssum c,n) in - assumption_message ident; + match local with + | Global -> + let (_,kn) = + declare_constant ident (ParameterEntry c, IsAssumption kind) in + assumption_message ident; + ConstRef kn + | Local -> + if Lib.is_section_p (Lib.cwd ()) then begin + let r = + declare_variable ident + (Lib.cwd(), SectionLocalAssum c, IsAssumption kind) in + assumption_message ident; if is_verbose () & Pfedit.refining () then msgerrnl (str"Warning: Variable " ++ pr_id ident ++ - str" is not visible from current goals"); - VarRef ident + str" is not visible from current goals"); + VarRef ident end - else - let (_,kn) = declare_constant ident (ParameterEntry c, NeverDischarge) in - assumption_message ident; - if_verbose - msg_warning (pr_id ident ++ str" is declared as a parameter" ++ - str" because it is at a global level"); - ConstRef kn - | NotDeclare -> - anomalylabstrm "Command.hypothesis_def_var" - (str "Strength NotDeclare not for Variable, only for Let") + else + let (_,kn) = + declare_constant ident (ParameterEntry c, IsAssumption kind) in + assumption_message ident; + if_verbose + msg_warning (pr_id ident ++ str" is declared as a parameter" ++ + str" because it is at a global level"); + ConstRef kn (* 3| Mutual Inductive definitions *) @@ -280,8 +280,7 @@ let build_mutual lind finite = let _ = declare_mutual_with_eliminations mie in List.iter (fun id -> - Class.try_add_new_coercion - (locate (make_short_qualid id)) NeverDischarge) coes + Class.try_add_new_coercion (locate (make_short_qualid id)) Global) coes (* try to find non recursive definitions *) @@ -333,7 +332,7 @@ let build_recursive lnameargsardef = let raw_arity = mkProdCit lparams arityc in let arity = interp_type sigma env0 raw_arity in let _ = declare_variable recname - (Lib.cwd(),SectionLocalAssum arity, NeverDischarge) in + (Lib.cwd(),SectionLocalAssum arity, IsAssumption Definitional) in (Environ.push_named (recname,None,arity) env, (arity::arl))) (env0,[]) lnameargsardef with e -> @@ -351,7 +350,6 @@ let build_recursive lnameargsardef = States.unfreeze fs; let (lnonrec,(namerec,defrec,arrec,nvrec)) = collect_non_rec env0 lrecnames recdef arityl (Array.to_list nv) in - let n = NeverDischarge in let recvec = Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in @@ -360,7 +358,7 @@ let build_recursive lnameargsardef = { const_entry_body = mkFix ((nvrec,i),recdecls); const_entry_type = Some arrec.(i); const_entry_opaque = false } in - let (_,kn) = declare_constant fi (DefinitionEntry ce, n) in + let (_,kn) = declare_constant fi (DefinitionEntry ce, IsDefinition) in (ConstRef kn) in (* declare the recursive definitions *) @@ -374,7 +372,7 @@ let build_recursive lnameargsardef = let ce = { const_entry_body = replace_vars subst def; const_entry_type = Some t; const_entry_opaque = false } in - let _ = declare_constant f (DefinitionEntry ce,n) in + let _ = declare_constant f (DefinitionEntry ce, IsDefinition) in warning ((string_of_id f)^" is non-recursively defined"); (var_subst f) :: subst) (List.map var_subst (Array.to_list namerec)) @@ -394,7 +392,7 @@ let build_corecursive lnameardef = let arj = type_judgment_of_rawconstr Evd.empty env0 arityc in let arity = arj.utj_val in let _ = declare_variable recname - (Lib.cwd(),SectionLocalAssum arj.utj_val,NeverDischarge) in + (Lib.cwd(),SectionLocalAssum arj.utj_val,IsAssumption Definitional) in (Environ.push_named (recname,None,arity) env, (arity::arl))) (env0,[]) lnameardef with e -> @@ -412,7 +410,6 @@ let build_corecursive lnameardef = States.unfreeze fs; let (lnonrec,(namerec,defrec,arrec,_)) = collect_non_rec env0 lrecnames recdef arityl [] in - let n = NeverDischarge in let recvec = Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in @@ -422,7 +419,7 @@ let build_corecursive lnameardef = const_entry_type = Some (arrec.(i)); const_entry_opaque = false } in - let _,kn = declare_constant fi (DefinitionEntry ce,n) in + let _,kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in (ConstRef kn) in let lrefrec = Array.mapi declare namerec in @@ -434,7 +431,7 @@ let build_corecursive lnameardef = let ce = { const_entry_body = replace_vars subst def; const_entry_type = Some t; const_entry_opaque = false } in - let _ = declare_constant f (DefinitionEntry ce,n) in + let _ = declare_constant f (DefinitionEntry ce,IsDefinition) in warning ((string_of_id f)^" is non-recursively defined"); (var_subst f) :: subst) (List.map var_subst (Array.to_list namerec)) @@ -454,7 +451,6 @@ let build_scheme lnamedepindsort = (ind,mib,mip,dep,interp_elimination_sort sort)) lnamedepindsort in - let n = NeverDischarge in let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in let rec declare decl fi lrecref = let decltype = Retyping.get_type_of env0 Evd.empty decl in @@ -462,7 +458,7 @@ let build_scheme lnamedepindsort = let ce = { const_entry_body = decl; const_entry_type = Some decltype; const_entry_opaque = false } in - let _,kn = declare_constant fi (DefinitionEntry ce,n) in + let _,kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in ConstRef kn :: lrecref in let lrecref = List.fold_right2 declare listdecl lrecnames [] in @@ -480,7 +476,7 @@ let rec binders_length = function | LocalRawDef _::bl -> 1 + binders_length bl | LocalRawAssum (idl,_)::bl -> List.length idl + binders_length bl -let start_proof_com sopt (local,stre) (bl,t) hook = +let start_proof_com sopt kind (bl,t) hook = let env = Global.env () in let sign = Global.named_context () in let sign = clear_proofs sign in @@ -496,7 +492,7 @@ let start_proof_com sopt (local,stre) (bl,t) hook = in let c = interp_type Evd.empty env (generalize_rawconstr t bl) in let _ = Typeops.infer_type env c in - Pfedit.start_proof id (local,stre) sign c hook + Pfedit.start_proof id kind sign c hook let apply_tac_not_declare id pft = function | None -> error "Type of Let missing" @@ -506,26 +502,22 @@ let apply_tac_not_declare id pft = function Pfedit.delete_current_proof (); Pfedit.by (Refiner.tclTHENSV cutt [|introduction id;exat|]) -let save id const (local,strength) hook = +let save id const kind hook = let {const_entry_body = pft; const_entry_type = tpo; const_entry_opaque = opacity } = const in - begin match strength with - | DischargeAt (disch_sp,_) when Lib.is_section_p disch_sp && local -> + begin match kind with + | IsLocal -> let c = SectionLocalDef (pft, tpo, opacity) in - let _ = declare_variable id (Lib.cwd(), c, strength) in - hook strength (VarRef id) - | NeverDischarge | DischargeAt _ -> - let _,kn = declare_constant id (DefinitionEntry const,strength) in - let ref = ConstRef kn in - hook strength ref - | NotDeclare -> apply_tac_not_declare id pft tpo + let _ = declare_variable id (Lib.cwd(), c, IsDefinition) in + hook Local (VarRef id) + | IsGlobal k -> + let k = theorem_kind_of_goal_kind k in + let _,kn = declare_constant id (DefinitionEntry const, k) in + hook Global (ConstRef kn) end; - if not (strength = NotDeclare) then - begin - Pfedit.delete_current_proof (); - if_verbose message ((string_of_id id) ^ " is defined") - end + Pfedit.delete_current_proof (); + if_verbose message ((string_of_id id) ^ " is defined") let save_named opacity = let id,(const,persistence,hook) = Pfedit.cook_proof () in @@ -545,12 +537,12 @@ let save_anonymous opacity save_ident = check_anonymity id save_ident; save save_ident const persistence hook -let save_anonymous_with_strength strength opacity save_ident = +let save_anonymous_with_strength kind opacity save_ident = let id,(const,_,hook) = Pfedit.cook_proof () in let const = { const with const_entry_opaque = opacity } in check_anonymity id save_ident; (* we consider that non opaque behaves as local for discharge *) - save save_ident const (not opacity,strength) hook + save save_ident const (IsGlobal (Proof kind)) hook let get_current_context () = try Pfedit.get_current_goal_context () diff --git a/toplevel/command.mli b/toplevel/command.mli index 88da5394a..9b3d99619 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -12,12 +12,13 @@ open Util open Names open Term +open Nametab open Declare open Library open Libnames open Nametab open Vernacexpr - +open Decl_kinds (*i*) (*s Declaration functions. The following functions take ASTs, @@ -25,16 +26,16 @@ open Vernacexpr functions of [Declare]; they return an absolute reference to the defined object *) -val declare_definition : identifier -> bool * strength -> +val declare_definition : identifier -> definition_kind -> local_binder list -> Tacred.red_expr option -> Coqast.t -> Coqast.t option -> global_reference val syntax_definition : identifier -> Coqast.t -> unit -val declare_assumption : identifier -> strength -> +val declare_assumption : identifier -> assumption_kind -> local_binder list -> Coqast.t -> global_reference -val build_mutual : Vernacexpr.inductive_expr list -> bool -> unit +val build_mutual : inductive_expr list -> bool -> unit val declare_mutual_with_eliminations : Entries.mutual_inductive_entry -> mutual_inductive @@ -49,7 +50,7 @@ val build_scheme : (identifier * bool * qualid located * Coqast.t) list -> unit val generalize_rawconstr : Coqast.t -> local_binder list -> Coqast.t -val start_proof_com : identifier option -> bool * strength -> +val start_proof_com : identifier option -> goal_kind -> (local_binder list * Coqast.t) -> Proof_type.declaration_hook -> unit (*s [save_named b] saves the current completed proof under the name it @@ -67,7 +68,7 @@ val save_anonymous : bool -> identifier -> unit declares the theorem under the name [name] and gives it the strength [strength] *) -val save_anonymous_with_strength : strength -> bool -> identifier -> unit +val save_anonymous_with_strength : theorem_kind -> bool -> identifier -> unit (* [get_current_context ()] returns the evar context and env of the current open proof if any, otherwise returns the empty evar context diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 26cf3083c..a58d20ad6 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -33,6 +33,7 @@ open Recordops open Library open Indtypes open Nametab +open Decl_kinds let recalc_sp dir sp = let (_,spid) = repr_path sp in Libnames.make_path dir spid @@ -45,17 +46,20 @@ let rec find_var id = function | [] -> false | (x,b,_)::l -> if x = id then b=None else find_var id l -let build_abstract_list hyps ids_to_discard = - let l = - List.fold_left - (fun vars id -> if find_var id hyps then mkVar id::vars else vars) - [] ids_to_discard in - Array.of_list l +let build_abstract_list sec_sp hyps ids_to_discard = + let l1,l2 = + List.split + (List.fold_left + (fun vars id -> + if find_var id hyps then (mkVar id, Libnames.make_path sec_sp id)::vars + else vars) + [] ids_to_discard) in + Array.of_list l1, l2 (* Discharge of inductives is done here (while discharge of constants is done by the kernel for efficiency). *) -let abstract_inductive ids_to_abs hyps inds = +let abstract_inductive sec_sp ids_to_abs hyps inds = let abstract_one_assum id t inds = let ntyp = List.length inds in let new_refs = @@ -82,7 +86,7 @@ let abstract_inductive ids_to_abs hyps inds = match hyps with | (hyp,None,t as d)::rest when id = hyp -> let inds' = abstract_one_assum hyp t inds in - (rest, inds', mkVar id::vars) + (rest, inds', (mkVar id, Libnames.make_path sec_sp id)::vars) | (hyp,Some b,t as d)::rest when id = hyp -> let inds' = abstract_one_def hyp b inds in (rest, inds', vars) @@ -109,9 +113,10 @@ let abstract_inductive ids_to_abs hyps inds = mind_entry_consnames = c; mind_entry_lc = shortlc }) inds' in - (inds'', Array.of_list vars) + let l1,l2 = List.split vars in + (inds'', Array.of_list l1, l2) -let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib = +let process_inductive sec_sp osecsp nsecsp oldenv (ids_to_discard,modlist) mib = assert (Array.length mib.mind_packets > 0); let finite = mib.mind_finite in let inds = @@ -135,7 +140,8 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib = (x, option_app (expmod_constr modlist) b,expmod_constr modlist t) sgn) mib.mind_hyps ~init:empty_named_context in - let (inds',abs_vars) = abstract_inductive ids_to_discard hyps' inds in + let (inds',abs_vars,discharged_hyps ) = + abstract_inductive sec_sp ids_to_discard hyps' inds in let lmodif_one_mind i = let nbc = Array.length mib.mind_packets.(i).mind_consnames in (((osecsp,i), DO_ABSTRACT ((nsecsp,i),abs_vars)), @@ -150,7 +156,8 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib = ({ mind_entry_finite = finite; mind_entry_inds = inds' }, indmodifs, - List.flatten cstrmodifs) + List.flatten cstrmodifs, + discharged_hyps) (* Discharge messages. *) @@ -175,9 +182,12 @@ let inductive_message inds = type opacity = bool type discharge_operation = - | Variable of identifier * section_variable_entry * strength * bool - | Constant of identifier * recipe * strength * constant * bool - | Inductive of mutual_inductive_entry * bool + | Variable of identifier * section_variable_entry * local_kind * bool * + Dischargedhypsmap.discharged_hyps + | Constant of identifier * recipe * global_kind * constant * bool * + Dischargedhypsmap.discharged_hyps + | Inductive of mutual_inductive_entry * bool * + Dischargedhypsmap.discharged_hyps | Class of cl_typ * cl_info_typ | Struc of inductive * (unit -> struc_typ) | Objdef of constant @@ -194,56 +204,31 @@ let process_object oldenv olddir full_olddir newdir let tag = object_tag lobj in match tag with | "VARIABLE" -> - let ((id,c,t),cst,stre) = - get_variable_with_constraints (basename sp) in + let ((id,c,t),cst) = get_variable_with_constraints (basename sp) in (* VARIABLE means local (entry Variable/Hypothesis/Local and are *) (* always discharged *) -(* - if stre = (DischargeAt sec_sp) or ids_to_discard <> [] then -*) - (Constraints cst :: ops, id :: ids_to_discard, work_alist) -(* - else - let imp = is_implicit_var sp in - let newdecl = - match c with - | None -> - SectionLocalAssum - (expmod_constr oldenv work_alist t) - | Some body -> - SectionLocalDef - (expmod_constr oldenv work_alist body) - in - (Variable (id,newdecl,stre,sticky,imp) :: ops, - ids_to_discard,work_alist) -*) + (Constraints cst :: ops, id :: ids_to_discard, work_alist) | ("CONSTANT" | "PARAMETER") -> (* CONSTANT/PARAMETER means never discharge (though visibility *) (* may vary) *) - let stre = constant_strength sp in -(* - if stre = (DischargeAt sec_sp) then - let cb = Environ.lookup_constant sp oldenv in - let constl = (sp, DO_REPLACE cb)::constl in - (ops, ids_to_discard, (constl,indl,cstrl)) - else -*) + let kind = constant_kind sp in let kn = Nametab.locate_constant (qualid_of_sp sp) in let lab = label kn in let cb = Environ.lookup_constant kn oldenv in let imp = is_implicit_constant kn in - let newkn = (*match stre with (* this did not work anyway...*) - | DischargeAt (d,_) when not (is_dirpath_prefix_of d dir) -> kn - | _ -> *)recalc_kn newdir kn in - let mods = - let abs_vars = build_abstract_list cb.const_hyps ids_to_discard in - [ (kn, DO_ABSTRACT(newkn,abs_vars)) ] + let newkn = recalc_kn newdir kn in + let abs_vars,discharged_hyps0 = + build_abstract_list full_olddir cb.const_hyps ids_to_discard in + (* let's add the new discharged hypothesis to those already discharged*) + let discharged_hyps = + discharged_hyps0 @ Dischargedhypsmap.get_discharged_hyps sp in + let mods = [ (kn, DO_ABSTRACT(newkn,abs_vars)) ] in let r = { d_from = cb; d_modlist = work_alist; d_abstract = ids_to_discard } in - let op = Constant (id_of_label lab, r,stre,newkn,imp) in + let op = Constant (id_of_label lab,r,kind,newkn,imp,discharged_hyps) in (op :: ops, ids_to_discard, (mods@constl, indl, cstrl)) | "INDUCTIVE" -> @@ -251,14 +236,17 @@ let process_object oldenv olddir full_olddir newdir let mib = Environ.lookup_mind kn oldenv in let newkn = recalc_kn newdir kn in let imp = is_implicit_args() (* CHANGE *) in - let (mie,indmods,cstrmods) = - process_inductive kn newkn oldenv (ids_to_discard,work_alist) mib in - ((Inductive(mie,imp)) :: ops, ids_to_discard, + let (mie,indmods,cstrmods,discharged_hyps0) = + process_inductive full_olddir kn newkn oldenv (ids_to_discard,work_alist) mib in + (* let's add the new discharged hypothesis to those already discharged*) + let discharged_hyps = + discharged_hyps0 @ Dischargedhypsmap.get_discharged_hyps sp in + ((Inductive(mie,imp,discharged_hyps)) :: ops, ids_to_discard, (constl,indmods@indl,cstrmods@cstrl)) | "CLASS" -> let ((cl,clinfo) as x) = outClass lobj in - if (match clinfo.cl_strength with DischargeAt (dp,_) -> dp = full_olddir | _ -> false) then + if clinfo.cl_strength = Local then (ops,ids_to_discard,work_alist) else let (y1,y2) = process_class olddir ids_to_discard x in @@ -266,7 +254,7 @@ let process_object oldenv olddir full_olddir newdir | "COERCION" -> let (((_,coeinfo),_,_)as x) = outCoercion lobj in - if (match coercion_strength coeinfo with DischargeAt (dp,_) -> dp = full_olddir | _ -> false) then + if coercion_strength coeinfo = Local then (ops,ids_to_discard,work_alist) else let y = process_coercion olddir ids_to_discard x in @@ -299,16 +287,15 @@ let process_item oldenv olddir full_olddir newdir acc = function | (_,_) -> acc let process_operation = function - | Variable (id,expmod_a,stre,imp) -> + | Variable (id,expmod_a,stre,imp,discharged_hyps) -> (* Warning:parentheses needed to get a side-effect from with_implicits *) - let _ = - with_implicits imp (declare_variable id) (Lib.cwd(),expmod_a,stre) in - () - | Constant (id,r,stre,kn,imp) -> - with_implicits imp (redeclare_constant id) (r,stre); + with_implicits imp (redeclare_variable id discharged_hyps) + (Lib.cwd(),expmod_a,stre) + | Constant (id,r,stre,kn,imp,discharged_hyps) -> + with_implicits imp (redeclare_constant id discharged_hyps) (r,stre); constant_message id - | Inductive (mie,imp) -> - let _ = with_implicits imp declare_mind mie in + | Inductive (mie,imp,discharged_hyps) -> + let _ = with_implicits imp (redeclare_inductive discharged_hyps) mie in inductive_message mie.mind_entry_inds | Class (y1,y2) -> Lib.add_anonymous_leaf (inClass (y1,y2)) diff --git a/toplevel/record.ml b/toplevel/record.ml index 60855b2fc..909cef6d0 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $:Id$ *) +(* $Id$ *) open Pp open Util @@ -25,7 +25,7 @@ open Astterm open Command open Inductive open Safe_typing -open Nametab +open Decl_kinds open Indtypes open Type_errors @@ -178,14 +178,14 @@ let declare_projections indsp coers fields = const_entry_body = proj; const_entry_type = Some projtyp; const_entry_opaque = false } in - declare_constant fid (DefinitionEntry cie,NeverDischarge) + declare_constant fid (DefinitionEntry cie,IsDefinition) with Type_errors.TypeError (ctx,te) -> raise (NotDefinable (BadTypedProj (fid,ctx,te))) in let refi = ConstRef kn in let constr_fi = mkConst kn in if coe then begin let cl = Class.class_of_ref (IndRef indsp) in - Class.try_add_new_coercion_with_source refi NeverDischarge cl + Class.try_add_new_coercion_with_source refi Global cl end; let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in let constr_fip = applist (constr_fi,proj_args) in @@ -228,5 +228,5 @@ let definition_structure ((is_coe,idstruc),ps,cfs,idbuild,s) = let rsp = (sp,0) in (* This is ind path of idstruc *) let sp_projs = declare_projections rsp coers fields in let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *) - if is_coe then Class.try_add_new_coercion build NeverDischarge; + if is_coe then Class.try_add_new_coercion build Global; Recordops.add_new_struc (rsp,idbuild,nparams,List.rev sp_projs) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 3c994cdc8..6054881f5 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -52,6 +52,9 @@ let print_usage_channel co command = -boot boot mode (implies -q and -batch) -emacs tells Coq it is executed under Emacs -dump-glob f dump globalizations in file f (to be used by coqdoc) + -xml exports XML files either to the hierarchy rooted in + the directory $COQ_XML_LIBRARY_ROOT (if set) or to + stdout (if unset) " (* print the usage on standard error *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index d9baaa79c..3b899d889 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -30,6 +30,7 @@ open Goptions open Libnames open Nametab open Vernacexpr +open Decl_kinds (* Pcoq hooks *) @@ -312,70 +313,51 @@ let vernac_notation = Metasyntax.add_notation (***********) (* Gallina *) -let interp_assumption = function - | (AssumptionHypothesis | AssumptionVariable) -> Declare.make_strength_0 () - | (AssumptionAxiom | AssumptionParameter) -> Libnames.NeverDischarge - -let interp_definition = function - | Definition -> (false, Libnames.NeverDischarge) - | LocalDefinition -> (true, Declare.make_strength_0 ()) - -let interp_theorem = function - | (Theorem | Lemma | Decl) -> Libnames.NeverDischarge - | Fact -> Declare.make_strength_1 () - | Remark -> Declare.make_strength_0 () - -let interp_goal = function - | StartTheoremProof x -> (false, interp_theorem x) - | StartDefinitionBody x -> interp_definition x - let start_proof_and_print idopt k t hook = start_proof_com idopt k t hook; print_subgoals (); if !pcoq <> None then (out_some !pcoq).start_proof () -let vernac_definition kind id def hook = - let (local,stre as k) = interp_definition kind in +let vernac_definition local id def hook = match def with | ProveBody (bl,t) -> (* local binders, typ *) if Lib.is_specification () then - let ref = declare_assumption id stre bl t in - hook stre ref + let ref = declare_assumption id (local,Definitional) bl t in + hook local ref else let hook _ _ = () in - start_proof_and_print (Some id) k (bl,t) hook + let kind = if local=Local then IsLocal else IsGlobal DefinitionBody in + start_proof_and_print (Some id) kind (bl,t) hook | DefineBody (bl,red_option,c,typ_opt) -> let red_option = match red_option with | None -> None | Some r -> let (evc,env)= Command.get_current_context () in Some (interp_redexp env evc r) in - let ref = declare_definition id k bl red_option c typ_opt in - hook stre ref + let ref = declare_definition id local bl red_option c typ_opt in + hook local ref let vernac_start_proof kind sopt (bl,t) lettop hook = if not(refining ()) then if lettop then errorlabstrm "Vernacentries.StartProof" (str "Let declarations can only be used in proof editing mode"); - let stre = interp_theorem kind in match Lib.is_specification (), sopt with | true, Some id -> let t = generalize_rawconstr t bl in - let ref = declare_assumption id stre [] t in - hook stre ref + let ref = declare_assumption id (Global,Logical) [] t in + hook Global ref | _ -> (* an explicit Goal command starts the refining mode even in a specification *) - start_proof_and_print sopt (false, stre) (bl,t) hook + start_proof_and_print sopt (IsGlobal (Proof kind)) (bl,t) hook let vernac_end_proof is_opaque idopt = if_verbose show_script (); match idopt with | None -> save_named is_opaque | Some (id,None) -> save_anonymous is_opaque id - | Some (id,Some kind) -> - save_anonymous_with_strength (interp_theorem kind) is_opaque id + | Some (id,Some kind) -> save_anonymous_with_strength kind is_opaque id (* A stupid macro that should be replaced by ``Exact c. Save.'' all along the theories [??] *) @@ -384,12 +366,11 @@ let vernac_exact_proof c = by (Tactics.exact_proof c); save_named true -let vernac_assumption kind l = - let stre = interp_assumption kind in +let vernac_assumption (islocal,_ as kind) l = List.iter (fun (is_coe,(id,c)) -> - let r = declare_assumption id stre [] c in - if is_coe then Class.try_add_new_coercion r stre) l + let r = declare_assumption id kind [] c in + if is_coe then Class.try_add_new_coercion r islocal) l let vernac_inductive f indl = build_mutual indl f @@ -840,7 +821,8 @@ let vernac_goal = function | None -> () | Some c -> if not (refining()) then begin - start_proof_com None (false,Libnames.NeverDischarge) c (fun _ _ ->()); + let unnamed_kind = Lemma (* Arbitrary *) in + start_proof_com None (IsGlobal (Proof unnamed_kind)) c (fun _ _ ->()); print_subgoals () end else error "repeated Goal not permitted in refining mode" diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index d7091bfa2..122c0b0b2 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -15,6 +15,7 @@ open Tacexpr open Extend open Genarg open Symbols +open Decl_kinds (* Toplevel control exceptions *) exception ProtectedLoop @@ -85,27 +86,6 @@ type showable = | ExplainProof of int list | ExplainTree of int list -type theorem_kind = - | Theorem - | Lemma - | Decl - | Fact - | Remark - -type definition_kind = - | Definition - | LocalDefinition - -type goal_kind = - | StartTheoremProof of theorem_kind - | StartDefinitionBody of definition_kind - -type assumption_kind = - | AssumptionHypothesis - | AssumptionVariable - | AssumptionAxiom - | AssumptionParameter - type comment = | CommentConstr of constr_ast | CommentString of string |