diff options
41 files changed, 514 insertions, 378 deletions
@@ -77,7 +77,8 @@ kernel/term_typing.cmi: kernel/univ.cmi kernel/typeops.cmi kernel/term.cmi \ kernel/entries.cmi kernel/declarations.cmi kernel/cooking.cmi kernel/type_errors.cmi: kernel/term.cmi kernel/names.cmi kernel/environ.cmi kernel/typeops.cmi: kernel/univ.cmi kernel/term.cmi kernel/sign.cmi \ - kernel/names.cmi kernel/environ.cmi kernel/entries.cmi + kernel/names.cmi kernel/environ.cmi kernel/entries.cmi \ + kernel/declarations.cmi kernel/univ.cmi: lib/pp.cmi kernel/names.cmi kernel/vconv.cmi: kernel/term.cmi kernel/reduction.cmi kernel/names.cmi \ kernel/environ.cmi @@ -829,12 +830,12 @@ kernel/sign.cmo: lib/util.cmi kernel/term.cmi kernel/names.cmi \ kernel/sign.cmi kernel/sign.cmx: lib/util.cmx kernel/term.cmx kernel/names.cmx \ kernel/sign.cmi -kernel/subtyping.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi \ - kernel/reduction.cmi kernel/names.cmi kernel/modops.cmi \ +kernel/subtyping.cmo: lib/util.cmi kernel/univ.cmi kernel/typeops.cmi \ + kernel/term.cmi kernel/reduction.cmi kernel/names.cmi kernel/modops.cmi \ kernel/mod_subst.cmi kernel/inductive.cmi kernel/environ.cmi \ kernel/entries.cmi kernel/declarations.cmi kernel/subtyping.cmi -kernel/subtyping.cmx: lib/util.cmx kernel/univ.cmx kernel/term.cmx \ - kernel/reduction.cmx kernel/names.cmx kernel/modops.cmx \ +kernel/subtyping.cmx: lib/util.cmx kernel/univ.cmx kernel/typeops.cmx \ + kernel/term.cmx kernel/reduction.cmx kernel/names.cmx kernel/modops.cmx \ kernel/mod_subst.cmx kernel/inductive.cmx kernel/environ.cmx \ kernel/entries.cmx kernel/declarations.cmx kernel/subtyping.cmi kernel/term.cmo: lib/util.cmi kernel/univ.cmi lib/pp.cmi kernel/names.cmi \ @@ -955,14 +956,14 @@ library/dischargedhypsmap.cmx: lib/util.cmx kernel/term.cmx \ kernel/names.cmx library/libobject.cmx library/libnames.cmx \ library/lib.cmx kernel/inductive.cmx kernel/environ.cmx \ kernel/declarations.cmx library/dischargedhypsmap.cmi -library/global.cmo: lib/util.cmi kernel/term.cmi library/summary.cmi \ - kernel/sign.cmi kernel/safe_typing.cmi kernel/names.cmi \ - library/libnames.cmi kernel/inductive.cmi kernel/environ.cmi \ - library/global.cmi -library/global.cmx: lib/util.cmx kernel/term.cmx library/summary.cmx \ - kernel/sign.cmx kernel/safe_typing.cmx kernel/names.cmx \ - library/libnames.cmx kernel/inductive.cmx kernel/environ.cmx \ - library/global.cmi +library/global.cmo: lib/util.cmi kernel/typeops.cmi kernel/term.cmi \ + library/summary.cmi kernel/sign.cmi kernel/safe_typing.cmi \ + kernel/names.cmi library/libnames.cmi kernel/inductive.cmi \ + kernel/environ.cmi library/global.cmi +library/global.cmx: lib/util.cmx kernel/typeops.cmx kernel/term.cmx \ + library/summary.cmx kernel/sign.cmx kernel/safe_typing.cmx \ + kernel/names.cmx library/libnames.cmx kernel/inductive.cmx \ + kernel/environ.cmx library/global.cmi library/goptions.cmo: lib/util.cmi kernel/term.cmi library/summary.cmi \ lib/pp.cmi library/nametab.cmi kernel/names.cmi kernel/mod_subst.cmi \ library/libobject.cmi library/libnames.cmi library/lib.cmi \ @@ -971,18 +972,18 @@ library/goptions.cmx: lib/util.cmx kernel/term.cmx library/summary.cmx \ lib/pp.cmx library/nametab.cmx kernel/names.cmx kernel/mod_subst.cmx \ library/libobject.cmx library/libnames.cmx library/lib.cmx \ library/goptions.cmi -library/impargs.cmo: lib/util.cmi interp/topconstr.cmi pretyping/termops.cmi \ - kernel/term.cmi library/summary.cmi kernel/reduction.cmi lib/pp.cmi \ - library/nametab.cmi kernel/names.cmi library/libobject.cmi \ - library/libnames.cmi library/lib.cmi kernel/inductive.cmi \ - library/global.cmi kernel/environ.cmi kernel/declarations.cmi \ - library/impargs.cmi -library/impargs.cmx: lib/util.cmx interp/topconstr.cmx pretyping/termops.cmx \ - kernel/term.cmx library/summary.cmx kernel/reduction.cmx lib/pp.cmx \ - library/nametab.cmx kernel/names.cmx library/libobject.cmx \ - library/libnames.cmx library/lib.cmx kernel/inductive.cmx \ - library/global.cmx kernel/environ.cmx kernel/declarations.cmx \ - library/impargs.cmi +library/impargs.cmo: lib/util.cmi kernel/typeops.cmi interp/topconstr.cmi \ + pretyping/termops.cmi kernel/term.cmi library/summary.cmi \ + kernel/reduction.cmi lib/pp.cmi library/nametab.cmi kernel/names.cmi \ + library/libobject.cmi library/libnames.cmi library/lib.cmi \ + kernel/inductive.cmi library/global.cmi kernel/environ.cmi \ + kernel/declarations.cmi library/impargs.cmi +library/impargs.cmx: lib/util.cmx kernel/typeops.cmx interp/topconstr.cmx \ + pretyping/termops.cmx kernel/term.cmx library/summary.cmx \ + kernel/reduction.cmx lib/pp.cmx library/nametab.cmx kernel/names.cmx \ + library/libobject.cmx library/libnames.cmx library/lib.cmx \ + kernel/inductive.cmx library/global.cmx kernel/environ.cmx \ + kernel/declarations.cmx library/impargs.cmi library/lib.cmo: lib/util.cmi kernel/term.cmi library/summary.cmi \ kernel/sign.cmi lib/pp.cmi lib/options.cmi library/nametab.cmi \ kernel/names.cmi library/nameops.cmi library/libobject.cmi \ @@ -1221,26 +1222,28 @@ parsing/ppvernac.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ library/impargs.cmx library/goptions.cmx library/global.cmx \ interp/genarg.cmx parsing/extend.cmx parsing/egrammar.cmx \ library/declaremods.cmx library/decl_kinds.cmx parsing/ppvernac.cmi -parsing/prettyp.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ - interp/syntax_def.cmi kernel/sign.cmi kernel/safe_typing.cmi \ - pretyping/reductionops.cmi kernel/reduction.cmi pretyping/recordops.cmi \ - parsing/printmod.cmi parsing/printer.cmi lib/pp.cmi interp/notation.cmi \ - library/nametab.cmi kernel/names.cmi library/nameops.cmi \ - library/libobject.cmi library/libnames.cmi library/lib.cmi \ - pretyping/inductiveops.cmi kernel/inductive.cmi library/impargs.cmi \ - library/global.cmi pretyping/evd.cmi kernel/environ.cmi \ - library/declare.cmi kernel/declarations.cmi kernel/conv_oracle.cmi \ - interp/constrextern.cmi pretyping/classops.cmi parsing/prettyp.cmi -parsing/prettyp.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ - interp/syntax_def.cmx kernel/sign.cmx kernel/safe_typing.cmx \ - pretyping/reductionops.cmx kernel/reduction.cmx pretyping/recordops.cmx \ - parsing/printmod.cmx parsing/printer.cmx lib/pp.cmx interp/notation.cmx \ - library/nametab.cmx kernel/names.cmx library/nameops.cmx \ - library/libobject.cmx library/libnames.cmx library/lib.cmx \ - pretyping/inductiveops.cmx kernel/inductive.cmx library/impargs.cmx \ - library/global.cmx pretyping/evd.cmx kernel/environ.cmx \ - library/declare.cmx kernel/declarations.cmx kernel/conv_oracle.cmx \ - interp/constrextern.cmx pretyping/classops.cmx parsing/prettyp.cmi +parsing/prettyp.cmo: lib/util.cmi kernel/typeops.cmi pretyping/termops.cmi \ + kernel/term.cmi interp/syntax_def.cmi kernel/sign.cmi \ + kernel/safe_typing.cmi pretyping/reductionops.cmi kernel/reduction.cmi \ + pretyping/recordops.cmi parsing/printmod.cmi parsing/printer.cmi \ + lib/pp.cmi interp/notation.cmi library/nametab.cmi kernel/names.cmi \ + library/nameops.cmi library/libobject.cmi library/libnames.cmi \ + library/lib.cmi pretyping/inductiveops.cmi kernel/inductive.cmi \ + library/impargs.cmi library/global.cmi pretyping/evd.cmi \ + kernel/environ.cmi library/declare.cmi kernel/declarations.cmi \ + kernel/conv_oracle.cmi interp/constrextern.cmi pretyping/classops.cmi \ + parsing/prettyp.cmi +parsing/prettyp.cmx: lib/util.cmx kernel/typeops.cmx pretyping/termops.cmx \ + kernel/term.cmx interp/syntax_def.cmx kernel/sign.cmx \ + kernel/safe_typing.cmx pretyping/reductionops.cmx kernel/reduction.cmx \ + pretyping/recordops.cmx parsing/printmod.cmx parsing/printer.cmx \ + lib/pp.cmx interp/notation.cmx library/nametab.cmx kernel/names.cmx \ + library/nameops.cmx library/libobject.cmx library/libnames.cmx \ + library/lib.cmx pretyping/inductiveops.cmx kernel/inductive.cmx \ + library/impargs.cmx library/global.cmx pretyping/evd.cmx \ + kernel/environ.cmx library/declare.cmx kernel/declarations.cmx \ + kernel/conv_oracle.cmx interp/constrextern.cmx pretyping/classops.cmx \ + parsing/prettyp.cmi parsing/printer.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ kernel/sign.cmi proofs/refiner.cmi proofs/proof_type.cmi \ parsing/ppconstr.cmi lib/pp.cmi proofs/pfedit.cmi lib/options.cmi \ @@ -1275,22 +1278,22 @@ parsing/q_util.cmo: toplevel/vernacexpr.cmo lib/util.cmi parsing/pcoq.cmi \ interp/genarg.cmi parsing/q_util.cmi parsing/q_util.cmx: toplevel/vernacexpr.cmx lib/util.cmx parsing/pcoq.cmx \ interp/genarg.cmx parsing/q_util.cmi -parsing/search.cmo: lib/util.cmi pretyping/typing.cmi pretyping/termops.cmi \ - kernel/term.cmi pretyping/rawterm.cmi parsing/printer.cmi lib/pp.cmi \ - pretyping/pattern.cmi library/nametab.cmi kernel/names.cmi \ - library/nameops.cmi pretyping/matching.cmi library/libobject.cmi \ - library/libnames.cmi pretyping/inductiveops.cmi library/global.cmi \ - pretyping/evd.cmi kernel/environ.cmi library/declaremods.cmi \ - library/declare.cmi kernel/declarations.cmi interp/coqlib.cmi \ - parsing/search.cmi -parsing/search.cmx: lib/util.cmx pretyping/typing.cmx pretyping/termops.cmx \ - kernel/term.cmx pretyping/rawterm.cmx parsing/printer.cmx lib/pp.cmx \ - pretyping/pattern.cmx library/nametab.cmx kernel/names.cmx \ - library/nameops.cmx pretyping/matching.cmx library/libobject.cmx \ - library/libnames.cmx pretyping/inductiveops.cmx library/global.cmx \ - pretyping/evd.cmx kernel/environ.cmx library/declaremods.cmx \ - library/declare.cmx kernel/declarations.cmx interp/coqlib.cmx \ - parsing/search.cmi +parsing/search.cmo: lib/util.cmi pretyping/typing.cmi kernel/typeops.cmi \ + pretyping/termops.cmi kernel/term.cmi pretyping/rawterm.cmi \ + parsing/printer.cmi lib/pp.cmi pretyping/pattern.cmi library/nametab.cmi \ + kernel/names.cmi library/nameops.cmi pretyping/matching.cmi \ + library/libobject.cmi library/libnames.cmi pretyping/inductiveops.cmi \ + library/global.cmi pretyping/evd.cmi kernel/environ.cmi \ + library/declaremods.cmi library/declare.cmi kernel/declarations.cmi \ + interp/coqlib.cmi parsing/search.cmi +parsing/search.cmx: lib/util.cmx pretyping/typing.cmx kernel/typeops.cmx \ + pretyping/termops.cmx kernel/term.cmx pretyping/rawterm.cmx \ + parsing/printer.cmx lib/pp.cmx pretyping/pattern.cmx library/nametab.cmx \ + kernel/names.cmx library/nameops.cmx pretyping/matching.cmx \ + library/libobject.cmx library/libnames.cmx pretyping/inductiveops.cmx \ + library/global.cmx pretyping/evd.cmx kernel/environ.cmx \ + library/declaremods.cmx library/declare.cmx kernel/declarations.cmx \ + interp/coqlib.cmx parsing/search.cmi parsing/tacextend.cmo: lib/util.cmi parsing/q_util.cmi parsing/q_coqast.cmo \ lib/pp_control.cmi lib/pp.cmi parsing/pcoq.cmi interp/genarg.cmi \ parsing/argextend.cmo @@ -1588,11 +1591,11 @@ pretyping/unification.cmx: lib/util.cmx pretyping/typing.cmx \ library/global.cmx pretyping/evd.cmx pretyping/evarutil.cmx \ kernel/environ.cmx pretyping/unification.cmi pretyping/vnorm.cmo: kernel/vm.cmi kernel/vconv.cmi lib/util.cmi \ - kernel/term.cmi kernel/reduction.cmi kernel/names.cmi \ + kernel/typeops.cmi kernel/term.cmi kernel/reduction.cmi kernel/names.cmi \ kernel/inductive.cmi kernel/environ.cmi kernel/declarations.cmi \ pretyping/vnorm.cmi pretyping/vnorm.cmx: kernel/vm.cmx kernel/vconv.cmx lib/util.cmx \ - kernel/term.cmx kernel/reduction.cmx kernel/names.cmx \ + kernel/typeops.cmx kernel/term.cmx kernel/reduction.cmx kernel/names.cmx \ kernel/inductive.cmx kernel/environ.cmx kernel/declarations.cmx \ pretyping/vnorm.cmi proofs/clenvtac.cmo: lib/util.cmi pretyping/unification.cmi \ @@ -1924,7 +1927,8 @@ tactics/equality.cmo: toplevel/vernacexpr.cmo lib/util.cmi kernel/univ.cmi \ pretyping/inductiveops.cmi kernel/inductive.cmi pretyping/indrec.cmi \ tactics/hipattern.cmi pretyping/evd.cmi pretyping/evarutil.cmi \ pretyping/evarconv.cmi proofs/evar_refiner.cmi kernel/environ.cmi \ - kernel/declarations.cmi interp/coqlib.cmi tactics/equality.cmi + kernel/declarations.cmi interp/coqlib.cmi pretyping/coercion.cmi \ + tactics/equality.cmi tactics/equality.cmx: toplevel/vernacexpr.cmx lib/util.cmx kernel/univ.cmx \ pretyping/typing.cmx kernel/typeops.cmx pretyping/termops.cmx \ kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \ @@ -1936,7 +1940,8 @@ tactics/equality.cmx: toplevel/vernacexpr.cmx lib/util.cmx kernel/univ.cmx \ pretyping/inductiveops.cmx kernel/inductive.cmx pretyping/indrec.cmx \ tactics/hipattern.cmx pretyping/evd.cmx pretyping/evarutil.cmx \ pretyping/evarconv.cmx proofs/evar_refiner.cmx kernel/environ.cmx \ - kernel/declarations.cmx interp/coqlib.cmx tactics/equality.cmi + kernel/declarations.cmx interp/coqlib.cmx pretyping/coercion.cmx \ + tactics/equality.cmi tactics/evar_tactics.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ tactics/tactics.cmi proofs/tacmach.cmi proofs/tacexpr.cmo kernel/sign.cmi \ proofs/refiner.cmi proofs/proof_type.cmi pretyping/evd.cmi \ @@ -2203,6 +2208,8 @@ tactics/termdn.cmx: lib/util.cmx kernel/term.cmx pretyping/rawterm.cmx \ pretyping/pattern.cmx library/nametab.cmx kernel/names.cmx \ library/nameops.cmx library/libnames.cmx tactics/dn.cmx \ tactics/termdn.cmi +test-suite/zarith.cmo: test-suite/zarith.cmi +test-suite/zarith.cmx: test-suite/zarith.cmi tools/coqdep.cmo: tools/coqdep_lexer.cmo config/coq_config.cmi tools/coqdep.cmx: tools/coqdep_lexer.cmx config/coq_config.cmx tools/gallina.cmo: tools/gallina_lexer.cmo @@ -2292,11 +2299,13 @@ toplevel/coqtop.cmx: kernel/vm.cmx toplevel/vernac.cmx kernel/vconv.cmx \ toplevel/coqinit.cmx config/coq_config.cmx interp/constrintern.cmx \ toplevel/cerrors.cmx toplevel/coqtop.cmi toplevel/discharge.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ - kernel/sign.cmi kernel/names.cmi kernel/inductive.cmi kernel/entries.cmi \ - kernel/declarations.cmi kernel/cooking.cmi toplevel/discharge.cmi + kernel/sign.cmi kernel/names.cmi kernel/inductive.cmi library/global.cmi \ + kernel/entries.cmi kernel/declarations.cmi kernel/cooking.cmi \ + toplevel/discharge.cmi toplevel/discharge.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ - kernel/sign.cmx kernel/names.cmx kernel/inductive.cmx kernel/entries.cmx \ - kernel/declarations.cmx kernel/cooking.cmx toplevel/discharge.cmi + kernel/sign.cmx kernel/names.cmx kernel/inductive.cmx library/global.cmx \ + kernel/entries.cmx kernel/declarations.cmx kernel/cooking.cmx \ + toplevel/discharge.cmi toplevel/fhimsg.cmo: lib/util.cmi kernel/type_errors.cmi kernel/term.cmi \ kernel/sign.cmi kernel/reduction.cmi lib/pp.cmi kernel/names.cmi \ parsing/g_minicoq.cmi kernel/environ.cmi toplevel/fhimsg.cmi @@ -2709,36 +2718,36 @@ contrib/extraction/common.cmx: lib/util.cmx kernel/term.cmx \ library/libnames.cmx kernel/inductive.cmx contrib/extraction/haskell.cmx \ lib/gset.cmx library/global.cmx contrib/extraction/extraction.cmx \ kernel/declarations.cmx contrib/extraction/common.cmi -contrib/extraction/extract_env.cmo: lib/util.cmi kernel/term.cmi \ - contrib/extraction/table.cmi kernel/reduction.cmi lib/pp.cmi \ - library/nametab.cmi kernel/names.cmi contrib/extraction/modutil.cmi \ - kernel/modops.cmi kernel/mod_subst.cmi contrib/extraction/miniml.cmi \ - library/library.cmi library/libobject.cmi library/libnames.cmi \ - library/lib.cmi library/global.cmi contrib/extraction/extraction.cmi \ - kernel/declarations.cmi contrib/extraction/common.cmi \ - contrib/extraction/extract_env.cmi -contrib/extraction/extract_env.cmx: lib/util.cmx kernel/term.cmx \ - contrib/extraction/table.cmx kernel/reduction.cmx lib/pp.cmx \ - library/nametab.cmx kernel/names.cmx contrib/extraction/modutil.cmx \ - kernel/modops.cmx kernel/mod_subst.cmx contrib/extraction/miniml.cmi \ - library/library.cmx library/libobject.cmx library/libnames.cmx \ - library/lib.cmx library/global.cmx contrib/extraction/extraction.cmx \ - kernel/declarations.cmx contrib/extraction/common.cmx \ - contrib/extraction/extract_env.cmi -contrib/extraction/extraction.cmo: lib/util.cmi pretyping/termops.cmi \ - kernel/term.cmi contrib/extraction/table.cmi library/summary.cmi \ - pretyping/retyping.cmi pretyping/reductionops.cmi kernel/reduction.cmi \ - pretyping/recordops.cmi library/nametab.cmi kernel/names.cmi \ - library/nameops.cmi contrib/extraction/mlutil.cmi \ +contrib/extraction/extract_env.cmo: lib/util.cmi kernel/typeops.cmi \ + kernel/term.cmi contrib/extraction/table.cmi kernel/reduction.cmi \ + lib/pp.cmi library/nametab.cmi kernel/names.cmi \ + contrib/extraction/modutil.cmi kernel/modops.cmi kernel/mod_subst.cmi \ + contrib/extraction/miniml.cmi library/library.cmi library/libobject.cmi \ + library/libnames.cmi library/lib.cmi library/global.cmi \ + contrib/extraction/extraction.cmi kernel/declarations.cmi \ + contrib/extraction/common.cmi contrib/extraction/extract_env.cmi +contrib/extraction/extract_env.cmx: lib/util.cmx kernel/typeops.cmx \ + kernel/term.cmx contrib/extraction/table.cmx kernel/reduction.cmx \ + lib/pp.cmx library/nametab.cmx kernel/names.cmx \ + contrib/extraction/modutil.cmx kernel/modops.cmx kernel/mod_subst.cmx \ + contrib/extraction/miniml.cmi library/library.cmx library/libobject.cmx \ + library/libnames.cmx library/lib.cmx library/global.cmx \ + contrib/extraction/extraction.cmx kernel/declarations.cmx \ + contrib/extraction/common.cmx contrib/extraction/extract_env.cmi +contrib/extraction/extraction.cmo: lib/util.cmi kernel/typeops.cmi \ + pretyping/termops.cmi kernel/term.cmi contrib/extraction/table.cmi \ + library/summary.cmi pretyping/retyping.cmi pretyping/reductionops.cmi \ + kernel/reduction.cmi pretyping/recordops.cmi library/nametab.cmi \ + kernel/names.cmi library/nameops.cmi contrib/extraction/mlutil.cmi \ contrib/extraction/miniml.cmi library/libnames.cmi \ pretyping/inductiveops.cmi kernel/inductive.cmi pretyping/evd.cmi \ kernel/environ.cmi kernel/declarations.cmi \ contrib/extraction/extraction.cmi -contrib/extraction/extraction.cmx: lib/util.cmx pretyping/termops.cmx \ - kernel/term.cmx contrib/extraction/table.cmx library/summary.cmx \ - pretyping/retyping.cmx pretyping/reductionops.cmx kernel/reduction.cmx \ - pretyping/recordops.cmx library/nametab.cmx kernel/names.cmx \ - library/nameops.cmx contrib/extraction/mlutil.cmx \ +contrib/extraction/extraction.cmx: lib/util.cmx kernel/typeops.cmx \ + pretyping/termops.cmx kernel/term.cmx contrib/extraction/table.cmx \ + library/summary.cmx pretyping/retyping.cmx pretyping/reductionops.cmx \ + kernel/reduction.cmx pretyping/recordops.cmx library/nametab.cmx \ + kernel/names.cmx library/nameops.cmx contrib/extraction/mlutil.cmx \ contrib/extraction/miniml.cmi library/libnames.cmx \ pretyping/inductiveops.cmx kernel/inductive.cmx pretyping/evd.cmx \ kernel/environ.cmx kernel/declarations.cmx \ @@ -2803,13 +2812,13 @@ contrib/extraction/scheme.cmx: lib/util.cmx contrib/extraction/table.cmx \ library/nameops.cmx contrib/extraction/mlutil.cmx \ contrib/extraction/miniml.cmi library/libnames.cmx \ contrib/extraction/scheme.cmi -contrib/extraction/table.cmo: lib/util.cmi kernel/term.cmi \ +contrib/extraction/table.cmo: lib/util.cmi kernel/typeops.cmi kernel/term.cmi \ library/summary.cmi kernel/reduction.cmi parsing/printer.cmi lib/pp.cmi \ lib/options.cmi library/nametab.cmi kernel/names.cmi library/nameops.cmi \ contrib/extraction/miniml.cmi library/libobject.cmi library/libnames.cmi \ library/lib.cmi library/goptions.cmi library/global.cmi \ kernel/environ.cmi kernel/declarations.cmi contrib/extraction/table.cmi -contrib/extraction/table.cmx: lib/util.cmx kernel/term.cmx \ +contrib/extraction/table.cmx: lib/util.cmx kernel/typeops.cmx kernel/term.cmx \ library/summary.cmx kernel/reduction.cmx parsing/printer.cmx lib/pp.cmx \ lib/options.cmx library/nametab.cmx kernel/names.cmx library/nameops.cmx \ contrib/extraction/miniml.cmi library/libobject.cmx library/libnames.cmx \ @@ -2950,10 +2959,10 @@ contrib/fourier/g_fourier.cmx: lib/util.cmx tactics/tacinterp.cmx \ parsing/pcoq.cmx contrib/fourier/fourierR.cmx parsing/egrammar.cmx \ toplevel/cerrors.cmx contrib/funind/functional_principles_proofs.cmo: lib/util.cmi \ - pretyping/typing.cmi pretyping/termops.cmi kernel/term.cmi \ - tactics/tactics.cmi tactics/tacticals.cmi pretyping/tacred.cmi \ - proofs/tacmach.cmi tactics/tacinterp.cmi kernel/sign.cmi \ - pretyping/reductionops.cmi contrib/recdef/recdef.cmo \ + pretyping/typing.cmi kernel/typeops.cmi pretyping/termops.cmi \ + kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ + pretyping/tacred.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \ + kernel/sign.cmi pretyping/reductionops.cmi contrib/recdef/recdef.cmo \ pretyping/rawterm.cmi proofs/proof_type.cmi parsing/printer.cmi \ lib/pp.cmi proofs/pfedit.cmi lib/options.cmi library/nametab.cmi \ kernel/names.cmi library/nameops.cmi library/libnames.cmi \ @@ -2964,10 +2973,10 @@ contrib/funind/functional_principles_proofs.cmo: lib/util.cmi \ toplevel/command.cmi kernel/closure.cmi toplevel/cerrors.cmi \ contrib/funind/functional_principles_proofs.cmi contrib/funind/functional_principles_proofs.cmx: lib/util.cmx \ - pretyping/typing.cmx pretyping/termops.cmx kernel/term.cmx \ - tactics/tactics.cmx tactics/tacticals.cmx pretyping/tacred.cmx \ - proofs/tacmach.cmx tactics/tacinterp.cmx kernel/sign.cmx \ - pretyping/reductionops.cmx contrib/recdef/recdef.cmx \ + pretyping/typing.cmx kernel/typeops.cmx pretyping/termops.cmx \ + kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \ + pretyping/tacred.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \ + kernel/sign.cmx pretyping/reductionops.cmx contrib/recdef/recdef.cmx \ pretyping/rawterm.cmx proofs/proof_type.cmx parsing/printer.cmx \ lib/pp.cmx proofs/pfedit.cmx lib/options.cmx library/nametab.cmx \ kernel/names.cmx library/nameops.cmx library/libnames.cmx \ @@ -3052,10 +3061,10 @@ contrib/funind/indfun_main.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ parsing/egrammar.cmx interp/coqlib.cmx interp/constrintern.cmx \ toplevel/cerrors.cmx contrib/funind/indfun.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ - interp/topconstr.cmi pretyping/termops.cmi kernel/term.cmi \ - tactics/tactics.cmi tactics/tacticals.cmi proofs/tacmach.cmi \ - tactics/tacinterp.cmi proofs/tacexpr.cmo library/states.cmi \ - kernel/sign.cmi contrib/recdef/recdef.cmo \ + kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \ + kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ + proofs/tacmach.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \ + library/states.cmi kernel/sign.cmi contrib/recdef/recdef.cmo \ contrib/funind/rawterm_to_relation.cmi pretyping/rawterm.cmi \ parsing/printer.cmi parsing/ppconstr.cmi lib/pp.cmi lib/options.cmi \ interp/notation.cmi kernel/names.cmi library/nameops.cmi \ @@ -3068,10 +3077,10 @@ contrib/funind/indfun.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ library/decl_kinds.cmo interp/constrintern.cmi interp/constrextern.cmi \ toplevel/command.cmi toplevel/cerrors.cmi contrib/funind/indfun.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ - interp/topconstr.cmx pretyping/termops.cmx kernel/term.cmx \ - tactics/tactics.cmx tactics/tacticals.cmx proofs/tacmach.cmx \ - tactics/tacinterp.cmx proofs/tacexpr.cmx library/states.cmx \ - kernel/sign.cmx contrib/recdef/recdef.cmx \ + kernel/typeops.cmx interp/topconstr.cmx pretyping/termops.cmx \ + kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \ + proofs/tacmach.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \ + library/states.cmx kernel/sign.cmx contrib/recdef/recdef.cmx \ contrib/funind/rawterm_to_relation.cmx pretyping/rawterm.cmx \ parsing/printer.cmx parsing/ppconstr.cmx lib/pp.cmx lib/options.cmx \ interp/notation.cmx kernel/names.cmx library/nameops.cmx \ @@ -3115,16 +3124,18 @@ contrib/funind/merge.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ interp/topconstr.cmi kernel/term.cmi tactics/tacinterp.cmi \ contrib/funind/rawtermops.cmi pretyping/rawterm.cmi parsing/printer.cmi \ pretyping/pretyping.cmi lib/pp.cmi lib/options.cmi kernel/names.cmi \ - pretyping/inductiveops.cmi kernel/inductive.cmi library/global.cmi \ - pretyping/evd.cmi kernel/environ.cmi pretyping/detyping.cmi \ - kernel/declarations.cmi interp/constrextern.cmi toplevel/command.cmi + library/nameops.cmi library/libnames.cmi pretyping/inductiveops.cmi \ + kernel/inductive.cmi library/global.cmi pretyping/evd.cmi \ + kernel/environ.cmi pretyping/detyping.cmi kernel/declarations.cmi \ + interp/constrintern.cmi interp/constrextern.cmi toplevel/command.cmi contrib/funind/merge.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ interp/topconstr.cmx kernel/term.cmx tactics/tacinterp.cmx \ contrib/funind/rawtermops.cmx pretyping/rawterm.cmx parsing/printer.cmx \ pretyping/pretyping.cmx lib/pp.cmx lib/options.cmx kernel/names.cmx \ - pretyping/inductiveops.cmx kernel/inductive.cmx library/global.cmx \ - pretyping/evd.cmx kernel/environ.cmx pretyping/detyping.cmx \ - kernel/declarations.cmx interp/constrextern.cmx toplevel/command.cmx + library/nameops.cmx library/libnames.cmx pretyping/inductiveops.cmx \ + kernel/inductive.cmx library/global.cmx pretyping/evd.cmx \ + kernel/environ.cmx pretyping/detyping.cmx kernel/declarations.cmx \ + interp/constrintern.cmx interp/constrextern.cmx toplevel/command.cmx contrib/funind/rawtermops.cmo: lib/util.cmi pretyping/rawterm.cmi lib/pp.cmi \ kernel/names.cmi library/nameops.cmi library/libnames.cmi \ pretyping/inductiveops.cmi contrib/funind/indfun_common.cmi \ @@ -3197,42 +3208,42 @@ contrib/funind/tacinvutils.cmx: lib/util.cmx pretyping/termops.cmx \ contrib/funind/tacinvutils.cmi contrib/interface/blast.cmo: toplevel/vernacinterp.cmi \ toplevel/vernacentries.cmi lib/util.cmi pretyping/typing.cmi \ - pretyping/termops.cmi kernel/term.cmi tactics/tactics.cmi \ - tactics/tacticals.cmi parsing/tactic_printer.cmi pretyping/tacred.cmi \ - proofs/tacmach.cmi tactics/tacinterp.cmi kernel/sign.cmi \ - proofs/refiner.cmi kernel/reduction.cmi pretyping/rawterm.cmi \ - proofs/proof_type.cmi proofs/proof_trees.cmi parsing/printer.cmi \ - parsing/pptactic.cmi lib/pp.cmi proofs/pfedit.cmi parsing/pcoq.cmi \ - contrib/interface/pbp.cmi pretyping/pattern.cmi kernel/names.cmi \ - library/nameops.cmi proofs/logic.cmi kernel/inductive.cmi \ - tactics/hipattern.cmi library/global.cmi lib/explore.cmi \ - pretyping/evd.cmi tactics/equality.cmi kernel/environ.cmi \ + kernel/typeops.cmi pretyping/termops.cmi kernel/term.cmi \ + tactics/tactics.cmi tactics/tacticals.cmi parsing/tactic_printer.cmi \ + pretyping/tacred.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \ + kernel/sign.cmi proofs/refiner.cmi kernel/reduction.cmi \ + pretyping/rawterm.cmi proofs/proof_type.cmi proofs/proof_trees.cmi \ + parsing/printer.cmi parsing/pptactic.cmi lib/pp.cmi proofs/pfedit.cmi \ + parsing/pcoq.cmi contrib/interface/pbp.cmi pretyping/pattern.cmi \ + kernel/names.cmi library/nameops.cmi proofs/logic.cmi \ + kernel/inductive.cmi tactics/hipattern.cmi library/global.cmi \ + lib/explore.cmi pretyping/evd.cmi tactics/equality.cmi kernel/environ.cmi \ tactics/eauto.cmi library/declare.cmi kernel/declarations.cmi \ toplevel/command.cmi pretyping/clenv.cmi tactics/auto.cmi \ contrib/interface/blast.cmi contrib/interface/blast.cmx: toplevel/vernacinterp.cmx \ toplevel/vernacentries.cmx lib/util.cmx pretyping/typing.cmx \ - pretyping/termops.cmx kernel/term.cmx tactics/tactics.cmx \ - tactics/tacticals.cmx parsing/tactic_printer.cmx pretyping/tacred.cmx \ - proofs/tacmach.cmx tactics/tacinterp.cmx kernel/sign.cmx \ - proofs/refiner.cmx kernel/reduction.cmx pretyping/rawterm.cmx \ - proofs/proof_type.cmx proofs/proof_trees.cmx parsing/printer.cmx \ - parsing/pptactic.cmx lib/pp.cmx proofs/pfedit.cmx parsing/pcoq.cmx \ - contrib/interface/pbp.cmx pretyping/pattern.cmx kernel/names.cmx \ - library/nameops.cmx proofs/logic.cmx kernel/inductive.cmx \ - tactics/hipattern.cmx library/global.cmx lib/explore.cmx \ - pretyping/evd.cmx tactics/equality.cmx kernel/environ.cmx \ + kernel/typeops.cmx pretyping/termops.cmx kernel/term.cmx \ + tactics/tactics.cmx tactics/tacticals.cmx parsing/tactic_printer.cmx \ + pretyping/tacred.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \ + kernel/sign.cmx proofs/refiner.cmx kernel/reduction.cmx \ + pretyping/rawterm.cmx proofs/proof_type.cmx proofs/proof_trees.cmx \ + parsing/printer.cmx parsing/pptactic.cmx lib/pp.cmx proofs/pfedit.cmx \ + parsing/pcoq.cmx contrib/interface/pbp.cmx pretyping/pattern.cmx \ + kernel/names.cmx library/nameops.cmx proofs/logic.cmx \ + kernel/inductive.cmx tactics/hipattern.cmx library/global.cmx \ + lib/explore.cmx pretyping/evd.cmx tactics/equality.cmx kernel/environ.cmx \ tactics/eauto.cmx library/declare.cmx kernel/declarations.cmx \ toplevel/command.cmx pretyping/clenv.cmx tactics/auto.cmx \ contrib/interface/blast.cmi contrib/interface/centaur.cmo: contrib/interface/xlate.cmi \ contrib/interface/vtp.cmi toplevel/vernacinterp.cmi \ toplevel/vernacexpr.cmo toplevel/vernacentries.cmi toplevel/vernac.cmi \ - lib/util.cmi contrib/interface/translate.cmi kernel/term.cmi \ - proofs/tacmach.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \ - contrib/interface/showproof_ct.cmo contrib/interface/showproof.cmi \ - parsing/search.cmi proofs/refiner.cmi kernel/reduction.cmi \ - pretyping/rawterm.cmi toplevel/protectedtoplevel.cmi \ + lib/util.cmi kernel/typeops.cmi contrib/interface/translate.cmi \ + kernel/term.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \ + proofs/tacexpr.cmo contrib/interface/showproof_ct.cmo \ + contrib/interface/showproof.cmi parsing/search.cmi proofs/refiner.cmi \ + kernel/reduction.cmi pretyping/rawterm.cmi toplevel/protectedtoplevel.cmi \ proofs/proof_type.cmi proofs/proof_trees.cmi parsing/printer.cmi \ pretyping/pretyping.cmi parsing/pptactic.cmi lib/pp.cmi proofs/pfedit.cmi \ parsing/pcoq.cmi contrib/interface/pbp.cmi library/nametab.cmi \ @@ -3248,11 +3259,11 @@ contrib/interface/centaur.cmo: contrib/interface/xlate.cmi \ contrib/interface/centaur.cmx: contrib/interface/xlate.cmx \ contrib/interface/vtp.cmx toplevel/vernacinterp.cmx \ toplevel/vernacexpr.cmx toplevel/vernacentries.cmx toplevel/vernac.cmx \ - lib/util.cmx contrib/interface/translate.cmx kernel/term.cmx \ - proofs/tacmach.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \ - contrib/interface/showproof_ct.cmx contrib/interface/showproof.cmx \ - parsing/search.cmx proofs/refiner.cmx kernel/reduction.cmx \ - pretyping/rawterm.cmx toplevel/protectedtoplevel.cmx \ + lib/util.cmx kernel/typeops.cmx contrib/interface/translate.cmx \ + kernel/term.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \ + proofs/tacexpr.cmx contrib/interface/showproof_ct.cmx \ + contrib/interface/showproof.cmx parsing/search.cmx proofs/refiner.cmx \ + kernel/reduction.cmx pretyping/rawterm.cmx toplevel/protectedtoplevel.cmx \ proofs/proof_type.cmx proofs/proof_trees.cmx parsing/printer.cmx \ pretyping/pretyping.cmx parsing/pptactic.cmx lib/pp.cmx proofs/pfedit.cmx \ parsing/pcoq.cmx contrib/interface/pbp.cmx library/nametab.cmx \ @@ -3302,21 +3313,23 @@ 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: toplevel/vernacexpr.cmo lib/util.cmi \ - interp/topconstr.cmi kernel/term.cmi kernel/sign.cmi kernel/reduction.cmi \ - parsing/prettyp.cmi lib/pp.cmi library/nametab.cmi kernel/names.cmi \ - library/nameops.cmi library/libobject.cmi library/libnames.cmi \ - library/lib.cmi kernel/inductive.cmi library/impargs.cmi \ - library/global.cmi kernel/environ.cmi library/declare.cmi \ - kernel/declarations.cmi library/decl_kinds.cmo interp/constrextern.cmi \ - pretyping/classops.cmi contrib/interface/name_to_ast.cmi + kernel/typeops.cmi interp/topconstr.cmi kernel/term.cmi kernel/sign.cmi \ + kernel/reduction.cmi parsing/prettyp.cmi lib/pp.cmi library/nametab.cmi \ + kernel/names.cmi library/nameops.cmi library/libobject.cmi \ + library/libnames.cmi library/lib.cmi kernel/inductive.cmi \ + library/impargs.cmi library/global.cmi kernel/environ.cmi \ + library/declare.cmi kernel/declarations.cmi library/decl_kinds.cmo \ + interp/constrextern.cmi pretyping/classops.cmi \ + contrib/interface/name_to_ast.cmi contrib/interface/name_to_ast.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ - interp/topconstr.cmx kernel/term.cmx kernel/sign.cmx kernel/reduction.cmx \ - parsing/prettyp.cmx lib/pp.cmx library/nametab.cmx kernel/names.cmx \ - library/nameops.cmx library/libobject.cmx library/libnames.cmx \ - library/lib.cmx kernel/inductive.cmx library/impargs.cmx \ - library/global.cmx kernel/environ.cmx library/declare.cmx \ - kernel/declarations.cmx library/decl_kinds.cmx interp/constrextern.cmx \ - pretyping/classops.cmx contrib/interface/name_to_ast.cmi + kernel/typeops.cmx interp/topconstr.cmx kernel/term.cmx kernel/sign.cmx \ + kernel/reduction.cmx parsing/prettyp.cmx lib/pp.cmx library/nametab.cmx \ + kernel/names.cmx library/nameops.cmx library/libobject.cmx \ + library/libnames.cmx library/lib.cmx kernel/inductive.cmx \ + library/impargs.cmx library/global.cmx kernel/environ.cmx \ + library/declare.cmx kernel/declarations.cmx library/decl_kinds.cmx \ + interp/constrextern.cmx pretyping/classops.cmx \ + contrib/interface/name_to_ast.cmi contrib/interface/parse.cmo: contrib/interface/xlate.cmi \ contrib/interface/vtp.cmi toplevel/vernacexpr.cmo \ toplevel/vernacentries.cmi lib/util.cmi lib/system.cmi lib/pp.cmi \ @@ -3362,7 +3375,7 @@ contrib/interface/showproof_ct.cmx: contrib/interface/xlate.cmx \ parsing/printer.cmx lib/pp.cmx toplevel/metasyntax.cmx library/global.cmx \ contrib/interface/ascent.cmi contrib/interface/showproof.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ - pretyping/typing.cmi contrib/interface/translate.cmi \ + pretyping/typing.cmi kernel/typeops.cmi contrib/interface/translate.cmi \ pretyping/termops.cmi kernel/term.cmi proofs/tacmach.cmi \ proofs/tacexpr.cmo kernel/sign.cmi contrib/interface/showproof_ct.cmo \ pretyping/reductionops.cmi pretyping/rawterm.cmi proofs/proof_type.cmi \ @@ -3373,7 +3386,7 @@ contrib/interface/showproof.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ kernel/declarations.cmi interp/constrintern.cmi pretyping/clenv.cmi \ contrib/interface/showproof.cmi contrib/interface/showproof.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ - pretyping/typing.cmx contrib/interface/translate.cmx \ + pretyping/typing.cmx kernel/typeops.cmx contrib/interface/translate.cmx \ pretyping/termops.cmx kernel/term.cmx proofs/tacmach.cmx \ proofs/tacexpr.cmx kernel/sign.cmx contrib/interface/showproof_ct.cmx \ pretyping/reductionops.cmx pretyping/rawterm.cmx proofs/proof_type.cmx \ @@ -3487,13 +3500,13 @@ contrib/omega/omega.cmo: lib/util.cmi kernel/names.cmi contrib/omega/omega.cmx: lib/util.cmx kernel/names.cmx contrib/recdef/recdef.cmo: toplevel/vernacinterp.cmi \ toplevel/vernacentries.cmi lib/util.cmi pretyping/typing.cmi \ - interp/topconstr.cmi pretyping/termops.cmi kernel/term.cmi \ - tactics/tactics.cmi tactics/tacticals.cmi proofs/tactic_debug.cmi \ - pretyping/tacred.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \ - kernel/safe_typing.cmi pretyping/rawterm.cmi proofs/proof_type.cmi \ - parsing/printer.cmi pretyping/pretyping.cmi parsing/ppconstr.cmi \ - lib/pp.cmi proofs/pfedit.cmi parsing/pcoq.cmi lib/options.cmi \ - library/nametab.cmi kernel/names.cmi library/nameops.cmi \ + kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \ + kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ + proofs/tactic_debug.cmi pretyping/tacred.cmi proofs/tacmach.cmi \ + tactics/tacinterp.cmi kernel/safe_typing.cmi pretyping/rawterm.cmi \ + proofs/proof_type.cmi parsing/printer.cmi pretyping/pretyping.cmi \ + parsing/ppconstr.cmi lib/pp.cmi proofs/pfedit.cmi parsing/pcoq.cmi \ + lib/options.cmi library/nametab.cmi kernel/names.cmi library/nameops.cmi \ library/libnames.cmi library/lib.cmi tactics/hiddentac.cmi \ library/global.cmi interp/genarg.cmi pretyping/evd.cmi \ tactics/equality.cmi kernel/environ.cmi kernel/entries.cmi \ @@ -3503,13 +3516,13 @@ contrib/recdef/recdef.cmo: toplevel/vernacinterp.cmi \ kernel/closure.cmi toplevel/cerrors.cmi tactics/auto.cmi contrib/recdef/recdef.cmx: toplevel/vernacinterp.cmx \ toplevel/vernacentries.cmx lib/util.cmx pretyping/typing.cmx \ - interp/topconstr.cmx pretyping/termops.cmx kernel/term.cmx \ - tactics/tactics.cmx tactics/tacticals.cmx proofs/tactic_debug.cmx \ - pretyping/tacred.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \ - kernel/safe_typing.cmx pretyping/rawterm.cmx proofs/proof_type.cmx \ - parsing/printer.cmx pretyping/pretyping.cmx parsing/ppconstr.cmx \ - lib/pp.cmx proofs/pfedit.cmx parsing/pcoq.cmx lib/options.cmx \ - library/nametab.cmx kernel/names.cmx library/nameops.cmx \ + kernel/typeops.cmx interp/topconstr.cmx pretyping/termops.cmx \ + kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \ + proofs/tactic_debug.cmx pretyping/tacred.cmx proofs/tacmach.cmx \ + tactics/tacinterp.cmx kernel/safe_typing.cmx pretyping/rawterm.cmx \ + proofs/proof_type.cmx parsing/printer.cmx pretyping/pretyping.cmx \ + parsing/ppconstr.cmx lib/pp.cmx proofs/pfedit.cmx parsing/pcoq.cmx \ + lib/options.cmx library/nametab.cmx kernel/names.cmx library/nameops.cmx \ library/libnames.cmx library/lib.cmx tactics/hiddentac.cmx \ library/global.cmx interp/genarg.cmx pretyping/evd.cmx \ tactics/equality.cmx kernel/environ.cmx kernel/entries.cmx \ @@ -3890,7 +3903,7 @@ contrib/xml/acic2Xml.cmx: contrib/xml/xml.cmx lib/util.cmx kernel/term.cmx \ contrib/xml/acic.cmo: kernel/term.cmi kernel/names.cmi contrib/xml/acic.cmx: kernel/term.cmx kernel/names.cmx contrib/xml/cic2acic.cmo: lib/util.cmi contrib/xml/unshare.cmi \ - kernel/univ.cmi pretyping/termops.cmi kernel/term.cmi \ + kernel/univ.cmi kernel/typeops.cmi pretyping/termops.cmi kernel/term.cmi \ pretyping/reductionops.cmi parsing/printer.cmi lib/pp.cmi \ library/nametab.cmi kernel/names.cmi library/nameops.cmi \ library/library.cmi library/libnames.cmi library/lib.cmi \ @@ -3899,7 +3912,7 @@ contrib/xml/cic2acic.cmo: lib/util.cmi contrib/xml/unshare.cmi \ library/dischargedhypsmap.cmi library/declare.cmi kernel/declarations.cmi \ contrib/xml/acic.cmo contrib/xml/cic2acic.cmx: lib/util.cmx contrib/xml/unshare.cmx \ - kernel/univ.cmx pretyping/termops.cmx kernel/term.cmx \ + kernel/univ.cmx kernel/typeops.cmx pretyping/termops.cmx kernel/term.cmx \ pretyping/reductionops.cmx parsing/printer.cmx lib/pp.cmx \ library/nametab.cmx kernel/names.cmx library/nameops.cmx \ library/library.cmx library/libnames.cmx library/lib.cmx \ @@ -3954,8 +3967,8 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/xml.cmx lib/util.cmx \ contrib/xml/unshare.cmo: contrib/xml/unshare.cmi contrib/xml/unshare.cmx: contrib/xml/unshare.cmi contrib/xml/xmlcommand.cmo: contrib/xml/xml.cmi toplevel/vernac.cmi \ - lib/util.cmi contrib/xml/unshare.cmi kernel/term.cmi proofs/tacmach.cmi \ - pretyping/recordops.cmi proofs/proof_trees.cmi \ + lib/util.cmi contrib/xml/unshare.cmi kernel/typeops.cmi kernel/term.cmi \ + proofs/tacmach.cmi pretyping/recordops.cmi proofs/proof_trees.cmi \ contrib/xml/proof2aproof.cmo proofs/pfedit.cmi library/nametab.cmi \ kernel/names.cmi library/library.cmi library/libobject.cmi \ library/libnames.cmi library/lib.cmi parsing/lexer.cmi \ @@ -3965,8 +3978,8 @@ contrib/xml/xmlcommand.cmo: contrib/xml/xml.cmi toplevel/vernac.cmi \ config/coq_config.cmi contrib/xml/cic2acic.cmo contrib/xml/acic2Xml.cmo \ contrib/xml/acic.cmo contrib/xml/xmlcommand.cmi contrib/xml/xmlcommand.cmx: contrib/xml/xml.cmx toplevel/vernac.cmx \ - lib/util.cmx contrib/xml/unshare.cmx kernel/term.cmx proofs/tacmach.cmx \ - pretyping/recordops.cmx proofs/proof_trees.cmx \ + lib/util.cmx contrib/xml/unshare.cmx kernel/typeops.cmx kernel/term.cmx \ + proofs/tacmach.cmx pretyping/recordops.cmx proofs/proof_trees.cmx \ contrib/xml/proof2aproof.cmx proofs/pfedit.cmx library/nametab.cmx \ kernel/names.cmx library/library.cmx library/libobject.cmx \ library/libnames.cmx library/lib.cmx parsing/lexer.cmx \ @@ -3985,6 +3998,10 @@ contrib/xml/xmlentries.cmx: contrib/xml/xmlcommand.cmx \ parsing/egrammar.cmx toplevel/cerrors.cmx contrib/xml/xml.cmo: contrib/xml/xml.cmi contrib/xml/xml.cmx: contrib/xml/xml.cmi +doc/refman/euclid.cmo: doc/refman/euclid.cmi +doc/refman/euclid.cmx: doc/refman/euclid.cmi +doc/refman/heapsort.cmo: doc/refman/heapsort.cmi +doc/refman/heapsort.cmx: doc/refman/heapsort.cmi ide/utils/config_file.cmo: ide/utils/config_file.cmi ide/utils/config_file.cmx: ide/utils/config_file.cmi ide/utils/configwin_html_config.cmo: ide/utils/configwin_types.cmo \ @@ -4138,74 +4155,74 @@ tools/coq_makefile.cmx: tools/coq-tex.cmo: tools/coq-tex.cmx: coq_fix_code.o: kernel/byterun/coq_fix_code.c \ - /usr/lib/ocaml/3.09.2/caml/config.h \ - /usr/lib/ocaml/3.09.2/caml/compatibility.h \ - /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/config.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \ - /usr/lib/ocaml/3.09.2/caml/fail.h /usr/lib/ocaml/3.09.2/caml/mlvalues.h \ - /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_instruct.h \ + /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \ kernel/byterun/coq_fix_code.h coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h \ - /usr/lib/ocaml/3.09.2/caml/compatibility.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \ - /usr/lib/ocaml/3.09.2/caml/alloc.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \ - /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h \ - kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ + kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + kernel/byterun/coq_jumptbl.h coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h \ - /usr/lib/ocaml/3.09.2/caml/compatibility.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \ - /usr/lib/ocaml/3.09.2/caml/alloc.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \ - /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ + kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/memory.h coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h \ - /usr/lib/ocaml/3.09.2/caml/compatibility.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \ + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \ - /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_values.h \ - /usr/lib/ocaml/3.09.2/caml/alloc.h + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/fail.h \ + /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + /usr/local/lib/ocaml/caml/alloc.h coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \ - /usr/lib/ocaml/3.09.2/caml/config.h \ - /usr/lib/ocaml/3.09.2/caml/compatibility.h \ - /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/config.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \ - /usr/lib/ocaml/3.09.2/caml/fail.h /usr/lib/ocaml/3.09.2/caml/mlvalues.h \ - /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_instruct.h \ + /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_instruct.h \ kernel/byterun/coq_fix_code.h coq_interp.d.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h \ - /usr/lib/ocaml/3.09.2/caml/compatibility.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \ - /usr/lib/ocaml/3.09.2/caml/alloc.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \ - /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h \ - kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ + kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + kernel/byterun/coq_jumptbl.h coq_memory.d.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h \ - /usr/lib/ocaml/3.09.2/caml/compatibility.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \ - /usr/lib/ocaml/3.09.2/caml/alloc.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h kernel/byterun/coq_instruct.h \ - kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \ - /usr/lib/ocaml/3.09.2/caml/misc.h /usr/lib/ocaml/3.09.2/caml/memory.h + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/alloc.h /usr/local/lib/ocaml/caml/mlvalues.h \ + kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \ + kernel/byterun/coq_memory.h /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/memory.h coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h \ - /usr/lib/ocaml/3.09.2/caml/compatibility.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/misc.h \ + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ - /usr/lib/ocaml/3.09.2/caml/config.h /usr/lib/ocaml/3.09.2/caml/fail.h \ - /usr/lib/ocaml/3.09.2/caml/mlvalues.h /usr/lib/ocaml/3.09.2/caml/misc.h \ - /usr/lib/ocaml/3.09.2/caml/memory.h kernel/byterun/coq_values.h \ - /usr/lib/ocaml/3.09.2/caml/alloc.h + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/fail.h \ + /usr/local/lib/ocaml/caml/mlvalues.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/memory.h kernel/byterun/coq_values.h \ + /usr/local/lib/ocaml/caml/alloc.h diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 04a23919b..549e5e4fd 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -74,7 +74,8 @@ let visit_ref v r = exception Impossible let check_arity env cb = - if Reduction.is_arity env cb.const_type then raise Impossible + let t = Typeops.type_of_constant_type env cb.const_type in + if Reduction.is_arity env t then raise Impossible let check_fix env cb i = match cb.const_body with diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 857d3400a..f725c2259 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -225,7 +225,7 @@ let rec extract_type env db j c args = | Const kn -> let r = ConstRef kn in let cb = lookup_constant kn env in - let typ = cb.const_type in + let typ = Typeops.type_of_constant_type env cb.const_type in (match flag_of_type env typ with | (Info, TypeScheme) -> let mlt = extract_type_app env db (r, type_sign env typ) args in @@ -321,7 +321,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) Array.map (fun mip -> let b = snd (mind_arity mip) <> InProp in - let ar = Inductive.type_of_inductive (mib,mip) in + let ar = Inductive.type_of_inductive env (mib,mip) in let s,v = if b then type_sign_vl env ar else [],[] in let t = Array.make (Array.length mip.mind_nf_lc) [] in { ip_typename = mip.mind_typename; @@ -401,7 +401,8 @@ and extract_ind env kn = (* kn is supposed to be in long form *) (* Is this record officially declared with its projections ? *) (* If so, we use this information. *) begin try - let n = nb_default_params env (Inductive.type_of_inductive(mib,mip0)) + let n = nb_default_params env + (Inductive.type_of_inductive env (mib,mip0)) in List.iter (option_iter @@ -446,7 +447,7 @@ and mlt_env env r = match r with | _ -> None with Not_found -> let cb = Environ.lookup_constant kn env in - let typ = cb.const_type in + let typ = Typeops.type_of_constant_type env cb.const_type in match cb.const_body with | None -> None | Some l_body -> @@ -473,7 +474,7 @@ let record_constant_type env kn opt_typ = lookup_type kn with Not_found -> let typ = match opt_typ with - | None -> constant_type env kn + | None -> Typeops.type_of_constant env kn | Some typ -> typ in let mlt = extract_type env [] 1 typ [] in let schema = (type_maxvar mlt, mlt) @@ -814,7 +815,7 @@ let extract_fixpoint env vkn (fi,ti,ci) = let extract_constant env kn cb = let r = ConstRef kn in - let typ = cb.const_type in + let typ = Typeops.type_of_constant_type env cb.const_type in match cb.const_body with | None -> (* A logical axiom is risky, an informative one is fatal. *) (match flag_of_type env typ with @@ -846,7 +847,7 @@ let extract_constant env kn cb = let extract_constant_spec env kn cb = let r = ConstRef kn in - let typ = cb.const_type in + let typ = Typeops.type_of_constant_type env cb.const_type in match flag_of_type env typ with | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype)) | (Logic, Default) -> Sval (r, Tdummy Kother) @@ -884,7 +885,7 @@ let extract_declaration env r = match r with type kind = Logical | Term | Type let constant_kind env cb = - match flag_of_type env cb.const_type with + match flag_of_type env (Typeops.type_of_constant_type env cb.const_type) with | (Logic,_) -> Logical | (Info,TypeScheme) -> Type | (Info,Default) -> Term diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index 596f3ccb0..47a0977a5 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -441,7 +441,7 @@ let extract_constant_inline inline r ids s = match g with | ConstRef kn -> let env = Global.env () in - let typ = Environ.constant_type env kn in + let typ = Typeops.type_of_constant env kn in let typ = Reduction.whd_betadeltaiota env typ in if Reduction.is_arity env typ then begin diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index ab411cf11..14e2233fe 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -890,7 +890,8 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = (* observe (str "f_body_with_params_and_other_fun " ++ pr_lconstr f_body_with_params_and_other_fun); *) let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in (* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *) - let type_ctxt,type_of_f = Sign.decompose_prod_n_assum (nb_params + nb_args) f_def.const_type in + let type_ctxt,type_of_f = Sign.decompose_prod_n_assum (nb_params + nb_args) + (Typeops.type_of_constant_type (Global.env()) f_def.const_type) in let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in let lemma_type = it_mkProd_or_LetIn ~init:eqn type_ctxt in let f_id = id_of_label (con_label (destConst f)) in diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index c7f100c36..82bb28695 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -306,8 +306,7 @@ let generate_principle list_map_i (fun i x -> let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in - let princ_type = - (Global.lookup_constant princ).Declarations.const_type + let princ_type = Typeops.type_of_constant (Global.env()) princ in Functional_principles_types.generate_functional_principle interactive_proof @@ -682,7 +681,8 @@ let make_graph (f_ref:global_reference) = with_full_print (fun () -> (Constrextern.extern_constr false env body, - Constrextern.extern_type false env c_body.const_type + Constrextern.extern_type false env + (Typeops.type_of_constant_type env c_body.const_type) ) ) () diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index 40c90f5a1..04110ea98 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -101,7 +101,7 @@ let id_to_constr id = let generate_type g_to_f f graph i = (*i we deduce the number of arguments of the function and its returned type from the graph i*) - let graph_arity = Inductive.type_of_inductive (Global.lookup_inductive (destInd graph)) in + let graph_arity = Inductive.type_of_inductive (Global.env()) (Global.lookup_inductive (destInd graph)) in let ctxt,_ = decompose_prod_assum graph_arity in let fun_ctxt,res_type = match ctxt with diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 9e4500686..dc27cf983 100644 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -92,7 +92,7 @@ let rec def_const_in_term_rec vl x = | Case(_,x,t,a) -> def_const_in_term_rec vl x | Cast(x,_,t)-> def_const_in_term_rec vl t - | Const(c) -> def_const_in_term_rec vl (lookup_constant c vl).const_type + | Const(c) -> def_const_in_term_rec vl (Typeops.type_of_constant vl c) | _ -> def_const_in_term_rec vl (type_of vl Evd.empty x) ;; let def_const_in_term_ x = diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index 8fcdb5d90..730e055b4 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -396,7 +396,7 @@ let inspect n = let (_, _, v) = get_variable (basename sp) in add_search2 (Nametab.locate (qualid_of_sp sp)) v | (sp,kn), "CONSTANT" -> - let {const_type=typ} = Global.lookup_constant (constant_of_kn kn) in + let typ = Typeops.type_of_constant (Global.env()) (constant_of_kn kn) in add_search2 (Nametab.locate (qualid_of_sp sp)) typ | (sp,kn), "MUTUALINDUCTIVE" -> add_search2 (Nametab.locate (qualid_of_sp sp)) diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index 6195caa47..9a503cfb5 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -149,7 +149,7 @@ let make_definition_ast name c typ implicits = let constant_to_ast_list kn = let cb = Global.lookup_constant kn in let c = cb.const_body in - let typ = cb.const_type in + let typ = Typeops.type_of_constant_type (Global.env()) cb.const_type in let l = implicits_of_global (ConstRef kn) in (match c with None -> diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index 997821c53..4bec73501 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -725,7 +725,7 @@ let rec nsortrec vl x = | Case(_,x,t,a) -> nsortrec vl x | Cast(x,_, t)-> nsortrec vl t - | Const c -> nsortrec vl (lookup_constant c vl).const_type + | Const c -> nsortrec vl (Typeops.type_of_constant vl c) | _ -> nsortrec vl (type_of vl Evd.empty x) ;; let nsort x = diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index 0d7146e68..353fcdb3b 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -119,8 +119,7 @@ let def_of_const t = let type_of_const t = match (kind_of_term t) with - Const sp -> - (Global.lookup_constant sp).const_type + Const sp -> Typeops.type_of_constant (Global.env()) sp |_ -> assert false let arg_type t = diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index f217b0371..ff07c3c47 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -241,7 +241,7 @@ let typeur sigma metamap = Util.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound")) | T.Const c -> let cb = Environ.lookup_constant c env in - T.body_of_type cb.Declarations.const_type + Typeops.type_of_constant_type env (cb.Declarations.const_type) | T.Evar ev -> Evd.existential_type sigma ev | T.Ind ind -> T.body_of_type (Inductiveops.type_of_inductive env ind) | T.Construct cstr -> diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml index a3336817e..c7d3b4ff0 100644 --- a/contrib/xml/doubleTypeInference.ml +++ b/contrib/xml/doubleTypeInference.ml @@ -122,7 +122,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = Typeops.judge_of_variable env id | T.Const c -> - E.make_judge cstr (E.constant_type env c) + E.make_judge cstr (Typeops.type_of_constant env c) | T.Ind ind -> E.make_judge cstr (Inductiveops.type_of_inductive env ind) diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 2e490b4c0..f286d2c8a 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -408,7 +408,7 @@ let mk_inductive_obj sp mib packs variables nparams hyps finite = let {D.mind_consnames=consnames ; D.mind_typename=typename } = p in - let arity = Inductive.type_of_inductive (mib,p) in + let arity = Inductive.type_of_inductive (Global.env()) (mib,p) in let lc = Inductiveops.arities_of_constructors (Global.env ()) (sp,!tyno) in let cons = (Array.fold_right (fun (name,lc) i -> (name,lc)::i) @@ -522,6 +522,7 @@ let print internal glob_ref kind xml_library_root = let id = N.id_of_label (N.con_label kn) in let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} = G.lookup_constant kn in + let typ = Typeops.type_of_constant_type (Global.env()) typ in Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps | Ln.IndRef (kn,_) -> let mib = G.lookup_mind kn in diff --git a/kernel/cooking.ml b/kernel/cooking.ml index dffbb76c0..68d301eb4 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -122,7 +122,14 @@ let cook_constant env r = on_body (fun c -> abstract_constant_body (expmod_constr r.d_modlist c) hyps) cb.const_body in - let typ = - abstract_constant_type (expmod_constr r.d_modlist cb.const_type) hyps in + let typ = match cb.const_type with + | NonPolymorphicType t -> + let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in + NonPolymorphicType typ + | PolymorphicArity (ctx,s) -> + let t = mkArity (ctx,Type s.poly_level) in + let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in + let ctx,_ = dest_prod env typ in + PolymorphicArity (ctx,s) in let boxed = Cemitcodes.is_boxed cb.const_body_code in (body, typ, cb.const_constraints, cb.const_opaque, boxed) diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 2e7a3639a..0646b1c22 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -25,7 +25,7 @@ type recipe = { val cook_constant : env -> recipe -> - constr_substituted option * constr * constraints * bool * bool + constr_substituted option * constant_type * constraints * bool * bool (*s Utility functions used in module [Discharge]. *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 17a8d5ac9..d0f2289dc 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -25,6 +25,15 @@ type engagement = ImpredicativeSet (*s Constants (internal representation) (Definition/Axiom) *) +type polymorphic_arity = { + poly_param_levels : universe option list; + poly_level : universe; +} + +type constant_type = + | NonPolymorphicType of types + | PolymorphicArity of rel_context * polymorphic_arity + type constr_substituted = constr substituted let from_val = from_val @@ -36,7 +45,7 @@ let subst_constr_subst = subst_substituted type constant_body = { const_hyps : section_context; (* New: younger hyp at top *) const_body : constr_substituted option; - const_type : types; + const_type : constant_type; const_body_code : Cemitcodes.to_patch_substituted; (* const_type_code : Cemitcodes.to_patch; *) const_constraints : constraints; @@ -90,11 +99,6 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p with In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn *) -type polymorphic_inductive_arity = { - mind_param_levels : universe option list; - mind_level : universe; -} - type monomorphic_inductive_arity = { mind_user_arity : constr; mind_sort : sorts; @@ -102,7 +106,7 @@ type monomorphic_inductive_arity = { type inductive_arity = | Monomorphic of monomorphic_inductive_arity -| Polymorphic of polymorphic_inductive_arity +| Polymorphic of polymorphic_arity type one_inductive_body = { @@ -186,11 +190,15 @@ type mutual_inductive_body = { mind_equiv : kernel_name option } +let subst_arity sub = function +| NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s) +| PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s) + (* TODO: should be changed to non-coping after Term.subst_mps *) let subst_const_body sub cb = { const_hyps = (assert (cb.const_hyps=[]); []); const_body = option_map (subst_constr_subst sub) cb.const_body; - const_type = subst_mps sub cb.const_type; + const_type = subst_arity sub cb.const_type; const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code; (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*) const_constraints = cb.const_constraints; diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 2cbdc3eb3..22cfd62a0 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -26,6 +26,15 @@ type engagement = ImpredicativeSet (**********************************************************************) (*s Representation of constants (Definition/Axiom) *) +type polymorphic_arity = { + poly_param_levels : universe option list; + poly_level : universe; +} + +type constant_type = + | NonPolymorphicType of types + | PolymorphicArity of rel_context * polymorphic_arity + type constr_substituted val from_val : constr -> constr_substituted @@ -34,7 +43,7 @@ val force : constr_substituted -> constr type constant_body = { const_hyps : section_context; (* New: younger hyp at top *) const_body : constr_substituted option; - const_type : types; + const_type : constant_type; const_body_code : to_patch_substituted; (*i const_type_code : to_patch;i*) const_constraints : constraints; @@ -70,11 +79,6 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths \end{verbatim} *) -type polymorphic_inductive_arity = { - mind_param_levels : universe option list; - mind_level : universe; -} - type monomorphic_inductive_arity = { mind_user_arity : constr; mind_sort : sorts; @@ -82,7 +86,7 @@ type monomorphic_inductive_arity = { type inductive_arity = | Monomorphic of monomorphic_inductive_arity -| Polymorphic of polymorphic_inductive_arity +| Polymorphic of polymorphic_arity type one_inductive_body = { diff --git a/kernel/environ.mli b/kernel/environ.mli index b6d9bf6d3..5fa5f5674 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -129,7 +129,7 @@ type const_evaluation_result = NoBody | Opaque exception NotEvaluableConst of const_evaluation_result val constant_value : env -> constant -> constr -val constant_type : env -> constant -> types +val constant_type : env -> constant -> constant_type val constant_opt_value : env -> constant -> constr option (************************************************************************) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index a41cc53be..4187b8bd6 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -392,7 +392,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) = let specif = lookup_mind_specif env mi in let env' = push_rel (Anonymous,None, - hnf_prod_applist env (type_of_inductive specif) lpar) env in + hnf_prod_applist env (type_of_inductive env specif) lpar) env in let ra_env' = (Imbr mi,Rtree.mk_param 0) :: List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in @@ -601,8 +601,8 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = let arkind,kelim = match ar_kind with | Inr (param_levels,lev) -> Polymorphic { - mind_param_levels = param_levels; - mind_level = lev; + poly_param_levels = param_levels; + poly_level = lev; }, all_sorts | Inl ((issmall,isunit),ar,s) -> let isunit = isunit && ntypes = 1 && not (is_recursive recargs.(0)) in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index bce14dc27..7dd9aa786 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -177,10 +177,10 @@ let rec make_subst env = function | [], _, _ -> assert false -let instantiate_universes env ctx mip ar argsorts = +let instantiate_universes env ctx ar argsorts = let args = Array.to_list argsorts in - let ctx,subst = make_subst env (ctx,ar.mind_param_levels,args) in - let level = subst_large_constraints subst ar.mind_level in + let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in + let level = subst_large_constraints subst ar.poly_level in ctx, if is_empty_univ level then mk_Prop else if is_base_univ level then mk_Set @@ -192,9 +192,14 @@ let type_of_inductive_knowing_parameters env mip paramtyps = s.mind_user_arity | Polymorphic ar -> let ctx = List.rev mip.mind_arity_ctxt in - let ctx,s = instantiate_universes env ctx mip ar paramtyps in + let ctx,s = instantiate_universes env ctx ar paramtyps in mkArity (List.rev ctx,s) +(* Type of a (non applied) inductive type *) + +let type_of_inductive env (_,mip) = + type_of_inductive_knowing_parameters env mip [||] + (* The max of an array of universes *) let cumulate_constructor_univ u = function @@ -205,20 +210,6 @@ let cumulate_constructor_univ u = function let max_inductive_sort = Array.fold_left cumulate_constructor_univ neutral_univ -(* Type of a (non applied) inductive type *) - -let type_of_inductive (mib,mip) = - match mip.mind_arity with - | Monomorphic s -> s.mind_user_arity - | Polymorphic s -> - let s = - if mib.mind_nparams = 0 then - if is_empty_univ s.mind_level then mk_Prop - else if is_base_univ s.mind_level then mk_Set - else Type s.mind_level - else Type s.mind_level in - mkArity (mip.mind_arity_ctxt,s) - (************************************************************************) (* Type of a constructor *) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index deca20a6b..9c75829d5 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -37,7 +37,7 @@ val lookup_mind_specif : env -> inductive -> mind_specif (*s Functions to build standard types related to inductive *) val ind_subst : mutual_inductive -> mutual_inductive_body -> constr list -val type_of_inductive : mind_specif -> types +val type_of_inductive : env -> mind_specif -> types val elim_sorts : mind_specif -> sorts_family list @@ -84,6 +84,9 @@ val set_inductive_level : env -> sorts -> types -> types val max_inductive_sort : sorts array -> universe +val instantiate_universes : env -> Sign.rel_context -> + polymorphic_arity -> types array -> Sign.rel_context * sorts + (***************************************************************) (* Debug *) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index efbee6af2..785778235 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -87,8 +87,8 @@ and merge_with env mtb with_decl = match cb.const_body with | None -> let (j,cst1) = Typeops.infer env' c in - let cst2 = - Reduction.conv_leq env' j.uj_type cb.const_type in + let typ = Typeops.type_of_constant_type env' cb.const_type in + let cst2 = Reduction.conv_leq env' j.uj_type typ in let cst = Constraint.union (Constraint.union cb.const_constraints cst1) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 264bd6215..9cfce4303 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -119,6 +119,12 @@ type global_declaration = | ConstantEntry of constant_entry | GlobalRecipe of Cooking.recipe +let hcons_constant_type = function + | NonPolymorphicType t -> + NonPolymorphicType (hcons1_constr t) + | PolymorphicArity (ctx,s) -> + PolymorphicArity (map_rel_context hcons1_constr ctx,s) + let hcons_constant_body cb = let body = match cb.const_body with None -> None @@ -127,7 +133,7 @@ let hcons_constant_body cb = in { cb with const_body = body; - const_type = hcons1_constr cb.const_type } + const_type = hcons_constant_type cb.const_type } let add_constant dir l decl senv = check_label l senv.labset; diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index c94219316..12c714411 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -96,7 +96,7 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = (* nparams done *) (* params_ctxt done because part of the inductive types *) (* Don't check the sort of the type if polymorphic *) - let cst = check_conv cst conv env (type_of_inductive (mib1,p1)) (type_of_inductive (mib2,p2)) + let cst = check_conv cst conv env (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2)) in cst in @@ -164,7 +164,9 @@ let check_constant cst env msid1 l info1 cb2 spec2 = | Constant cb1 -> assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ; (*Start by checking types*) - let cst = check_conv cst conv_leq env cb1.const_type cb2.const_type in + let typ1 = Typeops.type_of_constant_type env cb1.const_type in + let typ2 = Typeops.type_of_constant_type env cb2.const_type in + let cst = check_conv cst conv_leq env typ1 typ2 in let con = make_con (MPself msid1) empty_dirpath l in let cst = match cb2.const_body with @@ -186,8 +188,9 @@ let check_constant cst env msid1 l info1 cb2 spec2 = "name.")); assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ; if cb2.const_body <> None then error () ; - let arity1 = type_of_inductive (mind1,mind1.mind_packets.(i)) in - check_conv cst conv_leq env arity1 cb2.const_type + let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in + let typ2 = Typeops.type_of_constant_type env cb2.const_type in + check_conv cst conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> ignore (Util.error ( "The kernel does not recognize yet that a parameter can be " ^ @@ -197,7 +200,8 @@ let check_constant cst env msid1 l info1 cb2 spec2 = assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ; if cb2.const_body <> None then error () ; let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in - check_conv cst conv env ty1 cb2.const_type + let ty2 = Typeops.type_of_constant_type env cb2.const_type in + check_conv cst conv env ty1 ty2 | _ -> error () let rec check_modules cst env msid1 l msb1 msb2 = diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index f76c5ffe3..94cd39760 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -22,8 +22,35 @@ open Type_errors open Indtypes open Typeops +let extract_level env p = + let _,c = dest_prod_assum env p in + match kind_of_term c with Sort (Type u) -> Some u | _ -> None + +let extract_context_levels env = + List.fold_left + (fun l (_,b,p) -> if b=None then extract_level env p::l else l) [] + +let make_polymorphic_if_arity env t = + let params, ccl = dest_prod env t in + match kind_of_term ccl with + | Sort (Type u) -> + let param_ccls = extract_context_levels env params in + let s = { poly_param_levels = param_ccls; poly_level = u} in + PolymorphicArity (params,s) + | _ -> NonPolymorphicType t + let constrain_type env j cst1 = function - | None -> j.uj_type, cst1 + | None -> + make_polymorphic_if_arity env j.uj_type, cst1 + | Some t -> + let (tj,cst2) = infer_type env t in + let (_,cst3) = judge_of_cast env j DEFAULTcast tj in + assert (t = tj.utj_val); + make_polymorphic_if_arity env t, Constraint.union (Constraint.union cst1 cst2) cst3 + +let local_constrain_type env j cst1 = function + | None -> + j.uj_type, cst1 | Some t -> let (tj,cst2) = infer_type env t in let (_,cst3) = judge_of_cast env j DEFAULTcast tj in @@ -32,7 +59,7 @@ let constrain_type env j cst1 = function let translate_local_def env (b,topt) = let (j,cst) = infer env b in - let (typ,cst) = constrain_type env j cst topt in + let (typ,cst) = local_constrain_type env j cst topt in (j.uj_val,typ,cst) let translate_local_assum env t = @@ -83,16 +110,25 @@ let infer_declaration env dcl = c.const_entry_opaque, c.const_entry_boxed | ParameterEntry t -> let (j,cst) = infer env t in - None, Typeops.assumption_of_judgment env j, cst, false, false + None, NonPolymorphicType (Typeops.assumption_of_judgment env j), cst, + false, false + +let global_vars_set_constant_type env = function + | NonPolymorphicType t -> global_vars_set env t + | PolymorphicArity (ctx,_) -> + Sign.fold_rel_context + (fold_rel_declaration + (fun t c -> Idset.union (global_vars_set env t) c)) + ctx ~init:Idset.empty let build_constant_declaration env kn (body,typ,cst,op,boxed) = let ids = match body with - | None -> global_vars_set env typ + | None -> global_vars_set_constant_type env typ | Some b -> Idset.union (global_vars_set env (Declarations.force b)) - (global_vars_set env typ) + (global_vars_set_constant_type env typ) in let tps = Cemitcodes.from_val (compile_constant_body env body op boxed) in let hyps = keep_hyps env ids in diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 6fac9e050..83434e2ec 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -26,12 +26,11 @@ val translate_local_assum : env -> types -> types * Univ.constraints val infer_declaration : env -> constant_entry -> - Declarations.constr_substituted option * Term.types * Univ.constraints * - bool * bool + constr_substituted option * constant_type * constraints * bool * bool -val build_constant_declaration : env -> 'a -> - Declarations.constr_substituted option * Term.types * Univ.constraints * - bool * bool -> Declarations.constant_body +val build_constant_declaration : env -> 'a -> + constr_substituted option * constant_type * constraints * bool * bool -> + constant_body val translate_constant : env -> constant -> constant_entry -> constant_body diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 0d2874cb7..3c335d115 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -126,12 +126,31 @@ let check_hyps id env hyps = (* Instantiation of terms on real arguments. *) (* Type of constants *) + +let type_of_constant_knowing_parameters env t paramtyps = + match t with + | NonPolymorphicType t -> t + | PolymorphicArity (sign,ar) -> + let ctx = List.rev sign in + let ctx,s = instantiate_universes env ctx ar paramtyps in + mkArity (List.rev ctx,s) + +let type_of_constant_type env t = + type_of_constant_knowing_parameters env t [||] + +let type_of_constant env cst = + type_of_constant_type env (constant_type env cst) + +let judge_of_constant_knowing_parameters env cst jl = + let c = mkConst cst in + let cb = lookup_constant cst env in + let _ = check_args env c cb.const_hyps in + let paramstyp = Array.map (fun j -> j.uj_type) jl in + let t = type_of_constant_knowing_parameters env cb.const_type paramstyp in + make_judge c t + let judge_of_constant env cst = - let constr = mkConst cst in - let _ = - let ce = lookup_constant cst env in - check_args env constr ce.const_hyps in - make_judge constr (constant_type env cst) + judge_of_constant_knowing_parameters env cst [||] (* Type of a lambda-abstraction. *) @@ -348,11 +367,16 @@ let rec execute env cstr cu = | App (f,args) -> let (jl,cu1) = execute_array env args cu in let (j,cu2) = - if isInd f then - (* Sort-polymorphism of inductive types *) - judge_of_inductive_knowing_parameters env (destInd f) jl, cu1 - else - execute env f cu1 + match kind_of_term f with + | Ind ind -> + (* Sort-polymorphism of inductive types *) + judge_of_inductive_knowing_parameters env ind jl, cu1 + | Const cst -> + (* Sort-polymorphism of constant *) + judge_of_constant_knowing_parameters env cst jl, cu1 + | _ -> + (* No sort-polymorphism *) + execute env f cu1 in univ_combinator cu2 (judge_of_apply env j jl) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index aeb4d294b..43d7b33db 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -14,6 +14,7 @@ open Univ open Term open Environ open Entries +open Declarations (*i*) (*s Typing functions (not yet tagged as safe) *) @@ -47,6 +48,9 @@ val judge_of_variable : env -> variable -> unsafe_judgment (*s type of a constant *) val judge_of_constant : env -> constant -> unsafe_judgment +val judge_of_constant_knowing_parameters : + env -> constant -> unsafe_judgment array -> unsafe_judgment + (*s Type of application. *) val judge_of_apply : env -> unsafe_judgment -> unsafe_judgment array @@ -93,8 +97,9 @@ val type_fixpoint : env -> name array -> types array (* Kernel safe typing but applicable to partial proofs *) val typing : env -> constr -> unsafe_judgment -(* A virer *) -val execute : Environ.env -> - Term.types -> - Univ.Constraint.t * Univ.universes -> - Environ.unsafe_judgment * (Univ.Constraint.t * Univ.universes) +val type_of_constant : env -> constant -> types + +val type_of_constant_type : env -> constant_type -> types + +val type_of_constant_knowing_parameters : + env -> constant_type -> constr array -> types diff --git a/library/global.ml b/library/global.ml index 19b416519..30281bcc7 100644 --- a/library/global.ml +++ b/library/global.ml @@ -141,10 +141,10 @@ open Libnames let type_of_reference env = function | VarRef id -> Environ.named_type id env - | ConstRef c -> Environ.constant_type env c + | ConstRef c -> Typeops.type_of_constant env c | IndRef ind -> let specif = Inductive.lookup_mind_specif env ind in - Inductive.type_of_inductive specif + Inductive.type_of_inductive env specif | ConstructRef cstr -> let specif = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in diff --git a/library/impargs.ml b/library/impargs.ml index ffdeb0b88..b5488031b 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -259,10 +259,9 @@ let list_of_implicits = function let constants_table = ref Cmap.empty -let compute_constant_implicits kn = +let compute_constant_implicits cst = let env = Global.env () in - let cb = lookup_constant kn env in - auto_implicits env (body_of_type cb.const_type) + auto_implicits env (Typeops.type_of_constant env cst) let constant_implicits sp = try Cmap.find sp !constants_table with Not_found -> No_impl @@ -282,12 +281,13 @@ let compute_mib_implicits kn = let ar = Array.to_list (Array.map (* No need to lift, arities contain no de Bruijn *) - (fun mip -> (Name mip.mind_typename, None, type_of_inductive (mib,mip))) + (fun mip -> + (Name mip.mind_typename, None, type_of_inductive env (mib,mip))) mib.mind_packets) in let env_ar = push_rel_context ar env in let imps_one_inductive i mip = let ind = (kn,i) in - let ar = type_of_inductive (mib,mip) in + let ar = type_of_inductive env (mib,mip) in ((IndRef ind,auto_implicits env ar), Array.mapi (fun j c -> (ConstructRef (ind,j+1),auto_implicits env_ar c)) mip.mind_nf_lc) diff --git a/parsing/search.ml b/parsing/search.ml index 580cb790c..e225d59a4 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -57,12 +57,12 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) = fn (VarRef idc) env typ with Not_found -> (* we are in a section *) ()) | "CONSTANT" -> - let kn = locate_constant (qualid_of_sp sp) in - let {const_type=typ} = Global.lookup_constant kn in + let cst = locate_constant (qualid_of_sp sp) in + let typ = Typeops.type_of_constant env cst in if refopt = None || head_const typ = constr_of_global (out_some refopt) then - fn (ConstRef kn) env typ + fn (ConstRef cst) env typ | "INDUCTIVE" -> let kn = locate_mind (qualid_of_sp sp) in let mib = Global.lookup_mind kn in diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 452639170..041187d84 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -23,7 +23,7 @@ open Reductionops let type_of_inductive env ind = let specif = Inductive.lookup_mind_specif env ind in - Inductive.type_of_inductive specif + Inductive.type_of_inductive env specif (* Return type as quoted by the user *) let type_of_constructor env cstr = diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 1756c8377..656f370ae 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -53,9 +53,7 @@ let typeur sigma metamap = body_of_type ty with Not_found -> anomaly ("type_of: variable "^(string_of_id id)^" unbound")) - | Const c -> - let cb = lookup_constant c env in - body_of_type cb.const_type + | Const cst -> Typeops.type_of_constant env cst | Evar ev -> Evd.existential_type sigma ev | Ind ind -> body_of_type (type_of_inductive env ind) | Construct cstr -> body_of_type (type_of_constructor env cstr) @@ -76,6 +74,9 @@ let typeur sigma metamap = | App(f,args) when isInd f -> let t = type_of_inductive_knowing_parameters env (destInd f) args in strip_outer_cast (subst_type env sigma t (Array.to_list args)) + | App(f,args) when isConst f -> + let t = type_of_constant_knowing_parameters env (destConst f) args in + strip_outer_cast (subst_type env sigma t (Array.to_list args)) | App(f,args) -> strip_outer_cast (subst_type env sigma (type_of env f) (Array.to_list args)) @@ -100,6 +101,9 @@ let typeur sigma metamap = | App(f,args) when isInd f -> let t = type_of_inductive_knowing_parameters env (destInd f) args in sort_of_atomic_type env sigma t args + | App(f,args) when isConst f -> + let t = type_of_constant_knowing_parameters env (destConst f) args in + sort_of_atomic_type env sigma t args | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args | Lambda _ | Fix _ | Construct _ -> anomaly "sort_of: Not a type (1)" @@ -122,16 +126,24 @@ let typeur sigma metamap = let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in Inductive.type_of_inductive_knowing_parameters env mip argtyps - in type_of, sort_of, sort_family_of, type_of_inductive_knowing_parameters + and type_of_constant_knowing_parameters env cst args = + let t = constant_type env cst in + let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in + Typeops.type_of_constant_knowing_parameters env t argtyps + + in type_of, sort_of, sort_family_of, + type_of_inductive_knowing_parameters, type_of_constant_knowing_parameters -let get_type_of env sigma c = let f,_,_,_ = typeur sigma [] in f env c -let get_sort_of env sigma t = let _,f,_,_ = typeur sigma [] in f env t -let get_sort_family_of env sigma c = let _,_,f,_ = typeur sigma [] in f env c +let get_type_of env sigma c = let f,_,_,_,_ = typeur sigma [] in f env c +let get_sort_of env sigma t = let _,f,_,_,_ = typeur sigma [] in f env t +let get_sort_family_of env sigma c = let _,_,f,_,_ = typeur sigma [] in f env c let type_of_inductive_knowing_parameters env sigma ind args = - let _,_,_,f = typeur sigma [] in f env ind args + let _,_,_,f,_ = typeur sigma [] in f env ind args +let type_of_constant_knowing_parameters env sigma cst args = + let _,_,_,_,f = typeur sigma [] in f env cst args let get_type_of_with_meta env sigma metamap = - let f,_,_,_ = typeur sigma metamap in f env + let f,_,_,_,_ = typeur sigma metamap in f env (* Makes an assumption from a constr *) let get_assumption_of env evc c = c diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 900a96829..32b90cd86 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -36,3 +36,6 @@ val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment val type_of_inductive_knowing_parameters : env -> evar_map -> inductive -> constr array -> types + +val type_of_constant_knowing_parameters : env -> evar_map -> constant -> + constr array -> types diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 57c83fa7e..d248ba70e 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -53,7 +53,7 @@ let rec execute env evd cstr = j_nf_evar (evars_of evd) (judge_of_variable env id) | Const c -> - make_judge cstr (nf_evar (evars_of evd) (constant_type env c)) + make_judge cstr (nf_evar (evars_of evd) (type_of_constant env c)) | Ind ind -> make_judge cstr (nf_evar (evars_of evd) (type_of_inductive env ind)) @@ -90,12 +90,17 @@ let rec execute env evd cstr = | App (f,args) -> let jl = execute_array env evd args in let j = - if isInd f then - (* Sort-polymorphism of inductive types *) - judge_of_inductive_knowing_parameters env (destInd f) - (jv_nf_evar (evars_of evd) jl) - else - execute env evd f + match kind_of_term f with + | Ind ind -> + (* Sort-polymorphism of inductive types *) + judge_of_inductive_knowing_parameters env ind + (jv_nf_evar (evars_of evd) jl) + | Const cst -> + (* Sort-polymorphism of inductive types *) + judge_of_constant_knowing_parameters env cst + (jv_nf_evar (evars_of evd) jl) + | _ -> + execute env evd f in fst (judge_of_apply env j jl) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index fb05661d7..55f798de9 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -70,7 +70,7 @@ let construct_of_constr_block env tag typ = let constr_type_of_idkey env idkey = match idkey with | ConstKey cst -> - mkConst cst, (lookup_constant cst env).const_type + mkConst cst, Typeops.type_of_constant env cst | VarKey id -> let (_,_,ty) = lookup_named id env in mkVar id, ty @@ -80,7 +80,7 @@ let constr_type_of_idkey env idkey = mkRel n, lift n ty let type_of_ind env ind = - type_of_inductive (Inductive.lookup_mind_specif env ind) + type_of_inductive env (Inductive.lookup_mind_specif env ind) let build_branches_type env (mind,_ as _ind) mib mip params dep p = let rtbl = mip.mind_reloc_tbl in diff --git a/proofs/logic.ml b/proofs/logic.ml index 61e4ec58e..5f765c962 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -291,9 +291,17 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | App (f,l) -> let (acc',hdty) = - if isInd f & not (array_exists occur_meta l) (* we could be finer *) - then (goalacc,type_of_inductive_knowing_parameters env sigma (destInd f) l) - else mk_hdgoals sigma goal goalacc f + match kind_of_term f with + | Ind ind + when not (array_exists occur_meta l) (* we could be finer *) -> + (* Sort-polymorphism of inductive types *) + goalacc, type_of_inductive_knowing_parameters env sigma ind l + | Const cst + when not (array_exists occur_meta l) (* we could be finer *) -> + (* Sort-polymorphism of inductive types *) + goalacc, type_of_constant_knowing_parameters env sigma cst l + | _ -> + mk_hdgoals sigma goal goalacc f in let (acc'',conclty') = mk_arggoals sigma goal acc' hdty (Array.to_list l) in diff --git a/toplevel/command.ml b/toplevel/command.ml index b333a51bb..aee4afb43 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -105,7 +105,7 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) = let b = abstract_constr_expr com bl in let j = interp_constr_judgment sigma env b in { const_entry_body = j.uj_val; - const_entry_type = Some (refresh_universes j.uj_type); + const_entry_type = None; const_entry_opaque = opacity; const_entry_boxed = boxed } | Some comtyp -> @@ -225,7 +225,8 @@ let declare_one_elimination ind = if List.mem InType kelim then let elim = make_elim (new_sort_in_family InType) in let cte = declare (mindstr^(Indrec.elimination_suffix InType)) elim None in - let c = mkConst cte and t = constant_type (Global.env()) cte in + let c = mkConst cte in + let t = type_of_constant (Global.env()) cte in List.iter (fun (sort,suff) -> let (t',c') = Indrec.instantiate_type_indrec_scheme (new_sort_in_family sort) diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index ede095fbe..3f1b4c2c2 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -73,7 +73,7 @@ let process_inductive sechyps modlist mib = let inds = array_map_to_list (fun mip -> - let arity = expmod_constr modlist (Termops.refresh_universes (Inductive.type_of_inductive (mib,mip))) in + let arity = expmod_constr modlist (Termops.refresh_universes (Inductive.type_of_inductive (Global.env()) (mib,mip))) in let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in (mip.mind_typename, arity, |