diff options
55 files changed, 726 insertions, 765 deletions
@@ -132,8 +132,8 @@ parsing/pcoq.cmi: toplevel/vernacexpr.cmo lib/util.cmi interp/topconstr.cmi \ library/decl_kinds.cmo lib/bigint.cmi parsing/ppconstr.cmi: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \ proofs/tacexpr.cmo pretyping/rawterm.cmi interp/ppextend.cmi lib/pp.cmi \ - parsing/pcoq.cmi pretyping/pattern.cmi kernel/names.cmi \ - library/libnames.cmi interp/genarg.cmi kernel/environ.cmi + parsing/pcoq.cmi kernel/names.cmi library/libnames.cmi interp/genarg.cmi \ + kernel/environ.cmi parsing/pptactic.cmi: interp/topconstr.cmi kernel/term.cmi proofs/tacexpr.cmo \ pretyping/rawterm.cmi proofs/proof_type.cmi pretyping/pretyping.cmi \ interp/ppextend.cmi lib/pp.cmi library/libnames.cmi interp/genarg.cmi \ @@ -643,14 +643,12 @@ interp/syntax_def.cmx: lib/util.cmx interp/topconstr.cmx library/summary.cmx \ library/libnames.cmx library/lib.cmx interp/syntax_def.cmi interp/topconstr.cmo: lib/util.cmi kernel/term.cmi pretyping/rawterm.cmi \ lib/pp.cmi lib/options.cmi kernel/names.cmi library/nameops.cmi \ - kernel/mod_subst.cmi library/libnames.cmi library/global.cmi \ - pretyping/evd.cmi lib/dyn.cmi pretyping/detyping.cmi lib/bigint.cmi \ - interp/topconstr.cmi + kernel/mod_subst.cmi library/libnames.cmi pretyping/evd.cmi lib/dyn.cmi \ + pretyping/detyping.cmi lib/bigint.cmi interp/topconstr.cmi interp/topconstr.cmx: lib/util.cmx kernel/term.cmx pretyping/rawterm.cmx \ lib/pp.cmx lib/options.cmx kernel/names.cmx library/nameops.cmx \ - kernel/mod_subst.cmx library/libnames.cmx library/global.cmx \ - pretyping/evd.cmx lib/dyn.cmx pretyping/detyping.cmx lib/bigint.cmx \ - interp/topconstr.cmi + kernel/mod_subst.cmx library/libnames.cmx pretyping/evd.cmx lib/dyn.cmx \ + pretyping/detyping.cmx lib/bigint.cmx interp/topconstr.cmi kernel/cbytecodes.cmo: kernel/term.cmi kernel/names.cmi kernel/cbytecodes.cmi kernel/cbytecodes.cmx: kernel/term.cmx kernel/names.cmx kernel/cbytecodes.cmi kernel/cbytegen.cmo: lib/util.cmi kernel/term.cmi kernel/pre_env.cmi \ @@ -739,10 +737,10 @@ kernel/modops.cmx: lib/util.cmx kernel/univ.cmx kernel/term.cmx lib/pp.cmx \ kernel/names.cmx kernel/mod_subst.cmx kernel/environ.cmx \ kernel/entries.cmx kernel/declarations.cmx kernel/cemitcodes.cmx \ kernel/modops.cmi -kernel/names.cmo: lib/util.cmi lib/predicate.cmi lib/pp.cmi lib/options.cmi \ - lib/hashcons.cmi kernel/names.cmi -kernel/names.cmx: lib/util.cmx lib/predicate.cmx lib/pp.cmx lib/options.cmx \ - lib/hashcons.cmx kernel/names.cmi +kernel/names.cmo: lib/util.cmi lib/predicate.cmi lib/pp.cmi lib/hashcons.cmi \ + kernel/names.cmi +kernel/names.cmx: lib/util.cmx lib/predicate.cmx lib/pp.cmx lib/hashcons.cmx \ + kernel/names.cmi kernel/pre_env.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi \ kernel/sign.cmi kernel/names.cmi kernel/declarations.cmi \ kernel/pre_env.cmi @@ -1091,16 +1089,16 @@ parsing/ppconstr.cmo: lib/util.cmi kernel/univ.cmi interp/topconstr.cmi \ pretyping/termops.cmi kernel/term.cmi pretyping/rawterm.cmi \ interp/ppextend.cmi lib/pp.cmi pretyping/pattern.cmi lib/options.cmi \ interp/notation.cmi library/nametab.cmi kernel/names.cmi \ - library/nameops.cmi library/libnames.cmi library/global.cmi \ - interp/genarg.cmi pretyping/evd.cmi interp/constrintern.cmi \ - interp/constrextern.cmi lib/bigint.cmi parsing/ppconstr.cmi + library/nameops.cmi library/libnames.cmi interp/genarg.cmi \ + pretyping/evd.cmi interp/constrextern.cmi lib/bigint.cmi \ + parsing/ppconstr.cmi parsing/ppconstr.cmx: lib/util.cmx kernel/univ.cmx interp/topconstr.cmx \ pretyping/termops.cmx kernel/term.cmx pretyping/rawterm.cmx \ interp/ppextend.cmx lib/pp.cmx pretyping/pattern.cmx lib/options.cmx \ interp/notation.cmx library/nametab.cmx kernel/names.cmx \ - library/nameops.cmx library/libnames.cmx library/global.cmx \ - interp/genarg.cmx pretyping/evd.cmx interp/constrintern.cmx \ - interp/constrextern.cmx lib/bigint.cmx parsing/ppconstr.cmi + library/nameops.cmx library/libnames.cmx interp/genarg.cmx \ + pretyping/evd.cmx interp/constrextern.cmx lib/bigint.cmx \ + parsing/ppconstr.cmi parsing/pptactic.cmo: lib/util.cmi interp/topconstr.cmi pretyping/termops.cmi \ kernel/term.cmi proofs/tactic_debug.cmi proofs/tacexpr.cmo \ pretyping/rawterm.cmi proofs/proof_type.cmi parsing/printer.cmi \ @@ -1157,15 +1155,15 @@ parsing/prettyp.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.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 pretyping/pattern.cmi \ - lib/options.cmi library/nametab.cmi kernel/names.cmi library/nameops.cmi \ + parsing/ppconstr.cmi lib/pp.cmi proofs/pfedit.cmi lib/options.cmi \ + library/nametab.cmi kernel/names.cmi library/nameops.cmi \ library/libnames.cmi library/global.cmi pretyping/evd.cmi \ pretyping/evarutil.cmi kernel/environ.cmi library/declare.cmi \ interp/constrextern.cmi parsing/printer.cmi parsing/printer.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ kernel/sign.cmx proofs/refiner.cmx proofs/proof_type.cmx \ - parsing/ppconstr.cmx lib/pp.cmx proofs/pfedit.cmx pretyping/pattern.cmx \ - lib/options.cmx library/nametab.cmx kernel/names.cmx library/nameops.cmx \ + parsing/ppconstr.cmx lib/pp.cmx proofs/pfedit.cmx lib/options.cmx \ + library/nametab.cmx kernel/names.cmx library/nameops.cmx \ library/libnames.cmx library/global.cmx pretyping/evd.cmx \ pretyping/evarutil.cmx kernel/environ.cmx library/declare.cmx \ interp/constrextern.cmx parsing/printer.cmi @@ -1388,23 +1386,21 @@ pretyping/pretyping.cmo: lib/util.cmi kernel/typeops.cmi \ kernel/sign.cmi pretyping/retyping.cmi pretyping/reductionops.cmi \ pretyping/recordops.cmi pretyping/rawterm.cmi \ pretyping/pretype_errors.cmi lib/pp.cmi pretyping/pattern.cmi \ - lib/options.cmi kernel/names.cmi library/libnames.cmi \ - pretyping/inductiveops.cmi kernel/inductive.cmi pretyping/indrec.cmi \ - pretyping/evd.cmi pretyping/evarutil.cmi pretyping/evarconv.cmi \ - kernel/environ.cmi lib/dyn.cmi kernel/declarations.cmi \ - pretyping/coercion.cmi pretyping/classops.cmi pretyping/cases.cmi \ - pretyping/pretyping.cmi + kernel/names.cmi library/libnames.cmi pretyping/inductiveops.cmi \ + kernel/inductive.cmi pretyping/evd.cmi pretyping/evarutil.cmi \ + pretyping/evarconv.cmi kernel/environ.cmi lib/dyn.cmi \ + kernel/declarations.cmi pretyping/coercion.cmi pretyping/classops.cmi \ + pretyping/cases.cmi pretyping/pretyping.cmi pretyping/pretyping.cmx: lib/util.cmx kernel/typeops.cmx \ kernel/type_errors.cmx pretyping/termops.cmx kernel/term.cmx \ kernel/sign.cmx pretyping/retyping.cmx pretyping/reductionops.cmx \ pretyping/recordops.cmx pretyping/rawterm.cmx \ pretyping/pretype_errors.cmx lib/pp.cmx pretyping/pattern.cmx \ - lib/options.cmx kernel/names.cmx library/libnames.cmx \ - pretyping/inductiveops.cmx kernel/inductive.cmx pretyping/indrec.cmx \ - pretyping/evd.cmx pretyping/evarutil.cmx pretyping/evarconv.cmx \ - kernel/environ.cmx lib/dyn.cmx kernel/declarations.cmx \ - pretyping/coercion.cmx pretyping/classops.cmx pretyping/cases.cmx \ - pretyping/pretyping.cmi + kernel/names.cmx library/libnames.cmx pretyping/inductiveops.cmx \ + kernel/inductive.cmx pretyping/evd.cmx pretyping/evarutil.cmx \ + pretyping/evarconv.cmx kernel/environ.cmx lib/dyn.cmx \ + kernel/declarations.cmx pretyping/coercion.cmx pretyping/classops.cmx \ + pretyping/cases.cmx pretyping/pretyping.cmi pretyping/rawterm.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi \ kernel/sign.cmi library/nametab.cmi kernel/names.cmi library/libnames.cmi \ pretyping/evd.cmi lib/dyn.cmi pretyping/rawterm.cmi @@ -1790,15 +1786,15 @@ tactics/evar_tactics.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ pretyping/evarutil.cmx proofs/evar_refiner.cmx kernel/environ.cmx \ tactics/evar_tactics.cmi tactics/extraargs.cmo: lib/util.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \ - tactics/setoid_replace.cmi parsing/pptactic.cmi parsing/ppconstr.cmi \ + tactics/setoid_replace.cmi parsing/printer.cmi parsing/pptactic.cmi \ lib/pp.cmi parsing/pcoq.cmi kernel/names.cmi library/nameops.cmi \ toplevel/metasyntax.cmi parsing/lexer.cmi interp/genarg.cmi \ - interp/constrextern.cmi tactics/extraargs.cmi + tactics/extraargs.cmi tactics/extraargs.cmx: lib/util.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \ - tactics/setoid_replace.cmx parsing/pptactic.cmx parsing/ppconstr.cmx \ + tactics/setoid_replace.cmx parsing/printer.cmx parsing/pptactic.cmx \ lib/pp.cmx parsing/pcoq.cmx kernel/names.cmx library/nameops.cmx \ toplevel/metasyntax.cmx parsing/lexer.cmx interp/genarg.cmx \ - interp/constrextern.cmx tactics/extraargs.cmi + tactics/extraargs.cmi tactics/extratactics.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ tactics/tacinterp.cmi proofs/tacexpr.cmo library/summary.cmi \ @@ -2039,8 +2035,6 @@ 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 @@ -2301,20 +2295,18 @@ toplevel/whelp.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ pretyping/termops.cmi kernel/term.cmi proofs/tacmach.cmi lib/system.cmi \ interp/syntax_def.cmi proofs/refiner.cmi pretyping/rawterm.cmi lib/pp.cmi \ proofs/pfedit.cmi parsing/pcoq.cmi lib/options.cmi library/nametab.cmi \ - kernel/names.cmi library/libnames.cmi parsing/lexer.cmi \ - library/global.cmi interp/genarg.cmi kernel/environ.cmi \ - parsing/egrammar.cmi library/dischargedhypsmap.cmi pretyping/detyping.cmi \ - interp/constrintern.cmi toplevel/command.cmi toplevel/cerrors.cmi \ - toplevel/whelp.cmi + kernel/names.cmi library/libnames.cmi parsing/lexer.cmi interp/genarg.cmi \ + kernel/environ.cmi parsing/egrammar.cmi library/dischargedhypsmap.cmi \ + pretyping/detyping.cmi interp/constrintern.cmi toplevel/command.cmi \ + toplevel/cerrors.cmi toplevel/whelp.cmi toplevel/whelp.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ pretyping/termops.cmx kernel/term.cmx proofs/tacmach.cmx lib/system.cmx \ interp/syntax_def.cmx proofs/refiner.cmx pretyping/rawterm.cmx lib/pp.cmx \ proofs/pfedit.cmx parsing/pcoq.cmx lib/options.cmx library/nametab.cmx \ - kernel/names.cmx library/libnames.cmx parsing/lexer.cmx \ - library/global.cmx interp/genarg.cmx kernel/environ.cmx \ - parsing/egrammar.cmx library/dischargedhypsmap.cmx pretyping/detyping.cmx \ - interp/constrintern.cmx toplevel/command.cmx toplevel/cerrors.cmx \ - toplevel/whelp.cmi + kernel/names.cmx library/libnames.cmx parsing/lexer.cmx interp/genarg.cmx \ + kernel/environ.cmx parsing/egrammar.cmx library/dischargedhypsmap.cmx \ + pretyping/detyping.cmx interp/constrintern.cmx toplevel/command.cmx \ + toplevel/cerrors.cmx toplevel/whelp.cmi contrib/cc/ccalgo.cmo: lib/util.cmi kernel/term.cmi lib/pp.cmi \ kernel/names.cmi library/goptions.cmi contrib/cc/ccalgo.cmi contrib/cc/ccalgo.cmx: lib/util.cmx kernel/term.cmx lib/pp.cmx \ @@ -2491,7 +2483,7 @@ contrib/correctness/pwp.cmx: lib/util.cmx pretyping/termops.cmx \ contrib/correctness/pwp.cmi contrib/dp/dp.cmo: lib/util.cmi pretyping/typing.cmi pretyping/termops.cmi \ kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \ - proofs/tacmach.cmi library/summary.cmi parsing/ppconstr.cmi lib/pp.cmi \ + proofs/tacmach.cmi library/summary.cmi parsing/printer.cmi lib/pp.cmi \ library/nametab.cmi kernel/names.cmi library/nameops.cmi \ library/libnames.cmi tactics/hipattern.cmi library/global.cmi \ contrib/dp/fol.cmi pretyping/evd.cmi kernel/environ.cmi \ @@ -2500,7 +2492,7 @@ contrib/dp/dp.cmo: lib/util.cmi pretyping/typing.cmi pretyping/termops.cmi \ interp/coqlib.cmi contrib/dp/dp.cmi contrib/dp/dp.cmx: lib/util.cmx pretyping/typing.cmx pretyping/termops.cmx \ kernel/term.cmx tactics/tactics.cmx tactics/tacticals.cmx \ - proofs/tacmach.cmx library/summary.cmx parsing/ppconstr.cmx lib/pp.cmx \ + proofs/tacmach.cmx library/summary.cmx parsing/printer.cmx lib/pp.cmx \ library/nametab.cmx kernel/names.cmx library/nameops.cmx \ library/libnames.cmx tactics/hipattern.cmx library/global.cmx \ contrib/dp/fol.cmi pretyping/evd.cmx kernel/environ.cmx \ @@ -3242,25 +3234,25 @@ contrib/setoid_ring/newring.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ tactics/tacticals.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \ proofs/tacexpr.cmo library/summary.cmi tactics/setoid_replace.cmi \ pretyping/retyping.cmi proofs/refiner.cmi pretyping/rawterm.cmi \ - proofs/proof_type.cmi pretyping/pretyping.cmi parsing/pptactic.cmi \ - parsing/ppconstr.cmi lib/pp.cmi parsing/pcoq.cmi kernel/names.cmi \ - kernel/mod_subst.cmi library/libobject.cmi library/lib.cmi \ - parsing/lexer.cmi library/global.cmi interp/genarg.cmi pretyping/evd.cmi \ - kernel/esubst.cmi kernel/environ.cmi parsing/egrammar.cmi \ - interp/coqlib.cmi interp/constrintern.cmi kernel/closure.cmi \ - toplevel/cerrors.cmi + proofs/proof_type.cmi parsing/printer.cmi pretyping/pretyping.cmi \ + parsing/pptactic.cmi parsing/ppconstr.cmi lib/pp.cmi parsing/pcoq.cmi \ + kernel/names.cmi kernel/mod_subst.cmi library/libobject.cmi \ + library/lib.cmi parsing/lexer.cmi library/global.cmi interp/genarg.cmi \ + pretyping/evd.cmi kernel/esubst.cmi kernel/environ.cmi \ + parsing/egrammar.cmi interp/coqlib.cmi interp/constrintern.cmi \ + kernel/closure.cmi toplevel/cerrors.cmi contrib/setoid_ring/newring.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ pretyping/typing.cmx kernel/term.cmx tactics/tactics.cmx \ tactics/tacticals.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \ proofs/tacexpr.cmx library/summary.cmx tactics/setoid_replace.cmx \ pretyping/retyping.cmx proofs/refiner.cmx pretyping/rawterm.cmx \ - proofs/proof_type.cmx pretyping/pretyping.cmx parsing/pptactic.cmx \ - parsing/ppconstr.cmx lib/pp.cmx parsing/pcoq.cmx kernel/names.cmx \ - kernel/mod_subst.cmx library/libobject.cmx library/lib.cmx \ - parsing/lexer.cmx library/global.cmx interp/genarg.cmx pretyping/evd.cmx \ - kernel/esubst.cmx kernel/environ.cmx parsing/egrammar.cmx \ - interp/coqlib.cmx interp/constrintern.cmx kernel/closure.cmx \ - toplevel/cerrors.cmx + proofs/proof_type.cmx parsing/printer.cmx pretyping/pretyping.cmx \ + parsing/pptactic.cmx parsing/ppconstr.cmx lib/pp.cmx parsing/pcoq.cmx \ + kernel/names.cmx kernel/mod_subst.cmx library/libobject.cmx \ + library/lib.cmx parsing/lexer.cmx library/global.cmx interp/genarg.cmx \ + pretyping/evd.cmx kernel/esubst.cmx kernel/environ.cmx \ + parsing/egrammar.cmx interp/coqlib.cmx interp/constrintern.cmx \ + kernel/closure.cmx toplevel/cerrors.cmx contrib/subtac/eterm.cmo: pretyping/termops.cmi kernel/term.cmi \ tactics/tactics.cmi tactics/tacticals.cmi proofs/tacmach.cmi \ contrib/subtac/sutils.cmi kernel/reduction.cmi lib/pp.cmi \ @@ -3283,19 +3275,19 @@ contrib/subtac/g_eterm.cmx: lib/util.cmx proofs/tacmach.cmx \ parsing/egrammar.cmx toplevel/cerrors.cmx contrib/subtac/infer.cmo: lib/util.cmi toplevel/toplevel.cmi kernel/term.cmi \ contrib/subtac/scoq.cmo contrib/subtac/sast.cmo pretyping/rawterm.cmi \ - parsing/ppconstr.cmi lib/pp.cmi contrib/subtac/natural.cmo \ + parsing/printer.cmi lib/pp.cmi contrib/subtac/natural.cmo \ library/nametab.cmi kernel/names.cmi library/libnames.cmi \ pretyping/inductiveops.cmi kernel/inductive.cmi library/global.cmi \ kernel/declarations.cmi contrib/subtac/infer.cmi contrib/subtac/infer.cmx: lib/util.cmx toplevel/toplevel.cmx kernel/term.cmx \ contrib/subtac/scoq.cmx contrib/subtac/sast.cmx pretyping/rawterm.cmx \ - parsing/ppconstr.cmx lib/pp.cmx contrib/subtac/natural.cmx \ + parsing/printer.cmx lib/pp.cmx contrib/subtac/natural.cmx \ library/nametab.cmx kernel/names.cmx library/libnames.cmx \ pretyping/inductiveops.cmx kernel/inductive.cmx library/global.cmx \ kernel/declarations.cmx contrib/subtac/infer.cmi contrib/subtac/rewrite.cmo: lib/util.cmi kernel/univ.cmi pretyping/typing.cmi \ pretyping/termops.cmi kernel/term.cmi kernel/sign.cmi \ - contrib/subtac/scoq.cmo kernel/reduction.cmi parsing/ppconstr.cmi \ + contrib/subtac/scoq.cmo kernel/reduction.cmi parsing/printer.cmi \ lib/pp.cmi proofs/pfedit.cmi contrib/subtac/natural.cmo kernel/names.cmi \ library/libnames.cmi contrib/subtac/infer.cmi pretyping/inductiveops.cmi \ kernel/inductive.cmi library/global.cmi pretyping/evd.cmi \ @@ -3304,7 +3296,7 @@ contrib/subtac/rewrite.cmo: lib/util.cmi kernel/univ.cmi pretyping/typing.cmi \ contrib/subtac/rewrite.cmi contrib/subtac/rewrite.cmx: lib/util.cmx kernel/univ.cmx pretyping/typing.cmx \ pretyping/termops.cmx kernel/term.cmx kernel/sign.cmx \ - contrib/subtac/scoq.cmx kernel/reduction.cmx parsing/ppconstr.cmx \ + contrib/subtac/scoq.cmx kernel/reduction.cmx parsing/printer.cmx \ lib/pp.cmx proofs/pfedit.cmx contrib/subtac/natural.cmx kernel/names.cmx \ library/libnames.cmx contrib/subtac/infer.cmx pretyping/inductiveops.cmx \ kernel/inductive.cmx library/global.cmx pretyping/evd.cmx \ @@ -3475,6 +3467,8 @@ tools/coqdoc/pretty.cmo: tools/coqdoc/output.cmi tools/coqdoc/index.cmi \ tools/coqdoc/pretty.cmi tools/coqdoc/pretty.cmx: tools/coqdoc/output.cmx tools/coqdoc/index.cmx \ tools/coqdoc/pretty.cmi +tools/coqdoc/theory.cmo: tools/coqdoc/output.cmi +tools/coqdoc/theory.cmx: tools/coqdoc/output.cmx tactics/tauto.cmo: parsing/grammar.cma tactics/tauto.cmx: parsing/grammar.cma tactics/eqdecide.cmo: parsing/grammar.cma @@ -3576,102 +3570,74 @@ tools/coq_makefile.cmx: tools/coq-tex.cmo: tools/coq-tex.cmx: coq_fix_code.o: kernel/byterun/coq_fix_code.c \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/memory.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.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 \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/alloc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.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 \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/memory.h \ - kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.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 \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/alloc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.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 \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/memory.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 \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/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 \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/memory.h \ - kernel/byterun/coq_values.h /home/logical/local//lib/ocaml/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 \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/memory.h \ - kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.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 \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/alloc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.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 \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/memory.h \ - kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.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 \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/alloc.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.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 \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/memory.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 \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/compatibility.h \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/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 \ - /home/logical/local//lib/ocaml/caml/config.h \ - /home/logical/local//lib/ocaml/caml/fail.h \ - /home/logical/local//lib/ocaml/caml/mlvalues.h \ - /home/logical/local//lib/ocaml/caml/misc.h \ - /home/logical/local//lib/ocaml/caml/memory.h \ - kernel/byterun/coq_values.h /home/logical/local//lib/ocaml/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/correctness/ptactic.ml b/contrib/correctness/ptactic.ml index bd742b9df..5994fb38d 100644 --- a/contrib/correctness/ptactic.ml +++ b/contrib/correctness/ptactic.ml @@ -51,7 +51,7 @@ let coqast_of_prog p = (* 4a. traduction type *) let ty = Pmonad.trad_ml_type_c ren env c in - deb_print (Printer.prterm_env (Global.env())) ty; + deb_print (Printer.pr_lconstr_env (Global.env())) ty; (* 4b. traduction terme (terme intermédiaire de type cc_term) *) deb_mess @@ -65,12 +65,12 @@ let coqast_of_prog p = (fnl () ++ str"Pcic.constr_of_prog: Translation cc_term -> rawconstr..." ++ fnl ()); let r = Pcic.rawconstr_of_prog cc in - deb_print Printer.pr_rawterm r; + deb_print Printer.pr_lrawconstr r; (* 6. résolution implicites *) deb_mess (fnl () ++ str"Resolution implicits (? => Meta(n))..." ++ fnl ()); let oc = understand_gen_tcc Evd.empty (Global.env()) [] None r in - deb_print (Printer.prterm_env (Global.env())) (snd oc); + deb_print (Printer.pr_lconstr_env (Global.env())) (snd oc); p,oc,ty,v @@ -248,7 +248,7 @@ let correctness s p opttac = deb_mess (str"Pred.red_cci: Reduction..." ++ fnl ()); let oc = reduce_open_constr oc in deb_mess (str"AFTER REDUCTION:" ++ fnl ()); - deb_print (Printer.prterm_env (Global.env())) (snd oc); + deb_print (Printer.pr_lconstr_env (Global.env())) (snd oc); let tac = (tclTHEN (Extratactics.refine_tac oc) automatic) in let tac = match opttac with | None -> tac diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml index 45fdb75ec..29064578f 100644 --- a/contrib/correctness/putil.ml +++ b/contrib/correctness/putil.ml @@ -231,26 +231,26 @@ and c_of_constr c = open Pp open Util -let prterm x = Printer.prterm_env (Global.env()) x +let pr_lconstr x = Printer.pr_lconstr_env (Global.env()) x let pp_pre = function [] -> (mt ()) | l -> hov 0 (str"pre " ++ prlist_with_sep (fun () -> (spc ())) - (fun x -> prterm x.p_value) l) + (fun x -> pr_lconstr x.p_value) l) let pp_post = function None -> (mt ()) - | Some c -> hov 0 (str"post " ++ prterm c.a_value) + | Some c -> hov 0 (str"post " ++ pr_lconstr c.a_value) let rec pp_type_v = function Ref v -> hov 0 (pp_type_v v ++ spc () ++ str"ref") - | Array (cc,v) -> hov 0 (str"array " ++ prterm cc ++ str" of " ++ pp_type_v v) + | Array (cc,v) -> hov 0 (str"array " ++ pr_lconstr cc ++ str" of " ++ pp_type_v v) | Arrow (b,c) -> hov 0 (prlist_with_sep (fun () -> (mt ())) pp_binder b ++ pp_type_c c) - | TypePure c -> prterm c + | TypePure c -> pr_lconstr c and pp_type_c ((id,v),e,p,q) = hov 0 (str"returns " ++ pr_id id ++ str":" ++ pp_type_v v ++ spc () ++ @@ -297,7 +297,7 @@ let rec pp_cc_term = function | CC_case _ -> hov 0 (str"<Case: not yet implemented>") | CC_expr c -> - hov 0 (prterm c) + hov 0 (pr_lconstr c) | CC_hole c -> - (str"(?::" ++ prterm c ++ str")") + (str"(?::" ++ pr_lconstr c ++ str")") diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml index f25794e80..32b39b03d 100644 --- a/contrib/dp/dp.ml +++ b/contrib/dp/dp.ml @@ -172,7 +172,7 @@ let rec_names_for c = | Name id -> let c' = Names.make_con mp dp (label_of_id id) in ignore (Global.lookup_constant c'); - msgnl (Ppconstr.pr_term (mkConst c')); + msgnl (Printer.pr_constr (mkConst c')); c' | Anonymous -> raise Not_found) diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index f0a5489df..90a986385 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -44,7 +44,7 @@ let lookup env typ = with Not_found -> errorlabstrm "field" (str "No field is declared for type" ++ spc() ++ - Printer.prterm_env env typ) + Printer.pr_lconstr_env env typ) let _ = let init () = th_tab := Gmap.empty in diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml index 7dc01a461..0b371966b 100644 --- a/contrib/first-order/instances.ml +++ b/contrib/first-order/instances.ml @@ -121,7 +121,7 @@ let mk_open_instance id gl m t= let nid=(fresh_id avoid var_id gl) in (Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in let nt=it_mkLambda_or_LetIn revt (aux m []) in - let rawt=Detyping.detype (false,env) [] [] nt in + let rawt=Detyping.detype false [] [] nt in let rec raux n t= if n=0 then t else match t with diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml index f9ebafc2a..c1175a4d9 100644 --- a/contrib/first-order/sequent.ml +++ b/contrib/first-order/sequent.ml @@ -291,7 +291,7 @@ let print_cmap map= str "| " ++ Util.prlist Printer.pr_global l ++ str " : " ++ - Ppconstr.pr_constr xc ++ + Ppconstr.pr_constr_expr xc ++ cut () ++ s in msgnl (v 0 diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml index 064f279f0..2877c19db 100644 --- a/contrib/funind/tacinvutils.ml +++ b/contrib/funind/tacinvutils.ml @@ -21,9 +21,9 @@ open Reductionops (*s printing of constr -- debugging *) (* comment this line to see debug msgs *) -let msg x = () ;; let prterm c = str "" +let msg x = () ;; let pr_lconstr c = str "" (* uncomment this to see debugging *) -let prconstr c = msg (str" " ++ prterm c ++ str"\n") +let prconstr c = msg (str" " ++ pr_lconstr c ++ str"\n") let prlistconstr lc = List.iter prconstr lc let prstr s = msg(str s) @@ -31,7 +31,7 @@ let prchr () = msg (str" (ret) \n") let prNamedConstr s c = begin msg(str ""); - msg(str(s^"==>\n ") ++ prterm c ++ str "\n<==\n"); + msg(str(s^"==>\n ") ++ pr_lconstr c ++ str "\n<==\n"); msg(str ""); end diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index e79d14249..81e175232 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -280,12 +280,12 @@ let print_check judg = let value_ct_ast = (try translate_constr false (Global.env()) value with UserError(f,str) -> - raise(UserError(f,Printer.prterm value ++ + raise(UserError(f,Printer.pr_lconstr value ++ fnl () ++ str ))) in let type_ct_ast = (try translate_constr false (Global.env()) typ with UserError(f,str) -> - raise(UserError(f, Printer.prterm value ++ fnl() ++ str))) in + raise(UserError(f, Printer.pr_lconstr value ++ fnl() ++ str))) in ((ctf_SearchResults !global_request_id), (Some (P_pl (CT_premises_list @@ -557,7 +557,7 @@ let rec hyp_pattern_filter pat name a c = match kind_of_term c with | Prod(_, hyp, c2) -> (try -(* let _ = msgnl ((str "WHOLE ") ++ (Printer.prterm c)) in +(* let _ = msgnl ((str "WHOLE ") ++ (Printer.pr_lconstr c)) in let _ = msgnl ((str "PAT ") ++ (Printer.pr_pattern pat)) in *) if Matching.is_matching pat hyp then (msgnl (str "ok"); true) diff --git a/contrib/interface/showproof_ct.ml b/contrib/interface/showproof_ct.ml index f6ab47376..07ac73b6a 100644 --- a/contrib/interface/showproof_ct.ml +++ b/contrib/interface/showproof_ct.ml @@ -130,7 +130,7 @@ let rec sp_print x = | "\n" -> fnl () | "Retour chariot pour Show proof" -> fnl () |_ -> str s) - | CT_text_formula f -> prterm (Hashtbl.find ct_FORMULA_constr f) + | CT_text_formula f -> pr_lconstr (Hashtbl.find ct_FORMULA_constr f) | CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "to_prove"); CT_text_path (CT_signed_int_list p); CT_coerce_ID_to_TEXT (CT_ident "goal"); diff --git a/contrib/interface/translate.mli b/contrib/interface/translate.mli index 65d8331b2..9f25ce38a 100644 --- a/contrib/interface/translate.mli +++ b/contrib/interface/translate.mli @@ -6,6 +6,6 @@ open Term;; val translate_goal : goal -> ct_RULE;; (* The boolean argument indicates whether names from the environment should *) -(* be avoided (same interpretation as for prterm_env and ast_of_constr) *) +(* be avoided (same interpretation as for pr_lconstr_env and ast_of_constr) *) val translate_constr : bool -> env -> constr -> ct_FORMULA;; val translate_path : int list -> ct_SIGNED_INT_LIST;; diff --git a/contrib/jprover/jprover.ml4 b/contrib/jprover/jprover.ml4 index 467036e08..294943f7d 100644 --- a/contrib/jprover/jprover.ml4 +++ b/contrib/jprover/jprover.ml4 @@ -51,7 +51,7 @@ let mbreak s = Format.print_flush (); print_string ("-break at: "^s); let jp_error re = raise (JT.RefineError ("jprover", JT.StringError re)) (* print Coq constructor *) -let print_constr ct = Pp.ppnl (PR.prterm ct); Format.print_flush () +let print_constr ct = Pp.ppnl (PR.pr_lconstr ct); Format.print_flush () let rec print_constr_list = function | [] -> () diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 5d43b1686..8387b7f63 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -490,7 +490,7 @@ let context operation path (t : constr) = | ((P_TYPE :: p), LetIn (n,b,t,c)) -> (mkLetIn (n,b,loop i p t,c)) | (p, _) -> - ppnl (Printer.prterm t); + ppnl (Printer.pr_lconstr t); failwith ("abstract_path " ^ string_of_int(List.length p)) in loop 1 path t @@ -511,7 +511,7 @@ let occurence path (t : constr) = | ((P_TYPE :: p), Lambda (n,term,c)) -> loop p term | ((P_TYPE :: p), LetIn (n,b,term,c)) -> loop p term | (p, _) -> - ppnl (Printer.prterm t); + ppnl (Printer.pr_lconstr t); failwith ("occurence " ^ string_of_int(List.length p)) in loop path t @@ -1564,7 +1564,7 @@ let rec decidability gl t = | Kapp(Nat,[]) -> mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |]) | _ -> errorlabstrm "decidability" (str "Omega: Can't solve a goal with equality on " ++ - Printer.prterm typ) + Printer.pr_lconstr typ) end | Kapp(Zne,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zne, [| t1;t2 |]) | Kapp(Zle,[t1;t2]) -> mkApp (Lazy.force coq_dec_Zle, [| t1;t2 |]) diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 5448d1389..48e8763d5 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -287,7 +287,7 @@ let guess_theory a = with Not_found -> errorlabstrm "Ring" (str "No Declared Ring Theory for " ++ - prterm a ++ fnl () ++ + pr_lconstr a ++ fnl () ++ str "Use Add [Semi] Ring to declare it") (* Looks up an option *) @@ -325,7 +325,7 @@ let states_compatibility_for env plus mult opp morphs = let add_theory want_ring want_abstract want_setoid a aequiv asetth amorph aplus amult aone azero aopp aeq t cset = if theories_map_mem a then errorlabstrm "Add Semi Ring" (str "A (Semi-)(Setoid-)Ring Structure is already declared for " ++ - prterm a); + pr_lconstr a); let env = Global.env () in if (want_ring & want_setoid & ( not (implement_theory env t coq_Setoid_Ring_Theory diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml index 5a7e8afd5..c552da621 100644 --- a/contrib/romega/refl_omega.ml +++ b/contrib/romega/refl_omega.ml @@ -219,7 +219,7 @@ let print_env_reification env = [] -> Printf.printf " ===============================\n\n" | t :: l -> Printf.printf " (%c%02d) := " c i; - Pp.ppnl (Printer.prterm t); + Pp.ppnl (Printer.pr_lconstr t); Pp.flush_all (); loop c (succ i) l in print_newline (); diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index 2facb0dcb..0b0362a3b 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -31,6 +31,7 @@ open Ppconstr open Mod_subst open Tacinterp open Libobject +open Printer (****************************************************************************) (* Library linking *) @@ -346,18 +347,18 @@ let default_ring_equality is_semi (r,add,mul,opp,req) = let op_morph = op_morph r add mul opp req add_m.lem mul_m.lem opp_m.lem in msgnl - (str"Using setoid \""++pr_term rel.rel_aeq++str"\""++spc()++ - str"and morphisms \""++pr_term add_m.morphism_theory++ - str"\","++spc()++ str"\""++pr_term mul_m.morphism_theory++ - str"\""++spc()++str"and \""++pr_term opp_m.morphism_theory++ + (str"Using setoid \""++pr_constr rel.rel_aeq++str"\""++spc()++ + str"and morphisms \""++pr_constr add_m.morphism_theory++ + str"\","++spc()++ str"\""++pr_constr mul_m.morphism_theory++ + str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++ str"\""); op_morph) else (msgnl - (str"Using setoid \""++pr_term rel.rel_aeq++str"\"" ++ spc() ++ - str"and morphisms \""++pr_term add_m.morphism_theory++ + (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++ + str"and morphisms \""++pr_constr add_m.morphism_theory++ str"\""++spc()++str"and \""++ - pr_term mul_m.morphism_theory++str"\""); + pr_constr mul_m.morphism_theory++str"\""); op_smorph r add mul req add_m.lem mul_m.lem) in (setoid,op_morph) @@ -484,7 +485,7 @@ let ring gl = with Not_found -> errorlabstrm "ring" (str"cannot find a declared ring structure for equality"++ - spc()++str"\""++pr_term req++str"\"") in + spc()++str"\""++pr_constr req++str"\"") in let req = carg e.ring_req in let lemma1 = carg e.ring_lemma1 in let lemma2 = carg e.ring_lemma2 in @@ -503,7 +504,7 @@ let ring_rewrite rl = with Not_found -> errorlabstrm "ring" (str"cannot find a declared ring structure over"++ - spc()++str"\""++pr_term ty++str"\"") in + spc()++str"\""++pr_constr ty++str"\"") in let rl = List.fold_right (fun x l -> lapp coq_cons [|ty;x;l|]) rl (lapp coq_nil [|ty|]) in Tacinterp.eval_tactic diff --git a/contrib/subtac/infer.ml b/contrib/subtac/infer.ml index 987fbedda..d52d8edf5 100644 --- a/contrib/subtac/infer.ml +++ b/contrib/subtac/infer.ml @@ -6,7 +6,7 @@ open Util open Sast open Scoq open Pp -open Ppconstr +open Printer let ($) f g = fun x -> f (g x) @@ -385,7 +385,7 @@ let rec print_dterm' ctx = function ++ print_dterm_loc ctx t ++ str "," ++ print_dterm_loc ctx' t' ++ str ":" ++ print_dtype_loc ctx' tt' ++ str ")" - | DCoq (cstr, t) -> pr_term cstr + | DCoq (cstr, t) -> pr_constr cstr and print_dterm_loc ctx (_, x) = print_dterm' ctx x (*debug_msg 1 (str ":" ++ print_dtype_loc ctx (type_of_dterm ctx x))*) @@ -408,10 +408,10 @@ and print_dtype' ctx = function | DTTerm (t, tt, s) -> str "Term:(" ++ print_dterm_loc ctx t ++ str ")" | DTInd (n, t, i, s) -> str (string_of_id (snd n)) | DTCoq (c, t, s) -> - debug_msg 1 (str "Coq:(") ++ pr_term c ++ + debug_msg 1 (str "Coq:(") ++ pr_constr c ++ debug_msg 1 (str ":" ++ print_dtype_loc ctx t ++ str ")") | DTSort s -> - pr_term (mkSort (snd s)) + pr_constr (mkSort (snd s)) and print_dtype_loc ctx (_, t) = print_dtype' ctx t diff --git a/contrib/subtac/rewrite.ml b/contrib/subtac/rewrite.ml index b228be2a7..201f2d48b 100644 --- a/contrib/subtac/rewrite.ml +++ b/contrib/subtac/rewrite.ml @@ -7,7 +7,7 @@ open Term open Names open Scoq open Pp -open Ppconstr +open Printer open Util type recursion_info = { @@ -614,7 +614,7 @@ let subtac recursive id (s, t) = coqt, coqt', coqt', prog_info, [], [] in trace (str "Rewrite of coqtype done" ++ - str "coqtype' = " ++ pr_term coqtype'); + str "coqtype' = " ++ pr_constr coqtype'); let dterm, dtype = infer ctx t in trace (str "Inference done" ++ spc () ++ str "Infered term: " ++ print_dterm_loc ctx dterm ++ spc () ++ @@ -624,9 +624,9 @@ let subtac recursive id (s, t) = fst (rewrite_type prog_info coqctx dtype) in trace (str "Rewrite done" ++ spc () ++ - str "Inferred Coq term:" ++ pr_term dterm' ++ spc () ++ - str "Inferred Coq type:" ++ pr_term dtype' ++ spc () ++ - str "Rewritten Coq type:" ++ pr_term coqtype'); + str "Inferred Coq term:" ++ pr_constr dterm' ++ spc () ++ + str "Inferred Coq type:" ++ pr_constr dtype' ++ spc () ++ + str "Rewritten Coq type:" ++ pr_constr coqtype'); let coercespec = coerce prog_info coqctx dtype' coqtype' in trace (str "Specs coercion successfull"); let realt = app_opt coercespec dterm' in diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index caac70310..bac7ad7c6 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -388,7 +388,7 @@ try Acic.CicHash.find terms_to_types tt with _ -> (*CSC: Warning: it really happens, for example in Ring_theory!!! *) -Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.prterm tt)) ; assert false +Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.pr_lconstr tt)) ; assert false else (* We are already in an inner-type and Coscoy's double *) (* type inference algorithm has not been applied. *) @@ -402,9 +402,9 @@ Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-ty in (* Debugging only: print_endline "TERMINE:" ; flush stdout ; -Pp.ppnl (Printer.prterm tt) ; flush stdout ; +Pp.ppnl (Printer.pr_lconstr tt) ; flush stdout ; print_endline "TIPO:" ; flush stdout ; -Pp.ppnl (Printer.prterm synthesized) ; flush stdout ; +Pp.ppnl (Printer.pr_lconstr synthesized) ; flush stdout ; print_endline "ENVIRONMENT:" ; flush stdout ; Pp.ppnl (Printer.pr_context_of env) ; flush stdout ; print_endline "FINE_ENVIRONMENT" ; flush stdout ; diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml index 24676f186..518f6c115 100644 --- a/contrib/xml/doubleTypeInference.ml +++ b/contrib/xml/doubleTypeInference.ml @@ -40,13 +40,13 @@ let whd_betadeltaiotacprop env evar_map ty = Conv_oracle.set_opaque_const cprop; prerr_endline "###whd_betadeltaiotacprop:" ; let xxx = -(*Pp.msgerr (Printer.prterm_env env ty);*) +(*Pp.msgerr (Printer.pr_lconstr_env env ty);*) prerr_endline ""; (fst (Redexpr.reduction_of_red_expr red_exp)) env evar_map ty in prerr_endline "###FINE" ; (* -Pp.msgerr (Printer.prterm_env env xxx); +Pp.msgerr (Printer.pr_lconstr_env env xxx); *) prerr_endline ""; Conv_oracle.set_transparent_const cprop; @@ -258,7 +258,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types = in (*CSC: debugging stuff to be removed *) if Acic.CicHash.mem subterms_to_types cstr then - (Pp.ppnl (Pp.(++) (Pp.str "DUPLICATE INSERTION: ") (Printer.prterm cstr)) ; flush stdout ) ; + (Pp.ppnl (Pp.(++) (Pp.str "DUPLICATE INSERTION: ") (Printer.pr_lconstr cstr)) ; flush stdout ) ; Acic.CicHash.add subterms_to_types cstr types ; E.make_judge cstr res diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4 index 1de6a4325..578c1ed2f 100644 --- a/contrib/xml/proofTree2Xml.ml4 +++ b/contrib/xml/proofTree2Xml.ml4 @@ -67,9 +67,9 @@ Pp.ppnl (Pp.str "Problem during the conversion of constr into XML") ; Pp.ppnl (Pp.str "ENVIRONMENT:") ; Pp.ppnl (Printer.pr_context_of rel_env) ; Pp.ppnl (Pp.str "TERM:") ; -Pp.ppnl (Printer.prterm_env rel_env obj') ; +Pp.ppnl (Printer.pr_lconstr_env rel_env obj') ; Pp.ppnl (Pp.str "RAW-TERM:") ; -Pp.ppnl (Printer.prterm obj') ; +Pp.ppnl (Printer.pr_lconstr obj') ; Xml.xml_empty "MISSING TERM" [] (*; raise e*) *) ;; @@ -120,7 +120,7 @@ in with _ -> Pp.ppnl (Pp.(++) (Pp.str "The_generated_term_is_not_a_subterm_of_the_final_lambda_term") -(Printer.prterm constr)) ; +(Printer.pr_lconstr constr)) ; None in let rec aux node old_hyps = diff --git a/dev/base_include b/dev/base_include index 55e2c9286..cd837ab6a 100644 --- a/dev/base_include +++ b/dev/base_include @@ -17,16 +17,16 @@ #use "top_printers.ml";; #use "vm_printers.ml";; -#install_printer (* identifier *) prid;; -#install_printer (* label *) prlab;; -#install_printer prmsid;; -#install_printer prmbid;; -#install_printer prdir;; -#install_printer prmp;; -#install_printer (* section_path *) prsp;; -#install_printer (* qualid *) prqualid;; -#install_printer (* kernel_name *) prkn;; -#install_printer (* constant *) prcon;; +#install_printer (* identifier *) ppid;; +#install_printer (* label *) pplab;; +#install_printer (* mod_self_id *) ppmsid;; +#install_printer (* mod_bound_id *) ppmbid;; +#install_printer (* dir_path *) ppdir;; +#install_printer (* module_path *) ppmp;; +#install_printer (* section_path *) ppsp;; +#install_printer (* qualid *) ppqualid;; +#install_printer (* kernel_name *) ppkn;; +#install_printer (* constant *) ppcon;; #install_printer (* constr *) print_pure_constr;; #install_printer (* patch *) ppripos;; #install_printer (* values *) ppvalues;; @@ -1,35 +1,35 @@ load_printer "gramlib.cma" load_printer "printers.cma" -install_printer Top_printers.prid -install_printer Top_printers.prlab -install_printer Top_printers.prmsid -install_printer Top_printers.prmbid -install_printer Top_printers.prdir -install_printer Top_printers.prmp -install_printer Top_printers.prkn -install_printer Top_printers.prcon -install_printer Top_printers.prsp -install_printer Top_printers.prqualid +install_printer Top_printers.ppid +install_printer Top_printers.pplab +install_printer Top_printers.ppmsid +install_printer Top_printers.ppmbid +install_printer Top_printers.ppdir +install_printer Top_printers.ppmp +install_printer Top_printers.ppkn +install_printer Top_printers.ppcon +install_printer Top_printers.ppsp +install_printer Top_printers.ppqualid install_printer Top_printers.ppbigint install_printer Top_printers.pppattern -install_printer Top_printers.pprawterm +install_printer Top_printers.pprawconstr -install_printer Top_printers.ppterm -install_printer Top_printers.print_uni -install_printer Top_printers.pp_universes +install_printer Top_printers.ppconstr +install_printer Top_printers.ppuni +install_printer Top_printers.ppuniverses install_printer Top_printers.pptype -install_printer Top_printers.prj +install_printer Top_printers.ppj -install_printer Top_printers.prgoal -install_printer Top_printers.prsigmagoal +install_printer Top_printers.ppgoal +install_printer Top_printers.ppsigmagoal install_printer Top_printers.pproof -install_printer Top_printers.prevd -install_printer Top_printers.prclenv +install_printer Top_printers.ppevd +install_printer Top_printers.ppclenv install_printer Top_printers.pptac -install_printer Top_printers.pr_obj +install_printer Top_printers.ppobj install_printer Top_printers.pploc diff --git a/dev/include b/dev/include index d1b5a717b..563edd042 100644 --- a/dev/include +++ b/dev/include @@ -5,26 +5,26 @@ #use "base_include";; #install_printer (* pattern *) pppattern;; -#install_printer (* rawconstr *) pprawterm;; +#install_printer (* rawconstr *) pprawconstr;; -#install_printer (* constr *) ppterm;; -#install_printer (* constr_substituted *) ppsterm;; -#install_printer (* universe *) print_uni;; -#install_printer (* universes *) pp_universes;; -#install_printer (* type_judgement*) pptype;; -#install_printer (* judgement*) prj;; +#install_printer (* constr *) ppconstr;; +#install_printer (* constr_substituted *) ppsconstr;; +#install_printer (* universe *) ppuni;; +#install_printer (* universes *) ppuniverses;; +#install_printer (* type_judgement *) pptype;; +#install_printer (* judgement *) ppj;; -#install_printer (* goal *) prgoal;; -#install_printer (* sigma goal *) prsigmagoal;; +#install_printer (* goal *) ppgoal;; +#install_printer (* sigma goal *) ppsigmagoal;; #install_printer (* proof *) pproof;; -#install_printer (* evar_map *) prevm;; -#install_printer (* evar_defs *) prevd;; -#install_printer (* clenv *) prclenv;; +#install_printer (* evar_map *) ppevm;; +#install_printer (* evar_defs *) ppevd;; +#install_printer (* clenv *) ppclenv;; #install_printer (* env *) ppenv;; #install_printer (* tactic *) pptac;; -#install_printer (* object *) pr_obj;; -#install_printer (* global_reference *) prglobal;; +#install_printer (* object *) ppobj;; +#install_printer (* global_reference *) ppglobal;; #install_printer (* fconstr *) ppfconstr;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 4bf879e85..f4f17c1d7 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -29,31 +29,32 @@ open Evd let _ = Constrextern.print_evar_arguments := true (* name printers *) -let prid id = pp (pr_id id) -let prlab l = pp (pr_lab l) -let prmsid msid = pp (str (debug_string_of_msid msid)) -let prmbid mbid = pp (str (debug_string_of_mbid mbid)) -let prdir dir = pp (pr_dirpath dir) -let prmp mp = pp(str (string_of_mp mp)) -let prcon con = pp(pr_con con) -let prkn kn = pp(pr_kn kn) -let prsp sp = pp(pr_sp sp) -let prqualid qid = pp(pr_qualid qid) +let ppid id = pp (pr_id id) +let pplab l = pp (pr_lab l) +let ppmsid msid = pp (str (debug_string_of_msid msid)) +let ppmbid mbid = pp (str (debug_string_of_mbid mbid)) +let ppdir dir = pp (pr_dirpath dir) +let ppmp mp = pp(str (string_of_mp mp)) +let ppcon con = pp(pr_con con) +let ppkn kn = pp(pr_kn kn) +let ppsp sp = pp(pr_sp sp) +let ppqualid qid = pp(pr_qualid qid) (* term printers *) -let ppterm x = pp(Termops.print_constr x) -let ppsterm x = ppterm (Declarations.force x) -let ppterm_univ x = Constrextern.with_universes ppterm x -let pprawterm = (fun x -> pp(pr_rawterm x)) -let pppattern = (fun x -> pp(pr_pattern x)) -let pptype = (fun x -> pp(prtype x)) -let ppfconstr c = ppterm (Closure.term_of_fconstr c) +let ppconstr x = pp(Termops.print_constr x) +let ppterm = ppconstr +let ppsconstr x = ppconstr (Declarations.force x) +let ppconstr_univ x = Constrextern.with_universes ppconstr x +let pprawconstr = (fun x -> pp(pr_lrawconstr x)) +let pppattern = (fun x -> pp(pr_constr_pattern x)) +let pptype = (fun x -> pp(pr_ltype x)) +let ppfconstr c = ppconstr (Closure.term_of_fconstr c) let ppbigint n = pp (Bigint.pr_bigint n);; let pP s = pp (hov 0 s) -let safe_prglobal = function +let safe_pr_global = function | ConstRef kn -> pp (str "CONSTREF(" ++ pr_con kn ++ str ")") | IndRef (kn,i) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++ int i ++ str ")") @@ -61,23 +62,23 @@ let safe_prglobal = function int i ++ str "," ++ int j ++ str ")") | VarRef id -> pp (str "VARREF(" ++ pr_id id ++ str ")") -let prglobal x = try pp(pr_global x) with _ -> safe_prglobal x +let ppglobal x = try pp(pr_global x) with _ -> safe_pr_global x -let prconst (sp,j) = - pp (str"#" ++ pr_kn sp ++ str"=" ++ prterm j.uj_val) +let ppconst (sp,j) = + pp (str"#" ++ pr_kn sp ++ str"=" ++ pr_lconstr j.uj_val) -let prvar ((id,a)) = - pp (str"#" ++ pr_id id ++ str":" ++ prterm a) +let ppvar ((id,a)) = + pp (str"#" ++ pr_id id ++ str":" ++ pr_lconstr a) -let genprj f j = let (c,t) = f j in (c ++ str " : " ++ t) +let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t) -let prj j = pp (genprj prjudge j) +let ppj j = pp (genppj pr_ljudge j) (* proof printers *) -let prevm evd = pp(pr_evar_map evd) -let prevd evd = pp(pr_evar_defs evd) -let prclenv clenv = pp(pr_clenv clenv) -let prgoal g = pp(db_pr_goal g) +let ppevm evd = pp(pr_evar_map evd) +let ppevd evd = pp(pr_evar_defs evd) +let ppclenv clenv = pp(pr_clenv clenv) +let ppgoal g = pp(db_pr_goal g) let pr_gls gls = hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) @@ -88,14 +89,14 @@ let pr_glls glls = hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++ prlist_with_sep pr_fnl db_pr_goal (sig_it glls)) -let prsigmagoal g = pp(pr_goal (sig_it g)) +let ppsigmagoal g = pp(pr_goal (sig_it g)) let prgls gls = pp(pr_gls gls) let prglls glls = pp(pr_glls glls) let pproof p = pp(print_proof Evd.empty empty_named_context p) -let print_uni u = (pp (pr_uni u)) +let ppuni u = pp(pr_uni u) -let pp_universes u = pp (str"[" ++ pr_universes u ++ str"]") +let ppuniverses u = pp (str"[" ++ pr_universes u ++ str"]") let ppenv e = pp (str "[" ++ pr_named_context_of e ++ str "]" ++ spc() ++ @@ -103,7 +104,7 @@ let ppenv e = pp let pptac = (fun x -> pp(Pptactic.pr_glob_tactic (Global.env()) x)) -let pr_obj obj = Format.print_string (Libobject.object_tag obj) +let ppobj obj = Format.print_string (Libobject.object_tag obj) let cnt = ref 0 @@ -300,7 +301,7 @@ let print_pure_constr csr = print_string (Printexc.to_string e);print_flush (); raise e -let ppfconstr c = ppterm (Closure.term_of_fconstr c) +let ppfconstr c = ppconstr (Closure.term_of_fconstr c) let pploc x = let (l,r) = unloc x in print_string"(";print_int l;print_string",";print_int r;print_string")" diff --git a/ide/coq.ml b/ide/coq.ml index 0e208028c..a45a56dc4 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -249,7 +249,7 @@ type goal = hyp list * concl let prepare_hyp sigma env ((i,c,d) as a) = env, sigma, ((i,string_of_id i),c,d), - (msg (pr_var_decl env a), msg (prterm_env_at_top env d)) + (msg (pr_var_decl env a), msg (pr_lconstr_env_at_top env d)) let prepare_hyps sigma env = assert (rel_context env = []); @@ -263,7 +263,7 @@ let prepare_hyps sigma env = let prepare_goal sigma g = let env = evar_env g in (prepare_hyps sigma env, - (env, sigma, g.evar_concl, msg (prterm_env_at_top env g.evar_concl))) + (env, sigma, g.evar_concl, msg (pr_lconstr_env_at_top env g.evar_concl))) let get_current_goals () = let pfts = get_pftreestate () in diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 3ebfde29e..3707c0f9a 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -458,6 +458,9 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function with No_match -> extern_symbol_pattern allscopes vars t rules +let extern_cases_pattern vars p = + extern_cases_pattern_in_scope (None,Notation.current_scopes()) vars p + (**********************************************************************) (* Externalising applications *) @@ -839,15 +842,12 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function with No_match -> extern_symbol allscopes vars t rules -let extern_rawconstr vars c = +let extern_rawconstr vars c = extern false (None,Notation.current_scopes()) vars c let extern_rawtype vars c = extern_typ (None,Notation.current_scopes()) vars c -let extern_cases_pattern vars p = - extern_cases_pattern_in_scope (None,Notation.current_scopes()) vars p - (******************************************************************) (* Main translation function from constr -> constr_expr *) @@ -855,7 +855,7 @@ let loc = dummy_loc (* for constr and pattern, locations are lost *) let extern_constr_gen at_top scopt env t = let avoid = if at_top then ids_of_context env else [] in - let r = Detyping.detype (at_top,env) avoid (names_of_rel_context env) t in + let r = Detyping.detype at_top avoid (names_of_rel_context env) t in let vars = vars_of_env env in extern (not at_top) (scopt,Notation.current_scopes()) vars r @@ -867,16 +867,16 @@ let extern_constr at_top env t = let extern_type at_top env t = let avoid = if at_top then ids_of_context env else [] in - let r = Detyping.detype (at_top,env) avoid (names_of_rel_context env) t in + let r = Detyping.detype at_top avoid (names_of_rel_context env) t in extern_rawtype (vars_of_env env) r (******************************************************************) (* Main translation function from pattern -> constr_expr *) -let rec raw_of_pat tenv env = function +let rec raw_of_pat env = function | PRef ref -> RRef (loc,ref) | PVar id -> RVar (loc,id) - | PEvar (n,l) -> REvar (loc,n,Some (array_map_to_list (raw_of_pat tenv env) l)) + | PEvar (n,l) -> REvar (loc,n,Some (array_map_to_list (raw_of_pat env) l)) | PRel n -> let id = try match lookup_name_of_rel n env with | Name id -> id @@ -887,32 +887,35 @@ let rec raw_of_pat tenv env = function | PMeta None -> RHole (loc,Evd.InternalHole) | PMeta (Some n) -> RPatVar (loc,(false,n)) | PApp (f,args) -> - RApp (loc,raw_of_pat tenv env f,array_map_to_list (raw_of_pat tenv env) args) + RApp (loc,raw_of_pat env f,array_map_to_list (raw_of_pat env) args) | PSoApp (n,args) -> RApp (loc,RPatVar (loc,(true,n)), - List.map (raw_of_pat tenv env) args) + List.map (raw_of_pat env) args) | PProd (na,t,c) -> - RProd (loc,na,raw_of_pat tenv env t,raw_of_pat tenv (na::env) c) + RProd (loc,na,raw_of_pat env t,raw_of_pat (na::env) c) | PLetIn (na,t,c) -> - RLetIn (loc,na,raw_of_pat tenv env t, raw_of_pat tenv (na::env) c) + RLetIn (loc,na,raw_of_pat env t, raw_of_pat (na::env) c) | PLambda (na,t,c) -> - RLambda (loc,na,raw_of_pat tenv env t, raw_of_pat tenv (na::env) c) + RLambda (loc,na,raw_of_pat env t, raw_of_pat (na::env) c) | PCase ((_,cs),typopt,tm,[||]) -> if typopt <> None then failwith "TODO: PCase to RCases"; - RCases (loc,(*(option_app (raw_of_pat tenv env) typopt,*)None, - [raw_of_pat tenv env tm,(Anonymous,None)],[]) + RCases (loc,(*(option_app (raw_of_pat env) typopt,*)None, + [raw_of_pat env tm,(Anonymous,None)],[]) | PCase ((Some ind,cs),typopt,tm,bv) -> let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in - let k = (snd (lookup_mind_specif (Global.env()) ind)).Declarations.mind_nrealargs in - Detyping.detype_case false (raw_of_pat tenv env)(raw_of_eqn tenv env) + let mib,mip = lookup_mind_specif (Global.env()) ind in + let k = mip.Declarations.mind_nrealargs in + let nparams = mib.Declarations.mind_nparams in + let cstrnargs = mip.Declarations.mind_consnrealargs in + Detyping.detype_case false (raw_of_pat env)(raw_of_eqn env) (fun _ _ -> false (* lazy: don't try to display pattern with "if" *)) - tenv avoid ind cs typopt k tm bv + avoid (ind,cs,nparams,cstrnargs,k) typopt tm bv | PCase _ -> error "Unsupported case-analysis while printing pattern" - | PFix f -> Detyping.detype (false,tenv) [] env (mkFix f) - | PCoFix c -> Detyping.detype (false,tenv) [] env (mkCoFix c) + | PFix f -> Detyping.detype false [] env (mkFix f) + | PCoFix c -> Detyping.detype false [] env (mkCoFix c) | PSort s -> RSort (loc,s) -and raw_of_eqn tenv env constr construct_nargs branch = +and raw_of_eqn env constr construct_nargs branch = let make_pat x env b ids = let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in let id = next_name_away_with_default "x" x avoid in @@ -922,7 +925,7 @@ and raw_of_eqn tenv env constr construct_nargs branch = if n=0 then (dummy_loc, ids, [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)], - raw_of_pat tenv env b) + raw_of_pat env b) else match b with | PLambda (x,_,b) -> @@ -938,6 +941,6 @@ and raw_of_eqn tenv env constr construct_nargs branch = in buildrec [] [] env construct_nargs branch -let extern_pattern tenv env pat = +let extern_constr_pattern env pat = extern true (None,Notation.current_scopes()) Idset.empty - (raw_of_pat tenv env pat) + (raw_of_pat env pat) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index e97d778c3..37f7369ad 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -32,7 +32,7 @@ val check_same_type : constr_expr -> constr_expr -> unit val extern_cases_pattern : Idset.t -> cases_pattern -> cases_pattern_expr val extern_rawconstr : Idset.t -> rawconstr -> constr_expr val extern_rawtype : Idset.t -> rawconstr -> constr_expr -val extern_pattern : env -> names_context -> constr_pattern -> constr_expr +val extern_constr_pattern : names_context -> constr_pattern -> constr_expr (* If [b=true] in [extern_constr b env c] then the variables in the first level of quantification clashing with the variables in [env] are renamed *) diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 771c5716b..da67c9f3f 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -247,7 +247,7 @@ let aconstr_of_rawconstr vars a = a let aconstr_of_constr avoiding t = - aconstr_of_rawconstr [] (Detyping.detype (false,Global.env()) avoiding [] t) + aconstr_of_rawconstr [] (Detyping.detype false avoiding [] t) let rec subst_aconstr subst bound raw = match raw with @@ -630,6 +630,20 @@ let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,a],b) let mkLetInC (id,a,b) = CLetIn (dummy_loc,id,a,b) let mkProdC (idl,a,b) = CProdN (dummy_loc,[idl,a],b) +let rec abstract_constr_expr c = function + | [] -> c + | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl) + | LocalRawAssum (idl,t)::bl -> + List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl + (abstract_constr_expr c bl) + +let rec prod_constr_expr c = function + | [] -> c + | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl) + | LocalRawAssum (idl,t)::bl -> + List.fold_right (fun x b -> mkProdC([x],t,b)) idl + (prod_constr_expr c bl) + let coerce_to_id = function | CRef (Ident (loc,id)) -> (loc,id) | a -> user_err_loc diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 5b9d69cd6..d6f7dbd03 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -144,6 +144,9 @@ val mkProdC : name located list * constr_expr * constr_expr -> constr_expr val coerce_to_id : constr_expr -> identifier located +val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr +val prod_constr_expr : constr_expr -> local_binder list -> constr_expr + (* For binders parsing *) (* Includes let binders *) diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 2f2f0773b..5a969490d 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -20,6 +20,8 @@ open Topconstr open Term open Pattern open Rawterm +open Constrextern +open Termops (*i*) let sep_p = fun _ -> str"." @@ -124,6 +126,10 @@ let pr_sort = function | RProp Term.Pos -> str "Set" | RType u -> str "Type" ++ pr_opt pr_universe u +let pr_id = pr_id +let pr_name = pr_name +let pr_qualid = pr_qualid + let pr_expl_args pr (a,expl) = match expl with | None -> pr (lapp,L) a @@ -140,12 +146,6 @@ let pr_opt_type_spc pr = function | CHole _ -> mt () | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t -let pr_id = pr_id - -let pr_name = function - | Anonymous -> str"_" - | Name id -> pr_id id - let pr_lident (b,_ as loc,id) = if loc <> dummy_loc then let (b,_) = unloc loc in @@ -263,8 +263,6 @@ let rec extract_lam_binders = function LocalRawAssum (nal,t) :: bl, c | c -> [], c -let pr_global vars ref = pr_global_env vars ref - let split_lambda = function | CLambdaN (loc,[[na],t],c) -> (na,t,c) | CLambdaN (loc,([na],t)::bl,c) -> (na,t,CLambdaN(loc,bl,c)) @@ -588,20 +586,6 @@ and pr_dangling_with_for sep inherited a = let pr = pr mt -let rec abstract_constr_expr c = function - | [] -> c - | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl) - | LocalRawAssum (idl,t)::bl -> - List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl - (abstract_constr_expr c bl) - -let rec prod_constr_expr c = function - | [] -> c - | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl) - | LocalRawAssum (idl,t)::bl -> - List.fold_right (fun x b -> mkProdC([x],t,b)) idl - (prod_constr_expr c bl) - let rec strip_context n iscast t = if n = 0 then [], if iscast then match t with CCast (_,c,_,_) -> c | _ -> t else t @@ -631,34 +615,15 @@ let rec strip_context n iscast t = | CLetIn (_,na,b,c) -> let bl', c = strip_context (n-1) iscast c in LocalRawDef (na,b) :: bl', c - | _ -> anomaly "ppconstrnew: strip_context" + | _ -> anomaly "strip_context" -let pr_constr_env env c = pr lsimple c -let pr_lconstr_env env c = pr ltop c -let pr_constr c = pr_constr_env (Global.env()) c -let pr_lconstr c = pr_lconstr_env (Global.env()) c +let pr_constr_expr c = pr lsimple c +let pr_lconstr_expr c = pr ltop c +let pr_pattern_expr c = pr lsimple c +let pr_cases_pattern_expr = pr_patt ltop let pr_binders = pr_undelimited_binders (pr ltop) -let pr_lconstr_env_n env iscast bl c = bl, pr ltop c -let pr_type c = pr ltop c - -let transf_pattern env c = - if Options.do_translate() then - Constrextern.extern_rawconstr (Termops.vars_of_env env) - (Constrintern.for_grammar - (Constrintern.intern_gen false ~allow_soapp:true Evd.empty env) c) - else c - -let pr_pattern c = pr lsimple (transf_pattern (Global.env()) c) - -let pr_rawconstr_env env c = - pr_constr (Constrextern.extern_rawconstr (Termops.vars_of_env env) c) -let pr_lrawconstr_env env c = - pr_lconstr (Constrextern.extern_rawconstr (Termops.vars_of_env env) c) - -let pr_cases_pattern = pr_patt ltop - let pr_pattern_occ prc = function ([],c) -> prc c | (nl,c) -> hov 1 (prc c ++ spc() ++ str"at " ++ @@ -669,10 +634,6 @@ let pr_unfold_occ pr_ref = function | (nl,qid) -> hov 1 (pr_ref qid ++ spc() ++ str"at " ++ hov 0 (prlist_with_sep spc int nl)) -let pr_qualid qid = str (string_of_qualid qid) - -let pr_arg pr x = spc () ++ pr x - let pr_red_flag pr r = (if r.rBeta then pr_arg str "beta" else mt ()) ++ (if r.rIota then pr_arg str "iota" else mt ()) ++ @@ -726,17 +687,3 @@ let rec pr_may_eval test prc prlc pr2 = function | ConstrTerm c -> prc c let pr_may_eval a = pr_may_eval (fun _ -> false) a - -(** constr printers *) - -let pr_term_env env c = pr lsimple (Constrextern.extern_constr false env c) -let pr_lterm_env env c = pr ltop (Constrextern.extern_constr false env c) -let pr_term c = pr_term_env (Global.env()) c -let pr_lterm c = pr_lterm_env (Global.env()) c - -let pr_constr_pattern_env env c = - pr lsimple (Constrextern.extern_pattern env Termops.empty_names_context c) - -let pr_constr_pattern t = - pr lsimple - (Constrextern.extern_pattern (Global.env()) Termops.empty_names_context t) diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index e6af0e369..51fbfcb26 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -30,15 +30,17 @@ val extract_def_binders : val split_fix : int -> constr_expr -> constr_expr -> local_binder list * constr_expr * constr_expr -val pr_binders : local_binder list -> std_ppcmds val prec_less : int -> int * Ppextend.parenRelation -> bool -val pr_global : Idset.t -> global_reference -> std_ppcmds - val pr_tight_coma : unit -> std_ppcmds + val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds +val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds +val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds +val pr_metaid : identifier -> std_ppcmds + val pr_lident : identifier located -> std_ppcmds val pr_lname : name located -> std_ppcmds @@ -48,40 +50,22 @@ val pr_sep_com : (unit -> std_ppcmds) -> (constr_expr -> std_ppcmds) -> constr_expr -> std_ppcmds -val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds + val pr_id : identifier -> std_ppcmds val pr_name : name -> std_ppcmds val pr_qualid : qualid -> std_ppcmds -val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds -val pr_metaid : identifier -> std_ppcmds + val pr_red_expr : ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) -> ('a,'b) red_expr_gen -> std_ppcmds - -val pr_sort : rawsort -> std_ppcmds -val pr_pattern : Tacexpr.pattern_expr -> std_ppcmds -val pr_constr : constr_expr -> std_ppcmds -val pr_lconstr : constr_expr -> std_ppcmds -val pr_constr_env : env -> constr_expr -> std_ppcmds -val pr_lconstr_env : env -> constr_expr -> std_ppcmds -val pr_type : constr_expr -> std_ppcmds -val pr_cases_pattern : cases_pattern_expr -> std_ppcmds val pr_may_eval : - ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('a,'b) may_eval - -> std_ppcmds -val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr -val prod_constr_expr : constr_expr -> local_binder list -> constr_expr - + ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> + ('a,'b) may_eval -> std_ppcmds -val pr_rawconstr_env : env -> rawconstr -> std_ppcmds -val pr_lrawconstr_env : env -> rawconstr -> std_ppcmds - -(** constr printers *) - -val pr_term_env : env -> constr -> std_ppcmds -val pr_lterm_env : env -> constr -> std_ppcmds -val pr_term : constr -> std_ppcmds -val pr_lterm : constr -> std_ppcmds +val pr_sort : rawsort -> std_ppcmds -val pr_constr_pattern_env : env -> Pattern.constr_pattern -> std_ppcmds -val pr_constr_pattern : Pattern.constr_pattern -> std_ppcmds +val pr_binders : local_binder list -> std_ppcmds +val pr_pattern_expr : Tacexpr.pattern_expr -> std_ppcmds +val pr_constr_expr : constr_expr -> std_ppcmds +val pr_lconstr_expr : constr_expr -> std_ppcmds +val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 8476ccf2a..c2029dde5 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -20,6 +20,7 @@ open Libnames open Pattern open Ppextend open Ppconstr +open Printer let pr_global x = Nametab.pr_global_env Idset.empty x @@ -919,9 +920,9 @@ let drop_env f _env = f let rec raw_printers = (pr_raw_tactic_level, - drop_env pr_constr, - drop_env pr_lconstr, - pr_pattern, + drop_env pr_constr_expr, + drop_env pr_lconstr_expr, + pr_pattern_expr, drop_env pr_reference, drop_env pr_reference, pr_reference, @@ -958,8 +959,8 @@ and pr_glob_match_rule env t = let ((pr_tactic_level:Environ.env -> tolerability -> Proof_type.tactic_expr -> std_ppcmds),_) = make_pr_tac (pr_glob_tactic_level, - pr_term_env, - pr_lterm_env, + pr_constr_env, + pr_lconstr_env, pr_constr_pattern, pr_evaluable_reference_env, pr_inductive, @@ -976,10 +977,8 @@ let _ = Tactic_debug.set_tactic_printer (fun x -> pr_glob_tactic (Global.env()) x) let _ = Tactic_debug.set_match_pattern_printer - (fun env hyp -> - pr_match_pattern - (Printer.pr_pattern_env env (Termops.names_of_rel_context env)) hyp) + (fun env hyp -> pr_match_pattern (pr_constr_pattern_env env) hyp) let _ = Tactic_debug.set_match_rule_printer (fun rl -> - pr_match_rule false (pr_glob_tactic (Global.env())) Printer.pr_pattern rl) + pr_match_rule false (pr_glob_tactic (Global.env())) pr_constr_pattern rl) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 41c391802..2444b1be9 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -26,7 +26,7 @@ open Topconstr open Decl_kinds open Tacinterp -let pr_spc_type = pr_sep_com spc pr_type +let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr let pr_lident (b,_ as loc,id) = if loc <> dummy_loc then @@ -65,8 +65,8 @@ let pr_raw_tactic_env l env t = let pr_gen env t = pr_raw_generic - pr_constr - pr_lconstr + pr_constr_expr + pr_lconstr_expr (pr_raw_tactic_level env) pr_reference t let pr_raw_tactic tac = pr_raw_tactic (Global.env()) tac @@ -507,11 +507,11 @@ let rec pr_vernac = function | DefineBody (bl,red,body,d) -> let ty = match d with | None -> mt() - | Some ty -> spc() ++ str":" ++ pr_sep_com spc pr_lconstr ty + | Some ty -> spc() ++ str":" ++ pr_spc_lconstr ty in (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body)) | ProveBody (bl,t) -> - (pr_binders_arg bl, str" :" ++ pr_spc_type t, None) in + (pr_binders_arg bl, str" :" ++ pr_spc_lconstr t, None) in let (binds,typ,c) = pr_def_body b in hov 2 (pr_def_token d ++ spc() ++ pr_lident id ++ binds ++ typ ++ (match c with @@ -523,7 +523,7 @@ let rec pr_vernac = function (match bl with | [] -> mt() | _ -> pr_binders bl ++ spc()) - ++ str":" ++ pr_spc_type c) + ++ str":" ++ pr_spc_lconstr c) | VernacEndProof Admitted -> str"Admitted" | VernacEndProof (Proved (opac,o)) -> (match o with | None -> if opac then str"Qed" else str"Defined" @@ -536,13 +536,13 @@ let rec pr_vernac = function let n = List.length (List.flatten (List.map fst (List.map snd l))) in hov 2 (pr_assumption_token (n > 1) stre ++ spc() ++ - pr_ne_params_list pr_type l) + pr_ne_params_list pr_lconstr_expr l) | VernacInductive (f,l) -> let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ (if coe then str":>" else str":") ++ - pr_sep_com spc pr_type c) in + pr_spc_lconstr c) in let pr_constructor_list l = match l with | [] -> mt() | _ -> @@ -554,7 +554,7 @@ let rec pr_vernac = function hov 0 ( str key ++ spc() ++ pr_lident id ++ pr_and_type_binders_arg indpar ++ spc() ++ str":" ++ - spc() ++ pr_type s ++ + spc() ++ pr_lconstr_expr s ++ str" :=") ++ pr_constructor_list lc ++ pr_decl_notation pr_constr ntn in @@ -584,7 +584,7 @@ let rec pr_vernac = function spc() ++ str "{struct " ++ pr_name name ++ str"}" else mt() in pr_id id ++ pr_binders_arg bl ++ annot ++ spc() - ++ pr_type_option (fun c -> spc() ++ pr_type c) type_ + ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_ ++ str" :=" ++ brk(1,1) ++ pr_lconstr def ++ pr_decl_notation pr_constr ntn in @@ -599,7 +599,7 @@ let rec pr_vernac = function else ([],def,c) in let bl = bl @ bl' in pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++ - spc() ++ pr_type c ++ + spc() ++ pr_lconstr_expr c ++ str" :=" ++ brk(1,1) ++ pr_lconstr def in let start = if b then "Boxed CoFixpoint" else "CoFixpoint" in hov 1 (str start ++ spc() ++ @@ -614,20 +614,20 @@ let rec pr_vernac = function | (oc,AssumExpr (id,t)) -> hov 1 (pr_lname id ++ (if oc then str" :>" else str" :") ++ spc() ++ - pr_type t) + pr_lconstr_expr t) | (oc,DefExpr(id,b,opt)) -> (match opt with | Some t -> hov 1 (pr_lname id ++ (if oc then str" :>" else str" :") ++ spc() ++ - pr_type t ++ str" :=" ++ pr_lconstr b) + pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b) | None -> hov 1 (pr_lname id ++ str" :=" ++ spc() ++ pr_lconstr b)) in hov 2 (str (if b then "Record" else "Structure") ++ (if oc then str" > " else str" ") ++ pr_lident name ++ - pr_and_type_binders_arg ps ++ str" :" ++ spc() ++ pr_type s ++ - str" := " ++ + pr_and_type_binders_arg ps ++ str" :" ++ spc() ++ + pr_lconstr_expr s ++ str" := " ++ (match c with | None -> mt() | Some sc -> pr_lident sc) ++ @@ -732,7 +732,7 @@ let rec pr_vernac = function (* Rec by default *) str "Ltac ") ++ prlist_with_sep (fun () -> fnl() ++ str"with ") pr_tac_body l) | VernacHints (local,dbnames,h) -> - pr_hints local dbnames h pr_constr pr_pattern + pr_hints local dbnames h pr_constr pr_pattern_expr | VernacSyntacticDefinition (id,c,local,onlyparsing) -> hov 2 (str"Notation " ++ pr_locality local ++ pr_id id ++ str" :=" ++ @@ -749,7 +749,8 @@ let rec pr_vernac = function | VernacReserve (idl,c) -> hov 1 (str"Implicit Type" ++ str (if List.length idl > 1 then "s " else " ") ++ - prlist_with_sep spc pr_lident idl ++ str " :" ++ spc () ++ pr_type c) + prlist_with_sep spc pr_lident idl ++ str " :" ++ spc () ++ + pr_lconstr c) | VernacSetOpacity (fl,l) -> hov 1 ((if fl then str"Opaque" else str"Transparent") ++ spc() ++ prlist_with_sep sep pr_reference l) @@ -808,7 +809,7 @@ let rec pr_vernac = function | PrintAbout qid -> str"About" ++ spc() ++ pr_reference qid | PrintImplicit qid -> str"Print Implicit" ++ spc() ++ pr_reference qid in pr_printable p - | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_pattern + | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_pattern_expr | VernacLocate loc -> let pr_locate =function | LocateTerm qid -> pr_reference qid @@ -852,4 +853,4 @@ and pr_extend s cl = in pr_vernac -let pr_vernac v = make_pr_vernac pr_constr pr_lconstr v ++ sep_end () +let pr_vernac v = make_pr_vernac pr_constr_expr pr_lconstr_expr v ++ sep_end () diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 821679b4f..1bd110926 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -70,7 +70,7 @@ let print_ref reduce ref = let ctx,ccl = Reductionops.splay_prod_assum (Global.env()) Evd.empty typ in it_mkProd_or_LetIn ccl ctx else typ in - hov 0 (pr_global ref ++ str " :" ++ spc () ++ prtype typ) ++ fnl () + hov 0 (pr_global ref ++ str " :" ++ spc () ++ pr_ltype typ) ++ fnl () let print_argument_scopes = function | [Some sc] -> str"Argument scope is [" ++ str sc ++ str"]" ++ fnl() @@ -225,8 +225,8 @@ let print_located_qualid ref = (**** Printing declarations and judgments *) let print_typed_value_in_env env (trm,typ) = - (prterm_env env trm ++ fnl () ++ - str " : " ++ prtype_env env typ ++ fnl ()) + (pr_lconstr_env env trm ++ fnl () ++ + str " : " ++ pr_ltype_env env typ ++ fnl ()) let print_typed_value x = print_typed_value_in_env (Global.env ()) x @@ -239,20 +239,20 @@ let print_safe_judgment env j = print_typed_value_in_env env (trm, typ) (* To be improved; the type should be used to provide the types in the - abstractions. This should be done recursively inside prterm, so that + abstractions. This should be done recursively inside pr_lconstr, so that the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u) synthesizes the type nat of the abstraction on u *) let print_named_def name body typ = - let pbody = prterm body in - let ptyp = prtype typ in + let pbody = pr_lconstr body in + let ptyp = pr_ltype typ in (str "*** [" ++ str name ++ str " " ++ hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++ str ":" ++ brk (1,2) ++ ptyp) ++ str "]" ++ fnl ()) let print_named_assum name typ = - (str "*** [" ++ str name ++ str " : " ++ prtype typ ++ str "]" ++ fnl ()) + (str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]" ++ fnl ()) let print_named_decl (id,c,typ) = let s = string_of_id id in @@ -272,7 +272,7 @@ let print_params env params = let print_constructors envpar names types = let pc = prlist_with_sep (fun () -> brk(1,0) ++ str "| ") - (fun (id,c) -> pr_id id ++ str " : " ++ prterm_env envpar c) + (fun (id,c) -> pr_id id ++ str " : " ++ pr_lconstr_env envpar c) (Array.to_list (array_map2 (fun n t -> (n,t)) names types)) in hv 0 (str " " ++ pc) @@ -295,7 +295,7 @@ let print_one_inductive (sp,tyi) = let envpar = push_rel_context params env in hov 0 ( pr_global (IndRef (sp,tyi)) ++ brk(1,4) ++ print_params env params ++ - str ": " ++ prterm_env envpar arity ++ str " :=") ++ + str ": " ++ pr_lconstr_env envpar arity ++ str " :=") ++ brk(0,2) ++ print_constructors envpar cstrnames cstrtypes let pr_mutual_inductive finite indl = @@ -319,11 +319,11 @@ let print_section_variable sp = print_name_infos (VarRef sp) let print_body = function - | Some lc -> prterm (Declarations.force lc) + | Some lc -> pr_lconstr (Declarations.force lc) | None -> (str"<no body>") let print_typed_body (val_0,typ) = - (print_body val_0 ++ fnl () ++ str " : " ++ prtype typ ++ fnl ()) + (print_body val_0 ++ fnl () ++ str " : " ++ pr_ltype typ ++ fnl ()) let print_constant with_values sep sp = let cb = Global.lookup_constant sp in @@ -333,11 +333,11 @@ let print_constant with_values sep sp = match val_0 with | None -> str"*** [ " ++ - print_basename sp ++ str " : " ++ cut () ++ prtype typ ++ + print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ fnl () | _ -> print_basename sp ++ str sep ++ cut () ++ - (if with_values then print_typed_body (val_0,typ) else prtype typ) ++ + (if with_values then print_typed_body (val_0,typ) else pr_ltype typ) ++ fnl ()) let print_constant_with_infos sp = @@ -349,7 +349,7 @@ let print_syntactic_def sep kn = let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn in let c = Syntax_def.search_syntactic_definition dummy_loc kn in str "Notation " ++ pr_qualid qid ++ str sep ++ - Constrextern.without_symbols pr_rawterm c ++ fnl () + Constrextern.without_symbols pr_lrawconstr c ++ fnl () let print_leaf_entry with_values sep ((sp,kn as oname),lobj) = let tag = object_tag lobj in @@ -545,7 +545,7 @@ let inspect depth = open Classops -let print_coercion_value v = prterm (get_coercion_value v) +let print_coercion_value v = pr_lconstr (get_coercion_value v) let print_class i = let cl,_ = class_info_from_index i in @@ -588,7 +588,7 @@ let print_path_between cls clt = let print_canonical_projections () = prlist_with_sep pr_fnl (fun ((r1,r2),o) -> - pr_global r2 ++ str " <- " ++ pr_global r1 ++ str " ( " ++ prterm o.o_DEF ++ str " )") + pr_global r2 ++ str " <- " ++ pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )") (canonical_projections ()) (*************************************************************************) diff --git a/parsing/printer.ml b/parsing/printer.ml index 7efea20a8..782cd3b4a 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -26,65 +26,98 @@ open Proof_type open Refiner open Pfedit open Ppconstr +open Constrextern let emacs_str s = if !Options.print_emacs then s else "" (**********************************************************************) -(* Generic printing: choose old or new printers *) +(** Terms *) + + (* [at_top] means ids of env must be avoided in bound variables *) +let pr_constr_core at_top env t = + pr_constr_expr (extern_constr at_top env t) +let pr_lconstr_core at_top env t = + pr_lconstr_expr (extern_constr at_top env t) + +let pr_lconstr_env_at_top env = pr_lconstr_core true env +let pr_lconstr_env env = pr_lconstr_core false env +let pr_constr_env env = pr_constr_core false env + + (* NB do not remove the eta-redexes! Global.env() has side-effects... *) +let pr_lconstr t = pr_lconstr_env (Global.env()) t +let pr_constr t = pr_constr_env (Global.env()) t + +let pr_type_core at_top env t = + pr_constr_expr (extern_type at_top env t) +let pr_ltype_core at_top env t = + pr_lconstr_expr (extern_type at_top env t) + +let pr_ltype_env_at_top env = pr_ltype_core true env +let pr_ltype_env env = pr_ltype_core false env +let pr_type_env env = pr_type_core false env + +let pr_ltype t = pr_ltype_env (Global.env()) t +let pr_type t = pr_type_env (Global.env()) t + +let pr_ljudge_env env j = + (pr_lconstr_env env j.uj_val, pr_lconstr_env env j.uj_type) + +let pr_ljudge j = pr_ljudge_env (Global.env()) j + +let pr_lrawconstr_env env c = + pr_lconstr_expr (extern_rawconstr (vars_of_env env) c) +let pr_rawconstr_env env c = + pr_constr_expr (extern_rawconstr (vars_of_env env) c) + +let pr_lrawconstr c = + pr_lconstr_expr (extern_rawconstr Idset.empty c) +let pr_rawconstr c = + pr_constr_expr (extern_rawconstr Idset.empty c) -(* [at_top] means ids of env must be avoided in bound variables *) -let prterm_core at_top env t = - pr_lconstr (Constrextern.extern_constr at_top env t) -let prtype_core at_top env t = - pr_lconstr (Constrextern.extern_type at_top env t) let pr_cases_pattern t = - pr_cases_pattern (Constrextern.extern_cases_pattern Idset.empty t) -let pr_pattern_env tenv env t = - pr_constr (Constrextern.extern_pattern tenv env t) + pr_cases_pattern_expr (extern_cases_pattern Idset.empty t) + +let pr_constr_pattern_env env c = + pr_constr_expr (extern_constr_pattern (names_of_rel_context env) c) +let pr_constr_pattern t = + pr_constr_expr (extern_constr_pattern empty_names_context t) + +let _ = Termops.set_print_constr pr_lconstr_env (**********************************************************************) -(* Derived printers *) - -let prterm_env_at_top env = prterm_core true env -let prterm_env env = prterm_core false env -let prtype_env_at_top env = prtype_core true env -let prtype_env env = prtype_core false env -let prjudge_env env j = - (prterm_env env j.uj_val, prterm_env env j.uj_type) - -(* NB do not remove the eta-redexes! Global.env() has side-effects... *) -let prterm t = prterm_env (Global.env()) t -let prtype t = prtype_env (Global.env()) t -let prjudge j = prjudge_env (Global.env()) j - -let _ = Termops.set_print_constr prterm_env - -let pr_constant env cst = prterm_env env (mkConst cst) -let pr_existential env ev = prterm_env env (mkEvar ev) -let pr_inductive env ind = prterm_env env (mkInd ind) -let pr_constructor env cstr = prterm_env env (mkConstruct cstr) +(* Global references *) + +let pr_global_env env ref = + (* Il est important de laisser le let-in, car les streams s'évaluent + paresseusement : il faut forcer l'évaluation pour capturer + l'éventuelle levée d'une exception (cela arrive dans le debugger) *) + let s = string_of_qualid (shortest_qualid_of_global env ref) in + (str s) + let pr_global = pr_global_env Idset.empty + +let pr_constant env cst = pr_global_env (vars_of_env env) (ConstRef cst) +let pr_existential env ev = pr_lconstr_env env (mkEvar ev) +let pr_inductive env ind = pr_lconstr_env env (mkInd ind) +let pr_constructor env cstr = pr_lconstr_env env (mkConstruct cstr) + let pr_evaluable_reference ref = let ref' = match ref with | EvalConstRef const -> ConstRef const | EvalVarRef sp -> VarRef sp in pr_global ref' -let pr_rawterm t = - pr_lconstr (Constrextern.extern_rawconstr Idset.empty t) - -open Pattern - -let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t +(**********************************************************************) +(* Contexts and declarations *) let pr_var_decl env (id,c,typ) = let pbody = match c with | None -> (mt ()) | Some c -> (* Force evaluation *) - let pb = prterm_env env c in + let pb = pr_lconstr_env env c in (str" := " ++ pb ++ cut () ) in - let pt = prtype_env env typ in + let pt = pr_ltype_env env typ in let ptyp = (str" : " ++ pt) in (pr_id id ++ hov 0 (pbody ++ ptyp)) @@ -93,9 +126,9 @@ let pr_rel_decl env (na,c,typ) = | None -> mt () | Some c -> (* Force evaluation *) - let pb = prterm_env env c in + let pb = pr_lconstr_env env c in (str":=" ++ spc () ++ pb ++ spc ()) in - let ptyp = prtype_env env typ in + let ptyp = pr_ltype_env env typ in match na with | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) @@ -190,7 +223,7 @@ let pr_context_of env = match Options.print_hyps_limit () with let pr_goal g = let env = evar_env g in let penv = pr_context_of env in - let pc = prtype_env_at_top env g.evar_concl in + let pc = pr_ltype_env_at_top env g.evar_concl in str" " ++ hv 0 (penv ++ fnl () ++ str (emacs_str (String.make 1 (Char.chr 253))) ++ str "============================" ++ fnl () ++ @@ -199,14 +232,14 @@ let pr_goal g = (* display the conclusion of a goal *) let pr_concl n g = let env = evar_env g in - let pc = prtype_env_at_top env g.evar_concl in + let pc = pr_ltype_env_at_top env g.evar_concl in str (emacs_str (String.make 1 (Char.chr 253))) ++ str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" " ++ pc (* display evar type: a context and a type *) let pr_evgl_sign gl = let ps = pr_named_context_of (evar_env gl) in - let pc = prterm gl.evar_concl in + let pc = pr_lconstr gl.evar_concl in hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]") (* Print an enumerated list of existential variables *) @@ -284,12 +317,6 @@ let pr_nth_open_subgoal n = (* Elementary tactics *) -let print_constr8 t = - pr_constr (Constrextern.extern_constr false (Global.env()) t) - -let print_lconstr8 t = - pr_lconstr (Constrextern.extern_constr false (Global.env()) t) - let pr_prim_rule = function | Intro id -> str"intro " ++ pr_id id @@ -299,9 +326,9 @@ let pr_prim_rule = function | Cut (b,id,t) -> if b then - (str"assert " ++ print_constr8 t) + (str"assert " ++ pr_constr t) else - (str"cut " ++ print_constr8 t ++ str ";[intro " ++ pr_id id ++ str "|idtac]") + (str"cut " ++ pr_constr t ++ str ";[intro " ++ pr_id id ++ str "|idtac]") | FixRule (f,n,[]) -> (str"fix " ++ pr_id f ++ str"/" ++ int n) @@ -309,7 +336,7 @@ let pr_prim_rule = function | FixRule (f,n,others) -> let rec print_mut = function | (f,n,ar)::oth -> - pr_id f ++ str"/" ++ int n ++ str" : " ++ print_lconstr8 ar ++ print_mut oth + pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth | [] -> mt () in (str"fix " ++ pr_id f ++ str"/" ++ int n ++ str" with " ++ print_mut others) @@ -320,22 +347,22 @@ let pr_prim_rule = function | Cofix (f,others) -> let rec print_mut = function | (f,ar)::oth -> - (pr_id f ++ str" : " ++ print_lconstr8 ar ++ print_mut oth) + (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth) | [] -> mt () in (str"cofix " ++ pr_id f ++ str" with " ++ print_mut others) | Refine c -> str(if occur_meta c then "refine " else "exact ") ++ - Constrextern.with_meta_as_hole print_constr8 c + Constrextern.with_meta_as_hole pr_constr c | Convert_concl (c,_) -> - (str"change " ++ print_constr8 c) + (str"change " ++ pr_constr c) | Convert_hyp (id,None,t) -> - (str"change " ++ print_constr8 t ++ spc () ++ str"in " ++ pr_id id) + (str"change " ++ pr_constr t ++ spc () ++ str"in " ++ pr_id id) | Convert_hyp (id,Some c,t) -> - (str"change " ++ print_constr8 c ++ spc () ++ str"in " + (str"change " ++ pr_constr c ++ spc () ++ str"in " ++ pr_id id ++ str" (type of " ++ pr_id id ++ str ")") | Thin ids -> diff --git a/parsing/printer.mli b/parsing/printer.mli index 4890b1bea..f3cdfda47 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -21,51 +21,76 @@ open Nametab open Termops open Evd open Proof_type +open Rawterm (*i*) (* These are the entry points for printing terms, context, tac, ... *) -val prterm_env : env -> constr -> std_ppcmds -val prterm_env_at_top : env -> constr -> std_ppcmds -val prterm : constr -> std_ppcmds -val prtype_env : env -> types -> std_ppcmds -val prtype : types -> std_ppcmds -val prjudge_env : - env -> Environ.unsafe_judgment -> std_ppcmds * std_ppcmds -val prjudge : Environ.unsafe_judgment -> std_ppcmds * std_ppcmds - -val pr_rawterm : Rawterm.rawconstr -> std_ppcmds -val pr_cases_pattern : Rawterm.cases_pattern -> std_ppcmds - -val pr_constant : env -> constant -> std_ppcmds -val pr_existential : env -> existential -> std_ppcmds -val pr_constructor : env -> constructor -> std_ppcmds -val pr_inductive : env -> inductive -> std_ppcmds -val pr_global : global_reference -> std_ppcmds +(* Terms *) + +val pr_lconstr_env : env -> constr -> std_ppcmds +val pr_lconstr_env_at_top : env -> constr -> std_ppcmds +val pr_lconstr : constr -> std_ppcmds + +val pr_constr_env : env -> constr -> std_ppcmds +val pr_constr : constr -> std_ppcmds + +val pr_ltype_env : env -> types -> std_ppcmds +val pr_ltype : types -> std_ppcmds + +val pr_type_env : env -> types -> std_ppcmds +val pr_type : types -> std_ppcmds + +val pr_ljudge_env : env -> unsafe_judgment -> std_ppcmds * std_ppcmds +val pr_ljudge : unsafe_judgment -> std_ppcmds * std_ppcmds + +val pr_lrawconstr_env : env -> rawconstr -> std_ppcmds +val pr_lrawconstr : rawconstr -> std_ppcmds + +val pr_rawconstr_env : env -> rawconstr -> std_ppcmds +val pr_rawconstr : rawconstr -> std_ppcmds + +val pr_constr_pattern_env : env -> constr_pattern -> std_ppcmds +val pr_constr_pattern : constr_pattern -> std_ppcmds + +val pr_cases_pattern : cases_pattern -> std_ppcmds + +(* Printing global references using names as short as possible *) + +val pr_global_env : Idset.t -> global_reference -> std_ppcmds +val pr_global : global_reference -> std_ppcmds + +val pr_constant : env -> constant -> std_ppcmds +val pr_existential : env -> existential -> std_ppcmds +val pr_constructor : env -> constructor -> std_ppcmds +val pr_inductive : env -> inductive -> std_ppcmds val pr_evaluable_reference : evaluable_global_reference -> std_ppcmds -val pr_pattern : constr_pattern -> std_ppcmds -val pr_pattern_env : env -> names_context -> constr_pattern -> std_ppcmds -val pr_ne_context_of : std_ppcmds -> env -> std_ppcmds +(* Contexts *) -val pr_var_decl : env -> named_declaration -> std_ppcmds -val pr_rel_decl : env -> rel_declaration -> std_ppcmds +val pr_ne_context_of : std_ppcmds -> env -> std_ppcmds -val pr_named_context : env -> named_context -> std_ppcmds -val pr_named_context_of : env -> std_ppcmds -val pr_rel_context : env -> rel_context -> std_ppcmds -val pr_rel_context_of : env -> std_ppcmds -val pr_context_of : env -> std_ppcmds +val pr_var_decl : env -> named_declaration -> std_ppcmds +val pr_rel_decl : env -> rel_declaration -> std_ppcmds -val emacs_str : string -> string +val pr_named_context : env -> named_context -> std_ppcmds +val pr_named_context_of : env -> std_ppcmds +val pr_rel_context : env -> rel_context -> std_ppcmds +val pr_rel_context_of : env -> std_ppcmds +val pr_context_of : env -> std_ppcmds (* Proofs *) -val pr_goal : goal -> std_ppcmds -val pr_subgoals : evar_map -> goal list -> std_ppcmds -val pr_subgoal : int -> goal list -> std_ppcmds -val pr_open_subgoals : unit -> std_ppcmds -val pr_nth_open_subgoal : int -> std_ppcmds -val pr_evars_int : int -> (evar * evar_info) list -> std_ppcmds +val pr_goal : goal -> std_ppcmds +val pr_subgoals : evar_map -> goal list -> std_ppcmds +val pr_subgoal : int -> goal list -> std_ppcmds -val pr_prim_rule : prim_rule -> std_ppcmds +val pr_open_subgoals : unit -> std_ppcmds +val pr_nth_open_subgoal : int -> std_ppcmds +val pr_evars_int : int -> (evar * evar_info) list -> std_ppcmds + +val pr_prim_rule : prim_rule -> std_ppcmds + +(* Emacs/proof general support *) + +val emacs_str : string -> string diff --git a/parsing/search.ml b/parsing/search.ml index 42b5cef5c..580cb790c 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -102,7 +102,7 @@ let constr_to_section_path c = match kind_of_term c with let xor a b = (a or b) & (not (a & b)) let plain_display ref a c = - let pc = prterm_env a c in + let pc = pr_lconstr_env a c in let pr = pr_global ref in msg (hov 2 (pr ++ str":" ++ spc () ++ pc) ++ fnl ()) diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index 827cfcd0e..c00350053 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -70,7 +70,7 @@ let rec print_proof sigma osign pf = let pr_change gl = str"Change " ++ - prterm_env (Global.env_of_context gl.evar_hyps) gl.evar_concl ++ str"." + pr_lconstr_env (Global.env_of_context gl.evar_hyps) gl.evar_concl ++ str"." let rec print_script nochange sigma osign pf = let {evar_hyps=sign; evar_concl=cl} = pf.goal in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index b955d62d7..0d3e6674e 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -210,19 +210,10 @@ let extract_nondep_branches test c b n = | _ -> assert false in if test c n then Some (strip n b) else None -let detype_case computable detype detype_eqn testdep - tenv avoid indsp st p k c bl = +let detype_case computable detype detype_eqn testdep avoid data p c bl = + let (indsp,st,nparams,consnargsl,k) = data in let synth_type = synthetize_type () in let tomatch = detype c in - - (* Find constructors arity *) - let (mib,mip) = Inductive.lookup_mind_specif tenv indsp in - let get_consnarg j = - let typi = mis_nf_constructor_type (indsp,mib,mip) (j+1) in - let _,t = decompose_prod_n_assum (List.length mib.mind_params_ctxt) typi in - List.rev (fst (decompose_prod_assum t)) in - let consnargs = Array.init (Array.length mip.mind_consnames) get_consnarg in - let consnargsl = Array.map List.length consnargs in let alias, aliastyp, pred= if (not !Options.raw_print) & synth_type & computable & Array.length bl<>0 then @@ -252,8 +243,8 @@ let detype_case computable detype detype_eqn testdep let aliastyp = if List.for_all ((=) Anonymous) nl then None else - let pars = list_tabulate (fun _ -> Anonymous) mib.mind_nparams - in Some (dummy_loc,indsp,pars@nl) in + let pars = list_tabulate (fun _ -> Anonymous) nparams in + Some (dummy_loc,indsp,pars@nl) in n, aliastyp, Some typ in let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in @@ -304,7 +295,7 @@ let detype_case computable detype detype_eqn testdep RCases(dummy_loc,pred,[tomatch,(alias,aliastyp)],eqnl) -let rec detype tenv avoid env t = +let rec detype isgoal avoid env t = match kind_of_term (collapse_appl t) with | Rel n -> (try match lookup_name_of_rel n env with @@ -324,18 +315,18 @@ let rec detype tenv avoid env t = | Sort (Prop c) -> RSort (dummy_loc,RProp c) | Sort (Type u) -> RSort (dummy_loc,RType (Some u)) | Cast (c1,k,c2) -> - RCast(dummy_loc,detype tenv avoid env c1, k, - detype tenv avoid env c2) - | Prod (na,ty,c) -> detype_binder tenv BProd avoid env na ty c - | Lambda (na,ty,c) -> detype_binder tenv BLambda avoid env na ty c - | LetIn (na,b,_,c) -> detype_binder tenv BLetIn avoid env na b c + RCast(dummy_loc,detype isgoal avoid env c1, k, + detype isgoal avoid env c2) + | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c + | Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env na ty c + | LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env na b c | App (f,args) -> - RApp (dummy_loc,detype tenv avoid env f, - array_map_to_list (detype tenv avoid env) args) + RApp (dummy_loc,detype isgoal avoid env f, + array_map_to_list (detype isgoal avoid env) args) | Const sp -> RRef (dummy_loc, ConstRef sp) | Evar (ev,cl) -> REvar (dummy_loc, ev, - Some (List.map (detype tenv avoid env) (Array.to_list cl))) + Some (List.map (detype isgoal avoid env) (Array.to_list cl))) | Ind ind_sp -> RRef (dummy_loc, IndRef ind_sp) | Construct cstr_sp -> @@ -344,13 +335,14 @@ let rec detype tenv avoid env t = let comp = computable p (annot.ci_pp_info.ind_nargs) in let ind = annot.ci_ind in let st = annot.ci_pp_info.style in - detype_case comp (detype tenv avoid env) (detype_eqn tenv avoid env) - is_nondep_branch - (snd tenv) avoid ind st (Some p) annot.ci_pp_info.ind_nargs c bl - | Fix (nvn,recdef) -> detype_fix tenv avoid env nvn recdef - | CoFix (n,recdef) -> detype_cofix tenv avoid env n recdef - -and detype_fix tenv avoid env (vn,_ as nvn) (names,tys,bodies) = + detype_case comp (detype isgoal avoid env) (detype_eqn isgoal avoid env) + is_nondep_branch avoid + (ind,st,annot.ci_npar,annot.ci_cstr_nargs,annot.ci_pp_info.ind_nargs) + (Some p) c bl + | Fix (nvn,recdef) -> detype_fix isgoal avoid env nvn recdef + | CoFix (n,recdef) -> detype_cofix isgoal avoid env n recdef + +and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) = let def_avoid, def_env, lfi = Array.fold_left (fun (avoid, env, l) na -> @@ -359,14 +351,14 @@ and detype_fix tenv avoid env (vn,_ as nvn) (names,tys,bodies) = (avoid, env, []) names in let n = Array.length tys in let v = array_map3 - (fun c t i -> share_names tenv (i+1) [] def_avoid def_env c (lift n t)) + (fun c t i -> share_names isgoal (i+1) [] def_avoid def_env c (lift n t)) bodies tys vn in RRec(dummy_loc,RFix nvn,Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) -and detype_cofix tenv avoid env n (names,tys,bodies) = +and detype_cofix isgoal avoid env n (names,tys,bodies) = let def_avoid, def_env, lfi = Array.fold_left (fun (avoid, env, l) na -> @@ -375,14 +367,14 @@ and detype_cofix tenv avoid env n (names,tys,bodies) = (avoid, env, []) names in let ntys = Array.length tys in let v = array_map2 - (fun c t -> share_names tenv 0 [] def_avoid def_env c (lift ntys t)) + (fun c t -> share_names isgoal 0 [] def_avoid def_env c (lift ntys t)) bodies tys in RRec(dummy_loc,RCoFix n,Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) -and share_names tenv n l avoid env c t = +and share_names isgoal n l avoid env c t = match kind_of_term c, kind_of_term t with (* factorize even when not necessary to have better presentation *) | Lambda (na,t,c), Prod (na',t',c') -> @@ -390,35 +382,35 @@ and share_names tenv n l avoid env c t = Name _, _ -> na | _, Name _ -> na' | _ -> na in - let t = detype tenv avoid env t in + let t = detype isgoal avoid env t in let id = next_name_away na avoid in let avoid = id::avoid and env = add_name (Name id) env in - share_names tenv (n-1) ((Name id,None,t)::l) avoid env c c' + share_names isgoal (n-1) ((Name id,None,t)::l) avoid env c c' (* May occur for fix built interactively *) | LetIn (na,b,t',c), _ when n > 0 -> - let t' = detype tenv avoid env t' in - let b = detype tenv avoid env b in + let t' = detype isgoal avoid env t' in + let b = detype isgoal avoid env b in let id = next_name_away na avoid in let avoid = id::avoid and env = add_name (Name id) env in - share_names tenv n ((Name id,Some b,t')::l) avoid env c t + share_names isgoal n ((Name id,Some b,t')::l) avoid env c t (* Only if built with the f/n notation or w/o let-expansion in types *) | _, LetIn (_,b,_,t) when n > 0 -> - share_names tenv n l avoid env c (subst1 b t) + share_names isgoal n l avoid env c (subst1 b t) (* If it is an open proof: we cheat and eta-expand *) | _, Prod (na',t',c') when n > 0 -> - let t' = detype tenv avoid env t' in + let t' = detype isgoal avoid env t' in let id = next_name_away na' avoid in let avoid = id::avoid and env = add_name (Name id) env in let appc = mkApp (lift 1 c,[|mkRel 1|]) in - share_names tenv (n-1) ((Name id,None,t')::l) avoid env appc c' + share_names isgoal (n-1) ((Name id,None,t')::l) avoid env appc c' (* If built with the f/n notation: we renounce to share names *) | _ -> if n>0 then warning "Detyping.detype: cannot factorize fix enough"; - let c = detype tenv avoid env c in - let t = detype tenv avoid env t in + let c = detype isgoal avoid env c in + let t = detype isgoal avoid env t in (List.rev l,c,t) -and detype_eqn tenv avoid env constr construct_nargs branch = +and detype_eqn isgoal avoid env constr construct_nargs branch = let make_pat x avoid env b ids = if force_wildcard () & noccurn 1 b then PatVar (dummy_loc,Anonymous),avoid,(add_name Anonymous env),ids @@ -430,7 +422,7 @@ and detype_eqn tenv avoid env constr construct_nargs branch = if n=0 then (dummy_loc, ids, [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)], - detype tenv avoid env b) + detype isgoal avoid env b) else match kind_of_term b with | Lambda (x,_,b) -> @@ -455,17 +447,17 @@ and detype_eqn tenv avoid env constr construct_nargs branch = in buildrec [] [] avoid env construct_nargs branch -and detype_binder tenv bk avoid env na ty c = +and detype_binder isgoal bk avoid env na ty c = let na',avoid' = if bk = BLetIn then - concrete_let_name (fst tenv) avoid env na c + concrete_let_name isgoal avoid env na c else - concrete_name (fst tenv) avoid env na c in - let r = detype tenv avoid' (add_name na' env) c in + concrete_name isgoal avoid env na c in + let r = detype isgoal avoid' (add_name na' env) c in match bk with - | BProd -> RProd (dummy_loc, na',detype tenv avoid env ty, r) - | BLambda -> RLambda (dummy_loc, na',detype tenv avoid env ty, r) - | BLetIn -> RLetIn (dummy_loc, na',detype tenv avoid env ty, r) + | BProd -> RProd (dummy_loc, na',detype isgoal avoid env ty, r) + | BLambda -> RLambda (dummy_loc, na',detype isgoal avoid env ty, r) + | BLetIn -> RLetIn (dummy_loc, na',detype isgoal avoid env ty, r) let rec subst_pat subst pat = match pat with @@ -481,7 +473,7 @@ let rec subst_raw subst raw = | RRef (loc,ref) -> let ref',t = subst_global subst ref in if ref' == ref then raw else - detype (false,Global.env ()) [] [] t + detype false [] [] t | RVar _ -> raw | REvar _ -> raw diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 9f315938c..00b7c471a 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -21,20 +21,19 @@ open Mod_subst val subst_raw : substitution -> rawconstr -> rawconstr -(* [detype (b,env) avoid ctx c] turns [c], typed in [env], into a rawconstr *) +(* [detype isgoal avoid ctx c] turns a closed [c], into a rawconstr *) (* de Bruijn indexes are turned to bound names, avoiding names in [avoid] *) -(* [b] tells if naming must avoid global-level synonyms as intro does *) +(* [isgoal] tells if naming must avoid global-level synonyms as intro does *) (* [ctx] gives the names of the free variables *) -val detype : bool * env -> identifier list -> names_context -> constr -> - rawconstr +val detype : bool -> identifier list -> names_context -> constr -> rawconstr val detype_case : bool -> ('a -> rawconstr) -> (constructor -> int -> 'a -> loc * identifier list * cases_pattern list * rawconstr) -> ('a -> int -> bool) -> - env -> identifier list -> inductive -> case_style -> - 'a option -> int -> 'a -> 'a array -> rawconstr + identifier list -> inductive * case_style * int * int array * int -> + 'a option -> 'a -> 'a array -> rawconstr (* look for the index of a named var or a nondep var as it is renamed *) val lookup_name_as_renamed : env -> constr -> identifier -> int option diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 4bf81f7ae..5d2cbd57b 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -142,9 +142,9 @@ let db_mc_pattern_success debug = str "Let us execute the right-hand side part..." ++ fnl()) let pp_match_pattern env = function - | Term c -> Term (extern_pattern env (names_of_rel_context env) c) + | Term c -> Term (extern_constr_pattern (names_of_rel_context env) c) | Subterm (o,c) -> - Subterm (o,(extern_pattern env (names_of_rel_context env) c)) + Subterm (o,(extern_constr_pattern (names_of_rel_context env) c)) (* Prints a failure message for an hypothesis pattern *) let db_hyp_pattern_failure debug env (na,hyp) = diff --git a/tactics/auto.ml b/tactics/auto.ml index b7d88bf02..4f8df90b5 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -205,7 +205,7 @@ let make_apply_entry env sigma (eapply,verbose) name (c,cty) = in if eapply & (nmiss <> 0) then begin if verbose then - warn (str "the hint: eapply " ++ prterm c ++ + warn (str "the hint: eapply " ++ pr_lconstr c ++ str " will only be used by eauto"); (hd, { hname = name; @@ -231,7 +231,7 @@ let make_resolves env sigma name eap (c,cty) = [make_exact_entry; make_apply_entry env sigma eap] in if ents = [] then - errorlabstrm "Hint" (prterm c ++ spc () ++ str "cannot be used as a hint"); + errorlabstrm "Hint" (pr_lconstr c ++ spc () ++ str "cannot be used as a hint"); ents (* used to add an hypothesis to the local hint database *) @@ -476,11 +476,11 @@ let add_hints local dbnames0 h = let fmt_autotactic = function - | Res_pf (c,clenv) -> (str"apply " ++ prterm c) - | ERes_pf (c,clenv) -> (str"eapply " ++ prterm c) - | Give_exact c -> (str"exact " ++ prterm c) + | Res_pf (c,clenv) -> (str"apply " ++ pr_lconstr c) + | ERes_pf (c,clenv) -> (str"eapply " ++ pr_lconstr c) + | Give_exact c -> (str"exact " ++ pr_lconstr c) | Res_pf_THEN_trivial_fail (c,clenv) -> - (str"apply " ++ prterm c ++ str" ; trivial") + (str"apply " ++ pr_lconstr c ++ str" ; trivial") | Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c) | Extern tac -> (str "(external) " ++ Pptactic.pr_glob_tactic (Global.env()) tac) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 0c40f6b42..469fc5e42 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -48,7 +48,7 @@ let print_rewrite_hintdb bas = prlist_with_sep Pp.cut (fun (c,typ,d,t) -> str (if d then "rewrite -> " else "rewrite <- ") ++ - Printer.prterm c ++ str " of type " ++ Printer.prterm typ ++ + Printer.pr_lconstr c ++ str " of type " ++ Printer.pr_lconstr typ ++ str " then use tactic " ++ Pptactic.pr_glob_tactic (Global.env()) t) hints) with diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index eab475541..a6d82ea63 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -50,8 +50,7 @@ END let pr_gen prc _prlc _prtac c = prc c -let pr_rawc _prc _prlc _prtac raw = - Ppconstr.pr_constr (Constrextern.extern_rawconstr Idset.empty raw) +let pr_rawc _prc _prlc _prtac raw = Printer.pr_rawconstr raw let interp_raw _ _ (t,_) = t diff --git a/tactics/inv.ml b/tactics/inv.ml index 57630c964..9597cfa41 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -52,7 +52,7 @@ let check_no_metas clenv ccl = (str ("Cannot find an instantiation for variable"^ (if List.length metas = 1 then " " else "s ")) ++ prlist_with_sep pr_coma pr_name metas - (* ajouter "in " ++ prterm ccl mais il faut le bon contexte *)) + (* ajouter "in " ++ pr_lconstr ccl mais il faut le bon contexte *)) let var_occurs_in_pf gl id = let env = pf_env gl in diff --git a/tactics/leminv.ml b/tactics/leminv.ml index bd5c1bf41..e78731f57 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -40,7 +40,7 @@ let not_work_message = "tactic fails to build the inversion lemma, may be becaus let no_inductive_inconstr env constr = (str "Cannot recognize an inductive predicate in " ++ - prterm_env env constr ++ + pr_lconstr_env env constr ++ str "." ++ spc () ++ str "If there is one, may be the structure of the arity" ++ spc () ++ str "or of the type of constructors" ++ spc () ++ str "is hidden by constant definitions.") @@ -298,7 +298,7 @@ let lemInv id c gls = | UserError (a,b) -> errorlabstrm "LemInv" (str "Cannot refine current goal with the lemma " ++ - prterm_env (Global.env()) c) + pr_lconstr_env (Global.env()) c) let lemInv_gen id c = try_intros_until (fun id -> lemInv id c) id diff --git a/tactics/refine.ml b/tactics/refine.ml index a6b904c05..c0f333d4b 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -66,12 +66,12 @@ and sg_proofs = (term_with_holes option) list (* pour debugger *) let rec pp_th (TH(c,mm,sg)) = - (str"TH=[ " ++ hov 0 (prterm c ++ fnl () ++ + (str"TH=[ " ++ hov 0 (pr_lconstr c ++ fnl () ++ (* pp_mm mm ++ fnl () ++ *) pp_sg sg) ++ str "]") and pp_mm l = hov 0 (prlist_with_sep (fun _ -> (fnl ())) - (fun (n,c) -> (int n ++ str" --> " ++ prterm c)) l) + (fun (n,c) -> (int n ++ str" --> " ++ pr_lconstr c)) l) and pp_sg sg = hov 0 (prlist_with_sep (fun _ -> (fnl ())) (function None -> (str"None") | Some th -> (pp_th th)) sg) diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 8aa5f5532..cc58983bd 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -217,16 +217,16 @@ let relation_table_find s = Gmap.find s !relation_table let relation_table_mem s = Gmap.mem s !relation_table let prrelation s = - str "(" ++ prterm s.rel_a ++ str "," ++ prterm s.rel_aeq ++ str ")" + str "(" ++ pr_lconstr s.rel_a ++ str "," ++ pr_lconstr s.rel_aeq ++ str ")" let prrelation_class = function Relation eq -> (try prrelation (relation_table_find eq) with Not_found -> - str "[[ Error: " ++ prterm eq ++ + str "[[ Error: " ++ pr_lconstr eq ++ str " is not registered as a relation ]]") - | Leibniz (Some ty) -> prterm ty + | Leibniz (Some ty) -> pr_lconstr ty | Leibniz None -> str "_" let prmorphism_argument_gen prrelation (variance,rel) = @@ -239,11 +239,11 @@ let prmorphism_argument_gen prrelation (variance,rel) = let prargument_class = prmorphism_argument_gen prrelation_class let pr_morphism_signature (l,c) = - prlist (prmorphism_argument_gen Ppconstr.pr_constr) l ++ - Ppconstr.pr_constr c + prlist (prmorphism_argument_gen Ppconstr.pr_constr_expr) l ++ + Ppconstr.pr_constr_expr c let prmorphism k m = - prterm k ++ str ": " ++ + pr_lconstr k ++ str ": " ++ prlist prargument_class m.args ++ prrelation_class m.output @@ -259,7 +259,7 @@ let default_relation_for_carrier ?(filter=fun _ -> true) a = if tl <> [] then ppnl (str "Warning: There are several relations on the carrier \"" ++ - prterm a ++ str "\". The relation " ++ prrelation relation ++ + pr_lconstr a ++ str "\". The relation " ++ prrelation relation ++ str " is chosen.") ; Relation relation @@ -350,24 +350,24 @@ let (relation_to_obj, obj_to_relation)= str " is redeclared. The new declaration" ++ (match th'.rel_refl with None -> str "" - | Some t -> str " (reflevity proved by " ++ prterm t) ++ + | Some t -> str " (reflevity proved by " ++ pr_lconstr t) ++ (match th'.rel_sym with None -> str "" | Some t -> (if th'.rel_refl = None then str " (" else str " and ") ++ - str "symmetry proved by " ++ prterm t) ++ + str "symmetry proved by " ++ pr_lconstr t) ++ (if th'.rel_refl <> None && th'.rel_sym <> None then str ")" else str "") ++ str " replaces the old declaration" ++ (match old_relation.rel_refl with None -> str "" - | Some t -> str " (reflevity proved by " ++ prterm t) ++ + | Some t -> str " (reflevity proved by " ++ pr_lconstr t) ++ (match old_relation.rel_sym with None -> str "" | Some t -> (if old_relation.rel_refl = None then str " (" else str " and ") ++ - str "symmetry proved by " ++ prterm t) ++ + str "symmetry proved by " ++ pr_lconstr t) ++ (if old_relation.rel_refl <> None && old_relation.rel_sym <> None then str ")" else str "") ++ str "."); @@ -414,9 +414,9 @@ let morphism_table_add (m,c) = (str "Warning: The morphism " ++ prmorphism m old_morph ++ str " is redeclared. " ++ str "The new declaration whose compatibility is proved by " ++ - prterm c.lem ++ str " replaces the old declaration whose" ++ + pr_lconstr c.lem ++ str " replaces the old declaration whose" ++ str " compatibility was proved by " ++ - prterm old_morph.lem ++ str ".") + pr_lconstr old_morph.lem ++ str ".") with Not_found -> morphism_table := Gmap.add m (c::old) !morphism_table @@ -427,7 +427,7 @@ let default_morphism ?(filter=fun _ -> true) m = if ml <> [] then ppnl (str "Warning: There are several morphisms associated to \"" ++ - prterm m ++ str"\". Morphism " ++ prmorphism m m1 ++ + pr_lconstr m ++ str"\". Morphism " ++ prmorphism m m1 ++ str " is randomly chosen."); relation_morphism_of_constr_morphism m1 @@ -485,13 +485,13 @@ let print_setoids () = ppnl (str"Relation " ++ prrelation relation ++ str";" ++ (match relation.rel_refl with None -> str "" - | Some t -> str" reflexivity proved by " ++ prterm t) ++ + | Some t -> str" reflexivity proved by " ++ pr_lconstr t) ++ (match relation.rel_sym with None -> str "" - | Some t -> str " symmetry proved by " ++ prterm t) ++ + | Some t -> str " symmetry proved by " ++ pr_lconstr t) ++ (match relation.rel_trans with None -> str "" - | Some t -> str " transitivity proved by " ++ prterm t))) + | Some t -> str " transitivity proved by " ++ pr_lconstr t))) !relation_table ; Gmap.iter (fun k l -> @@ -499,7 +499,7 @@ let print_setoids () = (fun ({lem=lem} as mor) -> ppnl (str "Morphism " ++ prmorphism k mor ++ str ". Compatibility proved by " ++ - prterm lem ++ str ".")) + pr_lconstr lem ++ str ".")) l) !morphism_table ;; @@ -703,15 +703,15 @@ let add_morphism lemma_infos mor_name (m,quantifiers_rev,args,output) = output = output_constr; lem = lem; morphism_theory = mmor })); - Options.if_verbose ppnl (prterm m ++ str " is registered as a morphism") + Options.if_verbose ppnl (pr_lconstr m ++ str " is registered as a morphism") (* first order matching with a bit of conversion *) let unify_relation_carrier_with_type env rel t = let raise_error quantifiers_no = errorlabstrm "New Morphism" - (str "One morphism argument or its output has type " ++ prterm t ++ + (str "One morphism argument or its output has type " ++ pr_lconstr t ++ str " but the signature requires an argument of type \"" ++ - prterm rel.rel_a ++ str " " ++ prvect_with_sep pr_spc (fun _ -> str "?") + pr_lconstr rel.rel_a ++ str " " ++ prvect_with_sep pr_spc (fun _ -> str "?") (Array.make quantifiers_no 0) ++ str "\"") in let args = match kind_of_term t with @@ -757,9 +757,9 @@ let unify_relation_class_carrier_with_type env rel t = rel else errorlabstrm "New Morphism" - (str "One morphism argument or its output has type " ++ prterm t ++ + (str "One morphism argument or its output has type " ++ pr_lconstr t ++ str " but the signature requires an argument of type " ++ - prterm t') + pr_lconstr t') | Leibniz None -> Leibniz (Some t) | Relation rel -> Relation (unify_relation_carrier_with_type env rel t) @@ -837,8 +837,8 @@ let new_morphism m signature id hook = None -> if args_ty = [] then errorlabstrm "New Morphism" - (str "The term " ++ prterm m ++ str " has type " ++ - prterm typeofm ++ str " that is not a product.") ; + (str "The term " ++ pr_lconstr m ++ str " has type " ++ + pr_lconstr typeofm ++ str " that is not a product.") ; ignore (check_is_dependent 0 args_ty output) ; let args = List.map @@ -851,8 +851,8 @@ let new_morphism m signature id hook = let number_of_quantifiers = args_ty_len - number_of_arguments in if number_of_quantifiers < 0 then errorlabstrm "New Morphism" - (str "The morphism " ++ prterm m ++ str " has type " ++ - prterm typeofm ++ str " that attends at most " ++ int args_ty_len ++ + (str "The morphism " ++ pr_lconstr m ++ str " has type " ++ + pr_lconstr typeofm ++ str " that attends at most " ++ int args_ty_len ++ str " arguments. The signature that you specified requires " ++ int number_of_arguments ++ str " arguments.") else @@ -869,7 +869,7 @@ let new_morphism m signature id hook = rel, unify_relation_class_carrier_with_type env rel real_t with Not_found -> errorlabstrm "Add Morphism" - (str "Not a valid signature: " ++ prterm t ++ + (str "Not a valid signature: " ++ pr_lconstr t ++ str " is neither a registered relation nor the Leibniz " ++ str " equality.") in @@ -976,7 +976,7 @@ let check_eq env a_quantifiers_rev a aeq = (is_conv env Evd.empty (Typing.type_of env Evd.empty aeq) typ) then errorlabstrm "Add Relation Class" - (prterm aeq ++ str " should have type (" ++ prterm typ ++ str ")") + (pr_lconstr aeq ++ str " should have type (" ++ pr_lconstr typ ++ str ")") let check_property env a_quantifiers_rev a aeq strprop coq_prop t = if @@ -1070,7 +1070,7 @@ let int_add_relation id a aeq refl sym trans = rel_X_relation_class = current_constant id; rel_Xreflexive_relation_class = current_constant id_precise } in Lib.add_anonymous_leaf (relation_to_obj (aeq, aeq_rel)) ; - Options.if_verbose ppnl (prterm aeq ++ str " is registered as a relation"); + Options.if_verbose ppnl (pr_lconstr aeq ++ str " is registered as a relation"); match trans with None -> () | Some trans -> @@ -1233,7 +1233,7 @@ let relation_class_that_matches_a_constr caller_name new_goals hypt = function [] | [_] -> - errorlabstrm caller_name (prterm hypt ++ + errorlabstrm caller_name (pr_lconstr hypt ++ str " is not a registered relation.") | [_;_] -> [] | he::tl -> he::(get_all_but_last_two tl) in @@ -1257,7 +1257,7 @@ let relation_class_that_matches_a_constr caller_name new_goals hypt = with Not_found -> if l = [] then errorlabstrm caller_name - (prterm (mkApp (aeq, Array.of_list all_aeq_args)) ++ + (pr_lconstr (mkApp (aeq, Array.of_list all_aeq_args)) ++ str " is not a registered relation.") else let last,others = Util.list_sep_last l in @@ -1309,7 +1309,7 @@ let pr_new_goals i c = else (pr_fnl () ++ str " " ++ prlist_with_sep (fun () -> str "\n ") - (fun c -> str " ... |- " ++ prterm c) glc)) + (fun c -> str " ... |- " ++ pr_lconstr c) glc)) (* given a list of constr_with_marks, it returns the list where constr_with_marks than open more goals than simpler ones in the list @@ -1527,7 +1527,7 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction = errorlabstrm "Setoid_replace" (str "Rewriting in a product A -> B is possible only when A " ++ str "is a proposition (i.e. A is of type Prop). The type " ++ - prterm c1 ++ str " has type " ++ prterm typeofc1 ++ + pr_lconstr c1 ++ str " has type " ++ pr_lconstr typeofc1 ++ str " that is not convertible to Prop.") else aux output_relation output_direction @@ -1536,7 +1536,7 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction = | _ -> if occur_term t in_c then errorlabstrm "Setoid_replace" - (str "Trying to replace " ++ prterm t ++ str " in " ++ prterm in_c ++ + (str "Trying to replace " ++ pr_lconstr t ++ str " in " ++ pr_lconstr in_c ++ str " that is not an applicative context.") else [ToKeep (in_c,output_relation,output_direction)] @@ -1555,7 +1555,7 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction = match res' with [] when res = [] -> errorlabstrm "Setoid_rewrite" - (str "Either the term " ++ prterm t ++ str " that must be " ++ + (str "Either the term " ++ pr_lconstr t ++ str " that must be " ++ str "rewritten occurs in a covariant position or the goal is not " ++ str "made of morphism applications only. You can replace only " ++ str "occurrences that are in a contravariant position and such that " ++ @@ -1835,7 +1835,7 @@ let setoid_replace relation c1 c2 ~new_goals gl = with Not_found -> errorlabstrm "Setoid_rewrite" - (prterm rel ++ str " is not a registered relation.")) + (pr_lconstr rel ++ str " is not a registered relation.")) | None -> match default_relation_for_carrier (pf_type_of gl c1) with Relation sa -> sa diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 8f537a601..8d4d37f42 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -114,8 +114,8 @@ let pr_value env = function | VVoid -> str "()" | VInteger n -> int n | VIntroPattern ipat -> pr_intro_pattern ipat - | VConstr c -> prterm_env env c - | VConstr_context c -> prterm_env env c + | VConstr c -> pr_lconstr_env env c + | VConstr_context c -> pr_lconstr_env env c | (VTactic _ | VRTactic _ | VFun _ | VRec _) -> str "<fun>" (* Transforms a named_context into a (string * constr) list *) @@ -1917,7 +1917,7 @@ let subst_global_reference subst = let ref',t' = subst_global subst ref in if not (eq_constr (constr_of_global ref') t') then ppnl (str "Warning: the reference " ++ pr_global ref ++ str " is not " ++ - str " expanded to \"" ++ prterm t' ++ str "\", but to " ++ + str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++ pr_global ref') ; ref' in diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml index dd5160f76..91e77f495 100644 --- a/toplevel/fhimsg.ml +++ b/toplevel/fhimsg.ml @@ -231,7 +231,7 @@ let explain_ill_formed_rec_body k ctx err names i vdefs = | RecCallInCasePred c -> (str "Not allowed recursive call in the type of cases in") | NotGuardedForm c -> - str "Sub-expression " ++ prterm_env ctx c ++ spc() ++ + str "Sub-expression " ++ pr_lconstr_env ctx c ++ spc() ++ str "not in guarded form (should be a constructor, Cases or CoFix)" in let pvd = P.pr_term k ctx vdefs.(i) in diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 58b6f85c9..cd7fcc417 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -31,9 +31,9 @@ open Evd let quote s = h 0 (str "\"" ++ s ++ str "\"") -let prterm c = quote (prterm c) -let prterm_env e c = quote (prterm_env e c) -let prjudge_env e c = let v,t = prjudge_env e c in (quote v,quote t) +let pr_lconstr c = quote (pr_lconstr c) +let pr_lconstr_env e c = quote (pr_lconstr_env e c) +let pr_ljudge_env e c = let v,t = pr_ljudge_env e c in (quote v,quote t) let nth i = let many = match i mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in @@ -57,20 +57,20 @@ let explain_unbound_var ctx v = let explain_not_type ctx j = let pe = pr_ne_context_of (str"In environment") ctx in - let pc,pt = prjudge_env ctx j in + let pc,pt = pr_ljudge_env ctx j in pe ++ str "the term" ++ brk(1,1) ++ pc ++ spc () ++ str"has type" ++ spc () ++ pt ++ spc () ++ str"which should be Set, Prop or Type." let explain_bad_assumption ctx j = let pe = pr_ne_context_of (str"In environment") ctx in - let pc,pt = prjudge_env ctx j in + let pc,pt = pr_ljudge_env ctx j in pe ++ str "cannot declare a variable or hypothesis over the term" ++ brk(1,1) ++ pc ++ spc () ++ str"of type" ++ spc () ++ pt ++ spc () ++ str "because this term is not a type." let explain_reference_variables c = - let pc = prterm c in + let pc = pr_lconstr c in str "the constant" ++ spc () ++ pc ++ spc () ++ str "refers to variables which are not in the context" @@ -83,11 +83,11 @@ let rec pr_disjunction pr = function let explain_elim_arity ctx ind aritylst c pj okinds = let ctx = make_all_name_different ctx in let pi = pr_inductive ctx ind in - let pc = prterm_env ctx c in + let pc = pr_lconstr_env ctx c in let msg = match okinds with | Some(kp,ki,explanation) -> - let pki = prterm_env ctx ki in - let pkp = prterm_env ctx kp in + let pki = pr_lconstr_env ctx ki in + let pkp = pr_lconstr_env ctx kp in let explanation = match explanation with | NonInformativeToInformative -> "proofs can be eliminated only to build proofs" @@ -109,16 +109,16 @@ let explain_elim_arity ctx ind aritylst c pj okinds = (let sorts = List.map (fun x -> mkSort (new_sort_in_family x)) (list_uniquize (List.map (fun ar -> family_of_sort (destSort (snd (decompose_prod_assum ar)))) aritylst)) in - let ppar = pr_disjunction (prterm_env ctx) sorts in - let ppt = prterm_env ctx (snd (decompose_prod_assum pj.uj_type)) in + let ppar = pr_disjunction (pr_lconstr_env ctx) sorts in + let ppt = pr_lconstr_env ctx (snd (decompose_prod_assum pj.uj_type)) in str "," ++ spc() ++ str "the return type has sort" ++ spc() ++ ppt ++ spc () ++ str "while it should be " ++ ppar)) ++ fnl () ++ msg let explain_case_not_inductive ctx cj = let ctx = make_all_name_different ctx in - let pc = prterm_env ctx cj.uj_val in - let pct = prterm_env ctx cj.uj_type in + let pc = pr_lconstr_env ctx cj.uj_val in + let pct = pr_lconstr_env ctx cj.uj_type in match kind_of_term cj.uj_type with | Evar _ -> str "Cannot infer a type for this expression" @@ -129,17 +129,17 @@ let explain_case_not_inductive ctx cj = let explain_number_branches ctx cj expn = let ctx = make_all_name_different ctx in - let pc = prterm_env ctx cj.uj_val in - let pct = prterm_env ctx cj.uj_type in + let pc = pr_lconstr_env ctx cj.uj_val in + let pct = pr_lconstr_env ctx cj.uj_type in str "Matching on term" ++ brk(1,1) ++ pc ++ spc () ++ str "of type" ++ brk(1,1) ++ pct ++ spc () ++ str "expects " ++ int expn ++ str " branches" let explain_ill_formed_branch ctx c i actty expty = let ctx = make_all_name_different ctx in - let pc = prterm_env ctx c in - let pa = prterm_env ctx actty in - let pe = prterm_env ctx expty in + let pc = pr_lconstr_env ctx c in + let pa = pr_lconstr_env ctx actty in + let pe = pr_lconstr_env ctx expty in str "In pattern-matching on term" ++ brk(1,1) ++ pc ++ spc () ++ str "the branch " ++ int (i+1) ++ str " has type" ++ brk(1,1) ++ pa ++ spc () ++ @@ -147,8 +147,8 @@ let explain_ill_formed_branch ctx c i actty expty = let explain_generalization ctx (name,var) j = let pe = pr_ne_context_of (str "In environment") ctx in - let pv = prtype_env ctx var in - let (pc,pt) = prjudge_env (push_rel_assum (name,var) ctx) j in + let pv = pr_ltype_env ctx var in + let (pc,pt) = pr_ljudge_env (push_rel_assum (name,var) ctx) j in str"Illegal generalization: " ++ pe ++ str"Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++ str"over" ++ brk(1,1) ++ pc ++ str"," ++ spc () ++ @@ -157,8 +157,8 @@ let explain_generalization ctx (name,var) j = let explain_actual_type ctx j pt = let pe = pr_ne_context_of (str "In environment") ctx in - let (pc,pct) = prjudge_env ctx j in - let pt = prterm_env ctx pt in + let (pc,pct) = pr_ljudge_env ctx j in + let pt = pr_lconstr_env ctx pt in pe ++ str "The term" ++ brk(1,1) ++ pc ++ spc () ++ str "has type" ++ brk(1,1) ++ pct ++ brk(1,1) ++ @@ -168,7 +168,7 @@ let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl = let ctx = make_all_name_different ctx in let randl = Array.to_list randl in (* let pe = pr_ne_context_of (str"in environment") ctx in*) - let pr,prt = prjudge_env ctx rator in + let pr,prt = pr_ljudge_env ctx rator in let term_string1,term_string2 = if List.length randl > 1 then str "terms", (str"The "++nth n++str" term") @@ -176,7 +176,7 @@ let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl = str "term", str "This term" in let appl = prlist_with_sep pr_fnl (fun c -> - let pc,pct = prjudge_env ctx c in + let pc,pct = pr_ljudge_env ctx c in hov 2 (pc ++ spc () ++ str": " ++ pct)) randl in str"Illegal application (Type Error): " ++ (* pe ++ *) fnl () ++ @@ -184,20 +184,20 @@ let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl = str"of type" ++ brk(1,1) ++ prt ++ spc () ++ str"cannot be applied to the " ++ term_string1 ++ fnl () ++ str" " ++ v 0 appl ++ fnl () ++ term_string2 ++ str" has type" ++ - brk(1,1) ++ prterm_env ctx actualtyp ++ spc () ++ - str"which should be coercible to" ++ brk(1,1) ++ prterm_env ctx exptyp + brk(1,1) ++ pr_lconstr_env ctx actualtyp ++ spc () ++ + str"which should be coercible to" ++ brk(1,1) ++ pr_lconstr_env ctx exptyp let explain_cant_apply_not_functional ctx rator randl = let ctx = make_all_name_different ctx in let randl = Array.to_list randl in (* let pe = pr_ne_context_of (str"in environment") ctx in*) - let pr = prterm_env ctx rator.uj_val in - let prt = prterm_env ctx rator.uj_type in + let pr = pr_lconstr_env ctx rator.uj_val in + let prt = pr_lconstr_env ctx rator.uj_type in let term_string = if List.length randl > 1 then "terms" else "term" in let appl = prlist_with_sep pr_fnl (fun c -> - let pc = prterm_env ctx c.uj_val in - let pct = prterm_env ctx c.uj_type in + let pc = pr_lconstr_env ctx c.uj_val in + let pct = pr_lconstr_env ctx c.uj_type in hov 2 (pc ++ spc () ++ str": " ++ pct)) randl in str"Illegal application (Non-functional construction): " ++ @@ -208,14 +208,14 @@ let explain_cant_apply_not_functional ctx rator randl = str" " ++ v 0 appl let explain_unexpected_type ctx actual_type expected_type = - let pract = prterm_env ctx actual_type in - let prexp = prterm_env ctx expected_type in + let pract = pr_lconstr_env ctx actual_type in + let prexp = pr_lconstr_env ctx expected_type in str"This type is" ++ spc () ++ pract ++ spc () ++ str "but is expected to be" ++ spc () ++ prexp let explain_not_product ctx c = - let pr = prterm_env ctx c in + let pr = pr_lconstr_env ctx c in str"The type of this term is a product," ++ spc () ++ str"but it is casted with type" ++ brk(1,1) ++ pr @@ -234,7 +234,7 @@ let explain_ill_formed_rec_body ctx err names i = | NotEnoughAbstractionInFixBody -> str "Not enough abstractions in the definition" | RecursionNotOnInductiveType c -> - str "Recursive definition on" ++ spc() ++ prterm_env ctx c ++ spc() ++ + str "Recursive definition on" ++ spc() ++ pr_lconstr_env ctx c ++ spc() ++ str "which should be an inductive type" | RecursionOnIllegalTerm(j,arg,le,lt) -> let called = @@ -255,7 +255,7 @@ let explain_ill_formed_rec_body ctx err names i = prlist_with_sep pr_spc (pr_db ctx) lt in str "Recursive call to " ++ called ++ spc() ++ str "has principal argument equal to" ++ spc() ++ - prterm_env ctx arg ++ fnl() ++ str "instead of " ++ vars + pr_lconstr_env ctx arg ++ fnl() ++ str "instead of " ++ vars | NotEnoughArgumentsForFixCall j -> let called = @@ -266,31 +266,31 @@ let explain_ill_formed_rec_body ctx err names i = (* CoFixpoint guard errors *) | CodomainNotInductiveType c -> - str "the codomain is" ++ spc () ++ prterm_env ctx c ++ spc () ++ + str "the codomain is" ++ spc () ++ pr_lconstr_env ctx c ++ spc () ++ str "which should be a coinductive type" | NestedRecursiveOccurrences -> str "nested recursive occurrences" | UnguardedRecursiveCall c -> - str "unguarded recursive call in" ++ spc() ++ prterm_env ctx c + str "unguarded recursive call in" ++ spc() ++ pr_lconstr_env ctx c | RecCallInTypeOfAbstraction c -> str "recursive call forbidden in the domain of an abstraction:" ++ - spc() ++ prterm_env ctx c + spc() ++ pr_lconstr_env ctx c | RecCallInNonRecArgOfConstructor c -> str "recursive call on a non-recursive argument of constructor" ++ - spc() ++ prterm_env ctx c + spc() ++ pr_lconstr_env ctx c | RecCallInTypeOfDef c -> str "recursive call forbidden in the type of a recursive definition" ++ - spc() ++ prterm_env ctx c + spc() ++ pr_lconstr_env ctx c | RecCallInCaseFun c -> - str "recursive call in a branch of" ++ spc() ++ prterm_env ctx c + str "recursive call in a branch of" ++ spc() ++ pr_lconstr_env ctx c | RecCallInCaseArg c -> str "recursive call in the argument of cases in" ++ spc() ++ - prterm_env ctx c + pr_lconstr_env ctx c | RecCallInCasePred c -> str "recursive call in the type of cases in" ++ spc() ++ - prterm_env ctx c + pr_lconstr_env ctx c | NotGuardedForm c -> - str "sub-expression " ++ prterm_env ctx c ++ spc() ++ + str "sub-expression " ++ pr_lconstr_env ctx c ++ spc() ++ str "not in guarded form" ++ spc()++ str"(should be a constructor, an abstraction, a match, a cofix or a recursive call)" in @@ -300,8 +300,8 @@ let explain_ill_formed_rec_body ctx err names i = let explain_ill_typed_rec_body ctx i names vdefj vargs = let ctx = make_all_name_different ctx in - let pvd,pvdt = prjudge_env ctx (vdefj.(i)) in - let pv = prterm_env ctx vargs.(i) in + let pvd,pvdt = pr_ljudge_env ctx (vdefj.(i)) in + let pv = pr_lconstr_env ctx vargs.(i) in str"The " ++ (if Array.length vdefj = 1 then mt () else int (i+1) ++ str "-th") ++ str"recursive definition" ++ spc () ++ pvd ++ spc () ++ @@ -310,19 +310,19 @@ let explain_ill_typed_rec_body ctx i names vdefj vargs = (* let explain_not_inductive ctx c = let ctx = make_all_name_different ctx in - let pc = prterm_env ctx c in + let pc = pr_lconstr_env ctx c in str"The term" ++ brk(1,1) ++ pc ++ spc () ++ str "is not an inductive definition" *) let explain_cant_find_case_type ctx c = let ctx = make_all_name_different ctx in - let pe = prterm_env ctx c in + let pe = pr_lconstr_env ctx c in hov 3 (str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe) let explain_occur_check ctx ev rhs = let ctx = make_all_name_different ctx in let id = Evd.string_of_existential ev in - let pt = prterm_env ctx rhs in + let pt = pr_lconstr_env ctx rhs in str"Occur check failed: tried to define " ++ str id ++ str" with term" ++ brk(1,1) ++ pt @@ -350,7 +350,7 @@ let explain_not_clean ctx ev t k = let ctx = make_all_name_different ctx in let c = mkRel (Intset.choose (free_rels t)) in let id = Evd.string_of_existential ev in - let var = prterm_env ctx c in + let var = pr_lconstr_env ctx c in str"Tried to define " ++ explain_hole_kind ctx k ++ str" (" ++ str id ++ str ")" ++ spc() ++ str"with a term using variable " ++ var ++ spc () ++ @@ -366,33 +366,33 @@ let explain_var_not_found ctx id = spc () ++ str "in the current" ++ spc () ++ str "environment" let explain_wrong_case_info ctx ind ci = - let pi = prterm (mkInd ind) in + let pi = pr_lconstr (mkInd ind) in if ci.ci_ind = ind then str"Pattern-matching expression on an object of inductive" ++ spc () ++ pi ++ spc () ++ str"has invalid information" else - let pc = prterm (mkInd ci.ci_ind) in + let pc = pr_lconstr (mkInd ci.ci_ind) in str"A term of inductive type" ++ spc () ++ pi ++ spc () ++ str"was given to a pattern-matching expression on the inductive type" ++ spc () ++ pc let explain_cannot_unify m n = - let pm = prterm m in - let pn = prterm n in + let pm = pr_lconstr m in + let pn = pr_lconstr n in str"Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ str"with" ++ brk(1,1) ++ pn let explain_refiner_cannot_generalize ty = str "Cannot find a well-typed generalisation of the goal with type : " ++ - prterm ty + pr_lconstr ty let explain_no_occurrence_found c = - str "Found no subterm matching " ++ prterm c ++ str " in the current goal" + str "Found no subterm matching " ++ pr_lconstr c ++ str " in the current goal" let explain_cannot_unify_binding_type m n = - let pm = prterm m in - let pn = prterm n in + let pm = pr_lconstr m in + let pn = pr_lconstr n in str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++ str "which should be unifiable with" ++ brk(1,1) ++ pn @@ -461,36 +461,36 @@ let explain_pretype_error ctx err = let explain_refiner_bad_type arg ty conclty = str"refiner was given an argument" ++ brk(1,1) ++ - prterm arg ++ spc () ++ - str"of type" ++ brk(1,1) ++ prterm ty ++ spc () ++ - str"instead of" ++ brk(1,1) ++ prterm conclty + pr_lconstr arg ++ spc () ++ + str"of type" ++ brk(1,1) ++ pr_lconstr ty ++ spc () ++ + str"instead of" ++ brk(1,1) ++ pr_lconstr conclty let explain_refiner_occur_meta t = - str"cannot refine with term" ++ brk(1,1) ++ prterm t ++ + str"cannot refine with term" ++ brk(1,1) ++ pr_lconstr t ++ spc () ++ str"because there are metavariables, and it is" ++ spc () ++ str"neither an application nor a Case" let explain_refiner_occur_meta_goal t = - str"generated subgoal" ++ brk(1,1) ++ prterm t ++ + str"generated subgoal" ++ brk(1,1) ++ pr_lconstr t ++ spc () ++ str"has metavariables in it" let explain_refiner_cannot_apply t harg = str"in refiner, a term of type " ++ brk(1,1) ++ - prterm t ++ spc () ++ str"could not be applied to" ++ brk(1,1) ++ - prterm harg + pr_lconstr t ++ spc () ++ str"could not be applied to" ++ brk(1,1) ++ + pr_lconstr harg let explain_refiner_not_well_typed c = - str"The term " ++ prterm c ++ str" is not well-typed" + str"The term " ++ pr_lconstr c ++ str" is not well-typed" let explain_intro_needs_product () = str "Introduction tactics needs products" let explain_does_not_occur_in c hyp = - str "The term" ++ spc () ++ prterm c ++ spc () ++ str "does not occur in" ++ + str "The term" ++ spc () ++ pr_lconstr c ++ spc () ++ str "does not occur in" ++ spc () ++ pr_id hyp let explain_non_linear_proof c = - str "cannot refine with term" ++ brk(1,1) ++ prterm c ++ + str "cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++ spc () ++ str"because a metavariable has several occurrences" let explain_refiner_error = function @@ -506,20 +506,20 @@ let explain_refiner_error = function (* Inductive errors *) let error_non_strictly_positive env c v = - let pc = prterm_env env c in - let pv = prterm_env env v in + let pc = pr_lconstr_env env c in + let pv = pr_lconstr_env env v in str "Non strictly positive occurrence of " ++ pv ++ str " in" ++ brk(1,1) ++ pc let error_ill_formed_inductive env c v = - let pc = prterm_env env c in - let pv = prterm_env env v in + let pc = pr_lconstr_env env c in + let pv = pr_lconstr_env env v in str "Not enough arguments applied to the " ++ pv ++ str " in" ++ brk(1,1) ++ pc let error_ill_formed_constructor env c v = - let pc = prterm_env env c in - let pv = prterm_env env v in + let pc = pr_lconstr_env env c in + let pv = pr_lconstr_env env v in str "The conclusion of" ++ brk(1,1) ++ pc ++ brk(1,1) ++ str "is not valid;" ++ brk(1,1) ++ str "it must be built from " ++ pv @@ -532,9 +532,9 @@ let str_of_nth n = | _ -> "th") let error_bad_ind_parameters env c n v1 v2 = - let pc = prterm_env_at_top env c in - let pv1 = prterm_env env v1 in - let pv2 = prterm_env env v2 in + let pc = pr_lconstr_env_at_top env c in + let pv1 = pr_lconstr_env env v1 in + let pv2 = pr_lconstr_env env v2 in str ("The "^(str_of_nth n)^" argument of ") ++ pv2 ++ brk(1,1) ++ str "must be " ++ pv1 ++ str " in" ++ brk(1,1) ++ pc @@ -598,7 +598,7 @@ let explain_recursion_scheme_error = function let explain_bad_pattern ctx cstr ty = let ctx = make_all_name_different ctx in - let pt = prterm_env ctx ty in + let pt = pr_lconstr_env ctx ty in let pc = pr_constructor ctx cstr in str "Found the constructor " ++ pc ++ brk(1,1) ++ str "while matching a term of type " ++ pt ++ brk(1,1) ++ @@ -620,17 +620,17 @@ let explain_wrong_numarg_of_constructor ctx cstr n = let explain_wrong_predicate_arity ctx pred nondep_arity dep_arity= let ctx = make_all_name_different ctx in - let pp = prterm_env ctx pred in + let pp = pr_lconstr_env ctx pred in str "The elimination predicate " ++ spc () ++ pp ++ fnl () ++ str "should be of arity" ++ spc () ++ - prterm_env ctx nondep_arity ++ spc () ++ + pr_lconstr_env ctx nondep_arity ++ spc () ++ str "(for non dependent case) or" ++ - spc () ++ prterm_env ctx dep_arity ++ spc () ++ str "(for dependent case)." + spc () ++ pr_lconstr_env ctx dep_arity ++ spc () ++ str "(for dependent case)." let explain_needs_inversion ctx x t = let ctx = make_all_name_different ctx in - let px = prterm_env ctx x in - let pt = prterm_env ctx t in + let px = pr_lconstr_env ctx x in + let pt = pr_lconstr_env ctx t in str "Sorry, I need inversion to compile pattern matching of term " ++ px ++ str " of type: " ++ pt @@ -651,7 +651,7 @@ let explain_cannot_infer_predicate ctx typs = let ctx = make_all_name_different ctx in let pr_branch (cstr,typ) = let cstr,_ = decompose_app cstr in - str "For " ++ prterm_env ctx cstr ++ str " : " ++ prterm_env ctx typ + str "For " ++ pr_lconstr_env ctx cstr ++ str " : " ++ pr_lconstr_env ctx typ in str "Unable to unify the types found in the branches:" ++ spc () ++ hov 0 (prlist_with_sep pr_fnl pr_branch (Array.to_list typs)) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 6cc72c056..77312604b 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -71,9 +71,9 @@ let show_proof () = prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++ str"Subgoals" ++ fnl () ++ prlist (fun (mv,ty) -> Nameops.pr_meta mv ++ str" -> " ++ - prtype ty ++ fnl ()) + pr_ltype ty ++ fnl ()) meta_types - ++ str"Proof: " ++ prterm (Evarutil.nf_evar evc pfterm)) + ++ str"Proof: " ++ pr_lconstr (Evarutil.nf_evar evc pfterm)) let show_node () = let pts = get_pftreestate () in @@ -638,7 +638,7 @@ let vernac_declare_implicits locqid = function let vernac_reserve idl c = let t = Constrintern.interp_type Evd.empty (Global.env()) c in - let t = Detyping.detype (false,Global.env()) [] [] t in + let t = Detyping.detype false [] [] t in List.iter (fun id -> Reserve.declare_reserved_type id t) idl let make_silent_if_not_pcoq b = @@ -882,11 +882,11 @@ let vernac_print = function | PrintHintDb -> Auto.print_searchtable () | PrintSetoids -> Setoid_replace.print_setoids() | PrintScopes -> - pp (Notation.pr_scopes (Constrextern.without_symbols pr_rawterm)) + pp (Notation.pr_scopes (Constrextern.without_symbols pr_lrawconstr)) | PrintScope s -> - pp (Notation.pr_scope (Constrextern.without_symbols pr_rawterm) s) + pp (Notation.pr_scope (Constrextern.without_symbols pr_lrawconstr) s) | PrintVisibility s -> - pp (Notation.pr_visibility (Constrextern.without_symbols pr_rawterm) s) + pp (Notation.pr_visibility (Constrextern.without_symbols pr_lrawconstr) s) | PrintAbout qid -> msgnl (print_about qid) | PrintImplicit qid -> msg (print_impargs qid) @@ -928,7 +928,7 @@ let vernac_locate = function | LocateModule qid -> print_located_module qid | LocateFile f -> locate_file f | LocateNotation ntn -> - ppnl (Notation.locate_notation (Constrextern.without_symbols pr_rawterm) + ppnl (Notation.locate_notation (Constrextern.without_symbols pr_lrawconstr) (Metasyntax.standardize_locatable_notation ntn)) (********************) diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 42eec8c03..eb9fdae30 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -155,14 +155,14 @@ let send_whelp req s = let command = (fst browser_cmd_fmt) ^ url ^ (snd browser_cmd_fmt) in let _ = run_command (fun x -> x) print_string command in () -let whelp_constr req env c = - let c = detype (false,env) [whelm_special] [] c in +let whelp_constr req c = + let c = detype false [whelm_special] [] c in send_whelp req (make_string uri_of_constr c) let whelp_constr_expr req c = let (sigma,env)= get_current_context () in let _,c = interp_open_constr sigma env c in - whelp_constr req env c + whelp_constr req c let whelp_locate s = send_whelp "locate" s @@ -179,17 +179,17 @@ let locate_inductive r = let on_goal f = let gls = nth_goal_of_pftreestate 1 (get_pftreestate ()) in - f (Global.env()) (it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls)) + f (it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls)) type whelp_request = | Locate of string | Elim of inductive - | Constr of string * env * constr + | Constr of string * constr let whelp = function | Locate s -> whelp_locate s | Elim ind -> whelp_elim ind - | Constr (s,env,c) -> whelp_constr s env c + | Constr (s,c) -> whelp_constr s c VERNAC ARGUMENT EXTEND whelp_constr_request | [ "Match" ] -> [ "match" ] diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli index 1871f3906..4ad615a62 100644 --- a/toplevel/whelp.mli +++ b/toplevel/whelp.mli @@ -19,6 +19,6 @@ open Environ type whelp_request = | Locate of string | Elim of inductive - | Constr of string * env * constr + | Constr of string * constr val whelp : whelp_request -> unit |