aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--.depend168
-rw-r--r--contrib/correctness/pcic.ml5
-rw-r--r--contrib/interface/name_to_ast.ml9
-rw-r--r--contrib/interface/xlate.ml35
-rw-r--r--ide/coq.ml18
-rw-r--r--interp/modintern.ml4
-rw-r--r--interp/reserve.ml21
-rw-r--r--interp/reserve.mli13
-rw-r--r--interp/topconstr.ml4
-rw-r--r--interp/topconstr.mli4
-rw-r--r--library/declaremods.ml4
-rw-r--r--library/declaremods.mli9
-rwxr-xr-xparsing/ast.ml2
-rwxr-xr-xparsing/ast.mli2
-rw-r--r--parsing/g_basevernac.ml469
-rw-r--r--parsing/g_ltac.ml42
-rw-r--r--parsing/g_module.ml44
-rw-r--r--parsing/g_proofs.ml46
-rw-r--r--parsing/g_proofsnew.ml46
-rw-r--r--parsing/g_tactic.ml411
-rw-r--r--parsing/g_tacticnew.ml42
-rw-r--r--parsing/g_vernac.ml458
-rw-r--r--parsing/g_vernacnew.ml458
-rw-r--r--toplevel/command.ml18
-rw-r--r--toplevel/command.mli2
-rw-r--r--toplevel/record.ml10
-rw-r--r--toplevel/record.mli2
-rw-r--r--toplevel/vernacentries.ml29
-rw-r--r--toplevel/vernacexpr.ml108
-rw-r--r--translate/ppconstrnew.ml195
-rw-r--r--translate/ppconstrnew.mli8
-rw-r--r--translate/pptacticnew.ml41
-rw-r--r--translate/ppvernacnew.ml103
33 files changed, 567 insertions, 463 deletions
diff --git a/.depend b/.depend
index a4d3e55bc..8e38e47b8 100644
--- a/.depend
+++ b/.depend
@@ -18,7 +18,7 @@ interp/genarg.cmi: pretyping/evd.cmi library/libnames.cmi kernel/names.cmi \
interp/modintern.cmi: kernel/declarations.cmi kernel/entries.cmi \
kernel/environ.cmi interp/topconstr.cmi
interp/ppextend.cmi: kernel/names.cmi lib/pp.cmi
-interp/reserve.cmi: kernel/names.cmi pretyping/rawterm.cmi
+interp/reserve.cmi: kernel/names.cmi pretyping/rawterm.cmi lib/util.cmi
interp/symbols.cmi: lib/bignat.cmi pretyping/classops.cmi \
library/libnames.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
interp/ppextend.cmi pretyping/rawterm.cmi interp/topconstr.cmi \
@@ -45,10 +45,10 @@ kernel/indtypes.cmi: kernel/declarations.cmi kernel/entries.cmi \
kernel/univ.cmi
kernel/inductive.cmi: kernel/declarations.cmi kernel/environ.cmi \
kernel/names.cmi kernel/term.cmi kernel/univ.cmi
-kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \
- kernel/environ.cmi
kernel/modops.cmi: kernel/declarations.cmi kernel/entries.cmi \
kernel/environ.cmi kernel/names.cmi kernel/univ.cmi lib/util.cmi
+kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \
+ kernel/environ.cmi
kernel/names.cmi: lib/pp.cmi lib/predicate.cmi
kernel/reduction.cmi: kernel/environ.cmi kernel/sign.cmi kernel/term.cmi \
kernel/univ.cmi
@@ -68,9 +68,6 @@ kernel/typeops.cmi: kernel/entries.cmi kernel/environ.cmi kernel/names.cmi \
kernel/univ.cmi: kernel/names.cmi lib/pp.cmi
lib/bignat.cmi: lib/pp.cmi
lib/pp.cmi: lib/pp_control.cmi
-lib/rtree.cmi: lib/pp.cmi
-lib/system.cmi: lib/pp.cmi
-lib/util.cmi: lib/pp.cmi
library/declare.cmi: kernel/cooking.cmi library/decl_kinds.cmo \
kernel/declarations.cmi library/dischargedhypsmap.cmi kernel/entries.cmi \
kernel/indtypes.cmi library/libnames.cmi library/libobject.cmi \
@@ -78,7 +75,7 @@ library/declare.cmi: kernel/cooking.cmi library/decl_kinds.cmo \
kernel/sign.cmi kernel/term.cmi kernel/univ.cmi
library/declaremods.cmi: kernel/entries.cmi kernel/environ.cmi \
library/lib.cmi library/libnames.cmi library/libobject.cmi \
- kernel/names.cmi lib/pp.cmi kernel/safe_typing.cmi
+ kernel/names.cmi lib/pp.cmi kernel/safe_typing.cmi lib/util.cmi
library/dischargedhypsmap.cmi: kernel/environ.cmi library/libnames.cmi \
library/nametab.cmi kernel/term.cmi
library/global.cmi: kernel/declarations.cmi kernel/entries.cmi \
@@ -99,6 +96,9 @@ library/library.cmi: library/libnames.cmi library/libobject.cmi \
library/nameops.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi
library/nametab.cmi: library/libnames.cmi kernel/names.cmi lib/pp.cmi \
lib/util.cmi
+lib/rtree.cmi: lib/pp.cmi
+lib/system.cmi: lib/pp.cmi
+lib/util.cmi: lib/pp.cmi
parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi interp/genarg.cmi \
library/libnames.cmi kernel/names.cmi lib/pp.cmi interp/topconstr.cmi \
lib/util.cmi
@@ -314,11 +314,11 @@ toplevel/recordobj.cmi: library/libnames.cmi proofs/tacexpr.cmo
toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
kernel/term.cmi
toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi
-toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo
toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \
library/libnames.cmi kernel/names.cmi kernel/term.cmi \
interp/topconstr.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi
toplevel/vernacinterp.cmi: proofs/tacexpr.cmo
+toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo
translate/ppconstrnew.cmi: parsing/coqast.cmi kernel/environ.cmi \
parsing/extend.cmi interp/genarg.cmi library/libnames.cmi \
kernel/names.cmi pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi \
@@ -338,11 +338,11 @@ contrib/cc/ccalgo.cmi: kernel/names.cmi kernel/term.cmi
contrib/cc/ccproof.cmi: contrib/cc/ccalgo.cmi kernel/names.cmi
contrib/correctness/past.cmi: kernel/names.cmi contrib/correctness/ptype.cmi \
kernel/term.cmi interp/topconstr.cmi lib/util.cmi
-contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
- pretyping/rawterm.cmi
contrib/correctness/pcicenv.cmi: kernel/names.cmi \
contrib/correctness/penv.cmi contrib/correctness/prename.cmi \
kernel/sign.cmi kernel/term.cmi
+contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
+ pretyping/rawterm.cmi
contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/past.cmi \
contrib/correctness/ptype.cmi
contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi
@@ -486,6 +486,14 @@ ide/config_lexer.cmo: ide/config_parser.cmi lib/util.cmi
ide/config_lexer.cmx: ide/config_parser.cmx lib/util.cmx
ide/config_parser.cmo: lib/util.cmi ide/config_parser.cmi
ide/config_parser.cmx: lib/util.cmx ide/config_parser.cmi
+ide/coqide.cmo: ide/blaster_window.cmo ide/command_windows.cmi ide/coq.cmi \
+ ide/coq_commands.cmo ide/find_phrase.cmo ide/highlight.cmo \
+ ide/ideutils.cmi proofs/pfedit.cmi ide/preferences.cmi ide/undo.cmi \
+ lib/util.cmi toplevel/vernacexpr.cmo ide/coqide.cmi
+ide/coqide.cmx: ide/blaster_window.cmx ide/command_windows.cmx ide/coq.cmx \
+ ide/coq_commands.cmx ide/find_phrase.cmx ide/highlight.cmx \
+ ide/ideutils.cmx proofs/pfedit.cmx ide/preferences.cmx ide/undo.cmx \
+ lib/util.cmx toplevel/vernacexpr.cmx ide/coqide.cmi
ide/coq.cmo: toplevel/cerrors.cmi config/coq_config.cmi toplevel/coqtop.cmi \
kernel/declarations.cmi kernel/environ.cmi pretyping/evarutil.cmi \
pretyping/evd.cmi library/global.cmi tactics/hipattern.cmi \
@@ -508,14 +516,6 @@ ide/coq.cmx: toplevel/cerrors.cmx config/coq_config.cmx toplevel/coqtop.cmx \
toplevel/vernacentries.cmx toplevel/vernacexpr.cmx ide/coq.cmi
ide/coq_tactics.cmo: ide/coq_tactics.cmi
ide/coq_tactics.cmx: ide/coq_tactics.cmi
-ide/coqide.cmo: ide/blaster_window.cmo ide/command_windows.cmi ide/coq.cmi \
- ide/coq_commands.cmo ide/find_phrase.cmo ide/highlight.cmo \
- ide/ideutils.cmi proofs/pfedit.cmi ide/preferences.cmi ide/undo.cmi \
- lib/util.cmi toplevel/vernacexpr.cmo ide/coqide.cmi
-ide/coqide.cmx: ide/blaster_window.cmx ide/command_windows.cmx ide/coq.cmx \
- ide/coq_commands.cmx ide/find_phrase.cmx ide/highlight.cmx \
- ide/ideutils.cmx proofs/pfedit.cmx ide/preferences.cmx ide/undo.cmx \
- lib/util.cmx toplevel/vernacexpr.cmx ide/coqide.cmi
ide/find_phrase.cmo: ide/ideutils.cmi
ide/find_phrase.cmx: ide/ideutils.cmx
ide/highlight.cmo: ide/ideutils.cmi
@@ -591,10 +591,10 @@ interp/ppextend.cmo: kernel/names.cmi lib/pp.cmi lib/util.cmi \
interp/ppextend.cmx: kernel/names.cmx lib/pp.cmx lib/util.cmx \
interp/ppextend.cmi
interp/reserve.cmo: library/lib.cmi library/libobject.cmi library/nameops.cmi \
- kernel/names.cmi lib/options.cmi pretyping/rawterm.cmi \
+ kernel/names.cmi lib/options.cmi lib/pp.cmi pretyping/rawterm.cmi \
library/summary.cmi lib/util.cmi interp/reserve.cmi
interp/reserve.cmx: library/lib.cmx library/libobject.cmx library/nameops.cmx \
- kernel/names.cmx lib/options.cmx pretyping/rawterm.cmx \
+ kernel/names.cmx lib/options.cmx lib/pp.cmx pretyping/rawterm.cmx \
library/summary.cmx lib/util.cmx interp/reserve.cmi
interp/symbols.cmo: lib/bignat.cmi pretyping/classops.cmi library/global.cmi \
lib/gmap.cmi lib/gmapl.cmi library/lib.cmi library/libnames.cmi \
@@ -666,6 +666,12 @@ kernel/inductive.cmo: kernel/declarations.cmi kernel/environ.cmi \
kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \
kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx kernel/inductive.cmi
+kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
+ kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
+ kernel/univ.cmi lib/util.cmi kernel/modops.cmi
+kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
+ kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
+ kernel/univ.cmx lib/util.cmx kernel/modops.cmi
kernel/mod_typing.cmo: kernel/declarations.cmi kernel/entries.cmi \
kernel/environ.cmi kernel/modops.cmi kernel/names.cmi \
kernel/reduction.cmi kernel/subtyping.cmi kernel/term_typing.cmi \
@@ -674,12 +680,6 @@ kernel/mod_typing.cmx: kernel/declarations.cmx kernel/entries.cmx \
kernel/environ.cmx kernel/modops.cmx kernel/names.cmx \
kernel/reduction.cmx kernel/subtyping.cmx kernel/term_typing.cmx \
kernel/typeops.cmx kernel/univ.cmx lib/util.cmx kernel/mod_typing.cmi
-kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
- kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
- kernel/univ.cmi lib/util.cmi kernel/modops.cmi
-kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
- kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
- kernel/univ.cmx lib/util.cmx kernel/modops.cmi
kernel/names.cmo: lib/hashcons.cmi lib/options.cmi lib/pp.cmi \
lib/predicate.cmi lib/util.cmi kernel/names.cmi
kernel/names.cmx: lib/hashcons.cmx lib/options.cmx lib/pp.cmx \
@@ -760,10 +760,10 @@ lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi
lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi
lib/explore.cmo: lib/explore.cmi
lib/explore.cmx: lib/explore.cmi
-lib/gmap.cmo: lib/gmap.cmi
-lib/gmap.cmx: lib/gmap.cmi
lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi
lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi
+lib/gmap.cmo: lib/gmap.cmi
+lib/gmap.cmx: lib/gmap.cmi
lib/gset.cmo: lib/gset.cmi
lib/gset.cmx: lib/gset.cmi
lib/hashcons.cmo: lib/hashcons.cmi
@@ -772,24 +772,14 @@ lib/heap.cmo: lib/heap.cmi
lib/heap.cmx: lib/heap.cmi
lib/options.cmo: lib/util.cmi lib/options.cmi
lib/options.cmx: lib/util.cmx lib/options.cmi
-lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi
-lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi
lib/pp_control.cmo: lib/pp_control.cmi
lib/pp_control.cmx: lib/pp_control.cmi
+lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi
+lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi
lib/predicate.cmo: lib/predicate.cmi
lib/predicate.cmx: lib/predicate.cmi
lib/profile.cmo: lib/profile.cmi
lib/profile.cmx: lib/profile.cmi
-lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi
-lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi
-lib/stamps.cmo: lib/stamps.cmi
-lib/stamps.cmx: lib/stamps.cmi
-lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi
-lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi
-lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi
-lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi
-lib/util.cmo: lib/pp.cmi lib/util.cmi
-lib/util.cmx: lib/pp.cmx lib/util.cmi
library/declare.cmo: library/decl_kinds.cmo kernel/declarations.cmi \
library/dischargedhypsmap.cmi kernel/entries.cmi kernel/environ.cmi \
library/global.cmi library/impargs.cmi kernel/indtypes.cmi \
@@ -896,6 +886,16 @@ library/states.cmx: library/lib.cmx library/library.cmx library/summary.cmx \
lib/system.cmx library/states.cmi
library/summary.cmo: lib/dyn.cmi lib/pp.cmi lib/util.cmi library/summary.cmi
library/summary.cmx: lib/dyn.cmx lib/pp.cmx lib/util.cmx library/summary.cmi
+lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi
+lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi
+lib/stamps.cmo: lib/stamps.cmi
+lib/stamps.cmx: lib/stamps.cmi
+lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi
+lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi
+lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi
+lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi
+lib/util.cmo: lib/pp.cmi lib/util.cmi
+lib/util.cmx: lib/pp.cmx lib/util.cmi
parsing/argextend.cmo: parsing/ast.cmi interp/genarg.cmi parsing/pcoq.cmi \
parsing/q_coqast.cmo parsing/q_util.cmi lib/util.cmi \
toplevel/vernacexpr.cmo
@@ -1962,10 +1962,10 @@ tactics/termdn.cmo: tactics/dn.cmi library/libnames.cmi library/nameops.cmi \
tactics/termdn.cmx: tactics/dn.cmx library/libnames.cmx library/nameops.cmx \
kernel/names.cmx library/nametab.cmx pretyping/pattern.cmx \
pretyping/rawterm.cmx kernel/term.cmx lib/util.cmx tactics/termdn.cmi
-tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi
-tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx
tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo
tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx
+tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi
+tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx
tools/gallina.cmo: tools/gallina_lexer.cmo
tools/gallina.cmx: tools/gallina_lexer.cmx
toplevel/cerrors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \
@@ -2176,20 +2176,6 @@ toplevel/toplevel.cmx: toplevel/cerrors.cmx library/lib.cmx \
toplevel/vernac.cmx toplevel/vernacexpr.cmx toplevel/toplevel.cmi
toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi
toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi
-toplevel/vernac.cmo: interp/constrextern.cmi interp/constrintern.cmi \
- parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi library/library.cmi \
- kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
- lib/pp.cmi translate/ppvernacnew.cmi proofs/refiner.cmi \
- library/states.cmi lib/system.cmi tactics/tacinterp.cmi \
- proofs/tacmach.cmi lib/util.cmi toplevel/vernacentries.cmi \
- toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi
-toplevel/vernac.cmx: interp/constrextern.cmx interp/constrintern.cmx \
- parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx library/library.cmx \
- kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
- lib/pp.cmx translate/ppvernacnew.cmx proofs/refiner.cmx \
- library/states.cmx lib/system.cmx tactics/tacinterp.cmx \
- proofs/tacmach.cmx lib/util.cmx toplevel/vernacentries.cmx \
- toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi
toplevel/vernacentries.cmo: tactics/auto.cmi toplevel/class.cmi \
pretyping/classops.cmi toplevel/command.cmi interp/constrextern.cmi \
interp/constrintern.cmi library/decl_kinds.cmo library/declaremods.cmi \
@@ -2252,6 +2238,20 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx \
kernel/names.cmx lib/options.cmx lib/pp.cmx proofs/proof_type.cmx \
proofs/tacexpr.cmx tactics/tacinterp.cmx lib/util.cmx \
toplevel/vernacexpr.cmx toplevel/vernacinterp.cmi
+toplevel/vernac.cmo: interp/constrextern.cmi interp/constrintern.cmi \
+ parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi library/library.cmi \
+ kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
+ lib/pp.cmi translate/ppvernacnew.cmi proofs/refiner.cmi \
+ library/states.cmi lib/system.cmi tactics/tacinterp.cmi \
+ proofs/tacmach.cmi lib/util.cmi toplevel/vernacentries.cmi \
+ toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi
+toplevel/vernac.cmx: interp/constrextern.cmx interp/constrintern.cmx \
+ parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx library/library.cmx \
+ kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
+ lib/pp.cmx translate/ppvernacnew.cmx proofs/refiner.cmx \
+ library/states.cmx lib/system.cmx tactics/tacinterp.cmx \
+ proofs/tacmach.cmx lib/util.cmx toplevel/vernacentries.cmx \
+ toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi
translate/ppconstrnew.cmo: parsing/ast.cmi lib/bignat.cmi \
interp/constrextern.cmi interp/constrintern.cmi parsing/coqast.cmi \
pretyping/evd.cmi interp/genarg.cmi library/global.cmi library/lib.cmi \
@@ -2338,6 +2338,18 @@ contrib/cc/cctac.cmx: contrib/cc/ccalgo.cmx contrib/cc/ccproof.cmx \
kernel/sign.cmx tactics/tacinterp.cmx proofs/tacmach.cmx \
tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \
pretyping/termops.cmx lib/util.cmx
+contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
+ contrib/correctness/past.cmi contrib/correctness/penv.cmi \
+ contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
+ contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
+ contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \
+ kernel/univ.cmi contrib/correctness/pcicenv.cmi
+contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
+ contrib/correctness/past.cmi contrib/correctness/penv.cmx \
+ contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
+ contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
+ contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
+ kernel/univ.cmx contrib/correctness/pcicenv.cmi
contrib/correctness/pcic.cmo: kernel/declarations.cmi library/declare.cmi \
pretyping/detyping.cmi kernel/entries.cmi library/global.cmi \
kernel/indtypes.cmi library/libnames.cmi library/nameops.cmi \
@@ -2354,18 +2366,6 @@ contrib/correctness/pcic.cmx: kernel/declarations.cmx library/declare.cmx \
kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \
interp/topconstr.cmx kernel/typeops.cmx lib/util.cmx \
toplevel/vernacexpr.cmx contrib/correctness/pcic.cmi
-contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
- contrib/correctness/past.cmi contrib/correctness/penv.cmi \
- contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
- contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
- contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \
- kernel/univ.cmi contrib/correctness/pcicenv.cmi
-contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
- contrib/correctness/past.cmi contrib/correctness/penv.cmx \
- contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
- contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
- contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
- kernel/univ.cmx contrib/correctness/pcicenv.cmi
contrib/correctness/pdb.cmo: interp/constrintern.cmi library/global.cmi \
kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \
contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
@@ -3052,6 +3052,14 @@ contrib/interface/pbp.cmx: interp/coqlib.cmx kernel/environ.cmx \
proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
kernel/term.cmx pretyping/termops.cmx interp/topconstr.cmx \
pretyping/typing.cmx lib/util.cmx contrib/interface/pbp.cmi
+contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
+ parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
+ parsing/printer.cmi contrib/interface/translate.cmi \
+ contrib/interface/vtp.cmi contrib/interface/xlate.cmi
+contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
+ parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
+ parsing/printer.cmx contrib/interface/translate.cmx \
+ contrib/interface/vtp.cmx contrib/interface/xlate.cmx
contrib/interface/showproof.cmo: proofs/clenv.cmi interp/constrintern.cmi \
parsing/coqast.cmi kernel/declarations.cmi kernel/environ.cmi \
pretyping/evd.cmi interp/genarg.cmi library/global.cmi \
@@ -3076,14 +3084,6 @@ contrib/interface/showproof.cmx: proofs/clenv.cmx interp/constrintern.cmx \
pretyping/termops.cmx contrib/interface/translate.cmx \
pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx \
contrib/interface/showproof.cmi
-contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
- parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
- parsing/printer.cmi contrib/interface/translate.cmi \
- contrib/interface/vtp.cmi contrib/interface/xlate.cmi
-contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
- parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
- parsing/printer.cmx contrib/interface/translate.cmx \
- contrib/interface/vtp.cmx contrib/interface/xlate.cmx
contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
interp/constrextern.cmi contrib/interface/ctast.cmo kernel/environ.cmi \
pretyping/evarutil.cmi pretyping/evd.cmi library/libobject.cmi \
@@ -3258,12 +3258,12 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \
proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \
proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
kernel/term.cmx lib/util.cmx
-contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi
-contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx
contrib/xml/acic2Xml.cmo: contrib/xml/acic.cmo contrib/xml/cic2acic.cmo \
kernel/names.cmi kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi
contrib/xml/acic2Xml.cmx: contrib/xml/acic.cmx contrib/xml/cic2acic.cmx \
kernel/names.cmx kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx
+contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi
+contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx
contrib/xml/cic2acic.cmo: contrib/xml/acic.cmo library/declare.cmi \
library/dischargedhypsmap.cmi contrib/xml/doubleTypeInference.cmi \
kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
@@ -3318,8 +3318,6 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/acic.cmx contrib/xml/acic2Xml.cmx \
contrib/xml/xml.cmx
contrib/xml/unshare.cmo: contrib/xml/unshare.cmi
contrib/xml/unshare.cmx: contrib/xml/unshare.cmi
-contrib/xml/xml.cmo: contrib/xml/xml.cmi
-contrib/xml/xml.cmx: contrib/xml/xml.cmi
contrib/xml/xmlcommand.cmo: contrib/xml/acic.cmo contrib/xml/acic2Xml.cmo \
contrib/xml/cic2acic.cmo library/decl_kinds.cmo kernel/declarations.cmi \
library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \
@@ -3344,10 +3342,8 @@ contrib/xml/xmlentries.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \
contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
parsing/extend.cmx interp/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \
lib/util.cmx toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx
-ide/utils/configwin.cmo: ide/utils/configwin_ihm.cmo \
- ide/utils/configwin_types.cmo ide/utils/configwin.cmi
-ide/utils/configwin.cmx: ide/utils/configwin_ihm.cmx \
- ide/utils/configwin_types.cmx ide/utils/configwin.cmi
+contrib/xml/xml.cmo: contrib/xml/xml.cmi
+contrib/xml/xml.cmx: contrib/xml/xml.cmi
ide/utils/configwin_html_config.cmo: ide/utils/configwin_ihm.cmo \
ide/utils/configwin_messages.cmo ide/utils/configwin_types.cmo \
ide/utils/uoptions.cmi
@@ -3358,6 +3354,10 @@ ide/utils/configwin_ihm.cmo: ide/utils/configwin_messages.cmo \
ide/utils/configwin_types.cmo ide/utils/okey.cmi ide/utils/uoptions.cmi
ide/utils/configwin_ihm.cmx: ide/utils/configwin_messages.cmx \
ide/utils/configwin_types.cmx ide/utils/okey.cmx ide/utils/uoptions.cmx
+ide/utils/configwin.cmo: ide/utils/configwin_ihm.cmo \
+ ide/utils/configwin_types.cmo ide/utils/configwin.cmi
+ide/utils/configwin.cmx: ide/utils/configwin_ihm.cmx \
+ ide/utils/configwin_types.cmx ide/utils/configwin.cmi
ide/utils/configwin_types.cmo: ide/utils/configwin_keys.cmo \
ide/utils/uoptions.cmi
ide/utils/configwin_types.cmx: ide/utils/configwin_keys.cmx \
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index db2617da3..77d516a13 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -56,11 +56,12 @@ let tuple_n n =
(fun i ->
let id = make_ident ("proj_" ^ string_of_int n ^ "_") (Some i) in
let id' = make_ident "T" (Some i) in
- (false, Vernacexpr.AssumExpr (id, mkIdentC id')))
+ (false, Vernacexpr.AssumExpr ((dummy_loc,id), mkIdentC id')))
l1n
in
let cons = make_ident "Build_tuple_" (Some n) in
- Record.definition_structure ((false, id), params, fields, cons, mk_Set)
+ Record.definition_structure
+ ((false, (dummy_loc,id)), params, fields, cons, mk_Set)
(*s [(sig_n n)] generates the inductive
\begin{verbatim}
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index cdf83b22b..29582c382 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -105,7 +105,7 @@ let convert_constructors envpar names types =
array_map2
(fun n t ->
let coercion_flag = false (* arbitrary *) in
- (coercion_flag, (n, extern_constr true envpar t)))
+ (coercion_flag, ((dummy_loc,n), extern_constr true envpar t)))
names types in
Array.to_list array_idC;;
@@ -117,7 +117,7 @@ let convert_one_inductive sp tyi =
let env = Global.env () in
let envpar = push_rel_context params env in
let sp = sp_of_global (IndRef (sp, tyi)) in
- (basename sp, None,
+ ((dummy_loc,basename sp), None,
convert_env(List.rev params),
(extern_constr true envpar arity),
convert_constructors envpar cstrnames cstrtypes);;
@@ -154,12 +154,13 @@ let make_variable_ast name typ implicits =
*)
let make_variable_ast name typ implicits =
(VernacAssumption
- ((Local,Definitional), [false,(name, constr_to_ast (body_of_type typ))]))
+ ((Local,Definitional),
+ [false,((dummy_loc,name), constr_to_ast (body_of_type typ))]))
::(implicits_to_ast_list implicits);;
let make_definition_ast name c typ implicits =
- VernacDefinition ((Global,Definition), name, DefineBody ([], None,
+ VernacDefinition ((Global,Definition), (dummy_loc,name), DefineBody ([], None,
(constr_to_ast c), Some (constr_to_ast (body_of_type typ))),
(fun _ _ -> ()))
::(implicits_to_ast_list implicits);;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 1739240e0..35357d3ab 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1243,19 +1243,19 @@ let xlate_check =
| _ -> xlate_error "xlate_check";;
let build_constructors l =
- let f (coe,(id,c)) =
+ let f (coe,((_,id),c)) =
if coe then xlate_error "TODO: coercions in constructors"
else CT_constr (xlate_ident id, xlate_formula c) in
CT_constr_list (List.map f l)
let build_record_field_list l =
let build_record_field (coe,d) = match d with
- | AssumExpr (id,c) ->
+ | AssumExpr ((_,id),c) ->
if coe then CT_constr_coercion (xlate_ident id, xlate_formula c)
else
CT_coerce_CONSTR_to_RECCONSTR
(CT_constr (xlate_ident id, xlate_formula c))
- | DefExpr (id,c,topt) ->
+ | DefExpr ((_,id),c,topt) ->
xlate_error "TODO: manifest fields in Record" in
CT_recconstr_list (List.map build_record_field l);;
@@ -1281,7 +1281,7 @@ let cvt_optional_eval_for_definition c1 optional_eval =
xlate_formula c1))
let cvt_vernac_binder = function
- | (id,c) ->
+ | ((_,id),c) ->
CT_binder(CT_id_opt_ne_list (xlate_ident_opt (Some id),[]),xlate_formula c)
let cvt_vernac_binders args =
@@ -1418,10 +1418,10 @@ let xlate_vernac =
CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"), ctv_ID_OPT_NONE)
| VernacEndProof (Proved (false,None)) ->
CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Definition"), ctv_ID_OPT_NONE)
- | VernacEndProof (Proved (b,Some (s, Some kind))) ->
+ | VernacEndProof (Proved (b,Some ((_,s), Some kind))) ->
CT_save (CT_coerce_THM_to_THM_OPT (xlate_thm kind),
ctf_ID_OPT_SOME (xlate_ident s))
- | VernacEndProof (Proved (b,Some (s,None))) ->
+ | VernacEndProof (Proved (b,Some ((_,s),None))) ->
CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"),
ctf_ID_OPT_SOME (xlate_ident s))
| VernacEndProof Admitted -> xlate_error "TODO: Admitted"
@@ -1478,21 +1478,21 @@ let xlate_vernac =
| PrintVisibility _ -> xlate_error "TODO: Print Visibility"
| PrintAbout _ -> xlate_error "TODO: Print About"
| _ -> xlate_error "TODO: Print")
- | VernacBeginSection id ->
+ | VernacBeginSection (_,id) ->
CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id))
- | VernacEndSegment id -> CT_section_end (xlate_ident id)
- | VernacStartTheoremProof (k, s, ([],c), _, _) ->
+ | VernacEndSegment (_,id) -> CT_section_end (xlate_ident id)
+ | VernacStartTheoremProof (k, (_,s), ([],c), _, _) ->
CT_coerce_THEOREM_GOAL_to_COMMAND(
CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), xlate_ident s,xlate_formula c))
| VernacStartTheoremProof (k, s, (bl,c), _, _) ->
xlate_error "TODO: VernacStartTheoremProof"
| VernacSuspend -> CT_suspend
| VernacResume idopt -> CT_resume (xlate_ident_opt (option_app snd idopt))
- | VernacDefinition ((k,_),s,ProveBody (bl,typ),_) ->
+ | VernacDefinition ((k,_),(_,s),ProveBody (bl,typ),_) ->
if bl <> [] then xlate_error "TODO: Def bindings";
CT_coerce_THEOREM_GOAL_to_COMMAND(
CT_theorem_goal (CT_coerce_DEFN_to_DEFN_OR_THM (xlate_defn k), xlate_ident s,xlate_formula typ))
- | VernacDefinition ((kind,_),s,DefineBody(bl,red_option,c,typ_opt),_) ->
+ | VernacDefinition ((kind,_),(_,s),DefineBody(bl,red_option,c,typ_opt),_) ->
CT_definition
(xlate_defn kind, xlate_ident s, xlate_binder_list bl,
cvt_optional_eval_for_definition c red_option,
@@ -1513,8 +1513,9 @@ let xlate_vernac =
| (*Record from tactics/Record.v *)
VernacRecord
- (_, (add_coercion, s), binders, CSort (_,c1), rec_constructor_or_none, field_list) ->
- let record_constructor = xlate_ident_opt rec_constructor_or_none in
+ (_, (add_coercion, (_,s)), binders, CSort (_,c1), rec_constructor_or_none, field_list) ->
+ let record_constructor =
+ xlate_ident_opt (option_app snd rec_constructor_or_none) in
CT_record
((if add_coercion then CT_coercion_atm else
CT_coerce_NONE_to_COERCION_OPT(CT_none)),
@@ -1555,7 +1556,7 @@ let xlate_vernac =
*)
| VernacInductive (isind, lmi) ->
let co_or_ind = if isind then "Inductive" else "CoInductive" in
- let strip_mutind (s, notopt, parameters, c, constructors) =
+ let strip_mutind ((_,s), notopt, parameters, c, constructors) =
if notopt = None then
CT_ind_spec
(xlate_ident s, xlate_binder_list parameters, xlate_formula c,
@@ -1585,14 +1586,14 @@ let xlate_vernac =
(CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi))
| VernacScheme [] -> xlate_error "induction scheme"
| VernacScheme (lm :: lmi) ->
- let strip_ind (id, depstr, inde, sort) =
+ let strip_ind ((_,id), depstr, inde, sort) =
CT_scheme_spec
(xlate_ident id, xlate_dep depstr,
CT_coerce_ID_to_FORMULA (loc_qualid_to_ct_ID inde),
xlate_sort sort) in
CT_ind_scheme
(CT_scheme_spec_list (strip_ind lm, List.map strip_ind lmi))
- | VernacSyntacticDefinition (id, c, nopt) ->
+ | VernacSyntacticDefinition ((_,id), c, nopt) ->
CT_syntax_macro (xlate_ident id, xlate_formula c, xlate_int_opt nopt)
| VernacRequire (None, spec, lid) -> xlate_error "TODO: Read Module"
| VernacRequire (Some impexp, spec, [id]) ->
@@ -1653,7 +1654,7 @@ let xlate_vernac =
CT_coercion (local_opt, id_opt, loc_qualid_to_ct_ID id1,
xlate_class id2, xlate_class id3)
- | VernacIdentityCoercion (s, id1, id2, id3) ->
+ | VernacIdentityCoercion (s, (_,id1), id2, id3) ->
let id_opt = CT_identity in
let local_opt =
match s with
diff --git a/ide/coq.ml b/ide/coq.ml
index f8467f4f2..c6aa11432 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -312,16 +312,16 @@ let word_class s =
type reset_info = NoReset | Reset of Names.identifier * bool ref
let compute_reset_info = function
- | VernacDefinition (_, id, DefineBody _, _)
- | VernacBeginSection id
- | VernacDefineModule (id, _, _, _)
- | VernacDeclareModule (id, _, _, _)
- | VernacDeclareModuleType (id, _, _)
- | VernacAssumption (_, (_,(id,_))::_)
- | VernacInductive (_, (id,_,_,_,_) :: _) ->
+ | VernacDefinition (_, (_,id), DefineBody _, _)
+ | VernacBeginSection (_,id)
+ | VernacDefineModule ((_,id), _, _, _)
+ | VernacDeclareModule ((_,id), _, _, _)
+ | VernacDeclareModuleType ((_,id), _, _)
+ | VernacAssumption (_, (_,((_,id),_))::_)
+ | VernacInductive (_, ((_,id),_,_,_,_) :: _) ->
Reset (id, ref true)
- | VernacDefinition (_, id, ProveBody _, _)
- | VernacStartTheoremProof (_, id, _, _, _) ->
+ | VernacDefinition (_, (_,id), ProveBody _, _)
+ | VernacStartTheoremProof (_, (_,id), _, _, _) ->
Reset (id, ref false)
| _ -> NoReset
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 8a0c8e545..a8c0b22f3 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -79,9 +79,9 @@ let lookup_modtype (loc,qid) =
Modops.error_not_a_modtype_loc loc (string_of_qualid qid)
let transl_with_decl env = function
- | CWith_Module (id,qid) ->
+ | CWith_Module ((_,id),qid) ->
With_Module (id,lookup_module qid)
- | CWith_Definition (id,c) ->
+ | CWith_Definition ((_,id),c) ->
With_Definition (id,interp_constr Evd.empty env c)
let rec interp_modtype env = function
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 8b759b6aa..ed4cdba39 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -1,6 +1,17 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
(* Reserved names *)
open Util
+open Pp
open Names
open Nameops
open Summary
@@ -24,13 +35,15 @@ let _ =
Summary.survive_module = false;
Summary.survive_section = false }
-let declare_reserved_type id t =
+let declare_reserved_type (loc,id) t =
if id <> root_of_id id then
- error ((string_of_id id)^
- " is not reservable: it must have no trailing digits, quote, or _");
+ user_err_loc(loc,"declare_reserved_type",
+ (pr_id id ++ str
+ " is not reservable: it must have no trailing digits, quote, or _"));
begin try
let _ = Idmap.find id !reserve_table in
- error ((string_of_id id)^" is already bound to a type")
+ user_err_loc(loc,"declare_reserved_type",
+ (pr_id id++str" is already bound to a type"))
with Not_found -> () end;
add_anonymous_leaf (in_reserved (id,t))
diff --git a/interp/reserve.mli b/interp/reserve.mli
index 0c60caf9b..2f55e2e6b 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -1,6 +1,17 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+open Util
open Names
open Rawterm
-val declare_reserved_type : identifier -> rawconstr -> unit
+val declare_reserved_type : identifier located -> rawconstr -> unit
val find_reserved_type : identifier -> rawconstr
val anonymize_if_reserved : name -> rawconstr -> rawconstr
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 3e4d3684d..1e8a10a87 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -538,8 +538,8 @@ let rec replace_vars_constr_expr l = function
(* Concrete syntax for modules and modules types *)
type with_declaration_ast =
- | CWith_Module of identifier * qualid located
- | CWith_Definition of identifier * constr_expr
+ | CWith_Module of identifier located * qualid located
+ | CWith_Definition of identifier located * constr_expr
type module_type_ast =
| CMTEident of qualid located
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 241d84687..65beaa511 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -149,8 +149,8 @@ val local_binders_length : local_binder list -> int
(* Concrete syntax for modules and modules types *)
type with_declaration_ast =
- | CWith_Module of identifier * qualid located
- | CWith_Definition of identifier * constr_expr
+ | CWith_Module of identifier located * qualid located
+ | CWith_Definition of identifier located * constr_expr
type module_type_ast =
| CMTEident of qualid located
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 305024c3d..579182a60 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -429,9 +429,9 @@ let rec get_some_body mty env = match mty with
let intern_args interp_modtype (env,oldargs) (idl,arg) =
let lib_dir = Lib.library_dp() in
- let mbids = List.map (fun id -> make_mbid lib_dir (string_of_id id)) idl in
+ let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in
let mty = interp_modtype env arg in
- let dirs = List.map (fun id -> make_dirpath [id]) idl in
+ let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in
let mps = List.map (fun mbid -> MPbound mbid) mbids in
let substobjs = get_modtype_substobjs mty in
let substituted's =
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 94144d625..ff3268898 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -9,6 +9,7 @@
(*i $Id$ i*)
(*i*)
+open Util
open Names
open Entries
open Environ
@@ -38,12 +39,12 @@ open Lib
val declare_module :
(env -> 'modtype -> module_type_entry) -> (env -> 'modexpr -> module_expr) ->
identifier ->
- (identifier list * 'modtype) list -> ('modtype * bool) option ->
+ (identifier located list * 'modtype) list -> ('modtype * bool) option ->
'modexpr option -> unit
val start_module : (env -> 'modtype -> module_type_entry) ->
identifier ->
- (identifier list * 'modtype) list -> ('modtype * bool) option ->
+ (identifier located list * 'modtype) list -> ('modtype * bool) option ->
unit
val end_module : identifier -> unit
@@ -53,10 +54,10 @@ val end_module : identifier -> unit
(*s Module types *)
val declare_modtype : (env -> 'modtype -> module_type_entry) ->
- identifier -> (identifier list * 'modtype) list -> 'modtype -> unit
+ identifier -> (identifier located list * 'modtype) list -> 'modtype -> unit
val start_modtype : (env -> 'modtype -> module_type_entry) ->
- identifier -> (identifier list * 'modtype) list -> unit
+ identifier -> (identifier located list * 'modtype) list -> unit
val end_modtype : identifier -> unit
diff --git a/parsing/ast.ml b/parsing/ast.ml
index 869f55bb0..c0120177d 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -229,7 +229,7 @@ let coerce_to_id_ast a = match coerce_to_var a with
str"This expression should be a simple identifier")
let coerce_to_id = function
- | CRef (Ident (_,id)) -> id
+ | CRef (Ident (loc,id)) -> (loc,id)
| a -> user_err_loc
(constr_loc a,"Ast.coerce_to_id",
str"This expression should be a simple identifier")
diff --git a/parsing/ast.mli b/parsing/ast.mli
index 1faaf78a7..265674a6c 100755
--- a/parsing/ast.mli
+++ b/parsing/ast.mli
@@ -86,7 +86,7 @@ type grammar_action =
type env = (string * typed_ast) list
-val coerce_to_id : constr_expr -> identifier
+val coerce_to_id : constr_expr -> identifier located
val coerce_global_to_id : reference -> identifier
val coerce_reference_to_id : reference -> identifier
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index da16be9b5..bd505088c 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -28,6 +28,8 @@ let _ =
List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw
let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr"
+let lstring = Gram.Entry.create "lstring"
+
if !Options.v7 then
GEXTEND Gram
@@ -42,8 +44,11 @@ END;
if !Options.v7 then
GEXTEND Gram
- GLOBAL: command;
+ GLOBAL: command lstring;
+ lstring:
+ [ [ s = STRING -> s ] ]
+ ;
comment:
[ [ c = constr -> CommentConstr c
| s = STRING -> CommentString s
@@ -55,7 +60,7 @@ GEXTEND Gram
(* System directory *)
| IDENT "Pwd" -> VernacChdir None
| IDENT "Cd" -> VernacChdir None
- | IDENT "Cd"; dir = STRING -> VernacChdir (Some dir)
+ | IDENT "Cd"; dir = lstring -> VernacChdir (Some dir)
(* Toplevel control *)
| IDENT "Drop" -> VernacToplevelControl Drop
@@ -63,25 +68,25 @@ GEXTEND Gram
| "Quit" -> VernacToplevelControl Quit
(* Dump of the universe graph - to file or to stdout *)
- | IDENT "Dump"; IDENT "Universes"; fopt = OPT STRING ->
+ | IDENT "Dump"; IDENT "Universes"; fopt = OPT lstring ->
VernacPrint (PrintUniverses fopt)
| IDENT "Locate"; l = locatable -> VernacLocate l
(* Managing load paths *)
- | IDENT "Add"; IDENT "LoadPath"; dir = STRING; alias = as_dirpath ->
+ | IDENT "Add"; IDENT "LoadPath"; dir = lstring; alias = as_dirpath ->
VernacAddLoadPath (false, dir, alias)
- | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = STRING;
+ | IDENT "Add"; IDENT "Rec"; IDENT "LoadPath"; dir = lstring;
alias = as_dirpath -> VernacAddLoadPath (true, dir, alias)
- | IDENT "Remove"; IDENT "LoadPath"; dir = STRING ->
+ | IDENT "Remove"; IDENT "LoadPath"; dir = lstring ->
VernacRemoveLoadPath dir
(* For compatibility *)
- | IDENT "AddPath"; dir = STRING; "as"; alias = as_dirpath ->
+ | IDENT "AddPath"; dir = lstring; "as"; alias = as_dirpath ->
VernacAddLoadPath (false, dir, alias)
- | IDENT "AddRecPath"; dir = STRING; "as"; alias = as_dirpath ->
+ | IDENT "AddRecPath"; dir = lstring; "as"; alias = as_dirpath ->
VernacAddLoadPath (true, dir, alias)
- | IDENT "DelPath"; dir = STRING ->
+ | IDENT "DelPath"; dir = lstring ->
VernacRemoveLoadPath dir
(* Printing (careful factorization of entries) *)
@@ -104,7 +109,7 @@ GEXTEND Gram
VernacSearch (SearchRewrite c, l)
| IDENT "SearchAbout";
sl = [ "["; l = LIST1 [ r = global -> SearchRef r
- | s = STRING -> SearchString s ]; "]" -> l
+ | s = lstring -> SearchString s ]; "]" -> l
| qid = global -> [SearchRef qid] ];
l = in_or_out_modules ->
VernacSearch (SearchAbout sl, l)
@@ -116,9 +121,9 @@ GEXTEND Gram
VernacCheckMayEval (None, None, c)
| "Type"; c = constr -> VernacGlobalCheck c (* pas dans le RefMan *)
- | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = STRING ->
+ | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = lstring ->
VernacAddMLPath (false, dir)
- | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = STRING ->
+ | IDENT "Add"; IDENT "Rec"; IDENT "ML"; IDENT "Path"; dir = lstring ->
VernacAddMLPath (true, dir)
(*
| IDENT "SearchIsos"; c = constr -> VernacSearch (SearchIsos c)
@@ -199,17 +204,17 @@ GEXTEND Gram
;
locatable:
[ [ qid = global -> LocateTerm qid
- | IDENT "File"; f = STRING -> LocateFile f
+ | IDENT "File"; f = lstring -> LocateFile f
| IDENT "Library"; qid = global -> LocateLibrary qid
- | s = STRING -> LocateNotation s ] ]
+ | s = lstring -> LocateNotation s ] ]
;
option_value:
[ [ n = integer -> IntValue n
- | s = STRING -> StringValue s ] ]
+ | s = lstring -> StringValue s ] ]
;
option_ref_value:
[ [ id = global -> QualidRefValue id
- | s = STRING -> StringRefValue s ] ]
+ | s = lstring -> StringRefValue s ] ]
;
as_dirpath:
[ [ d = OPT [ "as"; d = dirpath -> d ] -> d ] ]
@@ -242,7 +247,7 @@ GEXTEND Gram
set_default_action_parser (parser_type_from_name univ); univ ] ]
;
syntax:
- [ [ IDENT "Token"; s = STRING ->
+ [ [ IDENT "Token"; s = lstring ->
Pp.warning "Token declarations are now useless"; VernacNop
| IDENT "Grammar"; IDENT "tactic"; IDENT "simple_tactic";
@@ -257,11 +262,11 @@ GEXTEND Gram
| IDENT "Syntax"; u = univ; el = LIST1 syntax_entry SEP ";" ->
VernacSyntax (u,el)
- | IDENT "Uninterpreted"; IDENT "Notation"; local = locality; s = STRING;
+ | IDENT "Uninterpreted"; IDENT "Notation"; local = locality; s = lstring;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
(s8,mv8) =
[IDENT "V8only";
- s8=OPT STRING;
+ s8=OPT lstring;
mv8=OPT["(";mv8=LIST1 syntax_modifier SEP ","; ")" -> mv8] ->
(s8,mv8)
| -> (None,None)] ->
@@ -271,7 +276,7 @@ GEXTEND Gram
| _ -> List.map map_modl modl in
VernacSyntaxExtension (local,Some (s,modl),Some(s8,mv8))
- | IDENT "Uninterpreted"; IDENT "V8Notation"; local = locality; s = STRING;
+ | IDENT "Uninterpreted"; IDENT "V8Notation"; local = locality; s = lstring;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] ->
VernacSyntaxExtension (local,None,Some(s,modl))
@@ -291,7 +296,7 @@ GEXTEND Gram
"["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl)
| IDENT "Infix"; local = locality; a = entry_prec; n = OPT natural;
- op = STRING;
+ op = lstring;
p = global;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
sc = OPT [ ":"; sc = IDENT -> sc];
@@ -299,7 +304,7 @@ GEXTEND Gram
[IDENT "V8only";
a8=entry_prec;
n8=OPT natural;
- op8=OPT STRING;
+ op8=OPT lstring;
mv8=["("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> []]
->
(match (a8,n8,mv8,op8) with
@@ -325,7 +330,7 @@ GEXTEND Gram
(op8,mv8)) mv8 in
VernacInfix (local,(op,mv),p,v8,sc)
| IDENT "Distfix"; local = locality; a = entry_prec; n = natural;
- s = STRING; p = global; sc = OPT [ ":"; sc = IDENT -> sc ] ->
+ s = lstring; p = global; sc = OPT [ ":"; sc = IDENT -> sc ] ->
let (a,s,c) = Metasyntax.translate_distfix a s p in
let mv = Some(s,[SetLevel n;SetAssoc a]) in
VernacNotation (local,c,mv,mv,sc)
@@ -336,12 +341,12 @@ GEXTEND Gram
l = [ "("; IDENT "only"; IDENT "parsing"; ")" -> [SetOnlyParsing]
| -> [] ] ->
VernacNotation (local,c,Some("'"^s^"'",l),None,None)
- | IDENT "Notation"; local = locality; s = STRING; ":="; c = constr;
+ | IDENT "Notation"; local = locality; s = lstring; ":="; c = constr;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
sc = OPT [ ":"; sc = IDENT -> sc ];
(s8,mv8) =
[IDENT "V8only";
- s8=OPT STRING;
+ s8=OPT lstring;
mv8=OPT["(";mv8=LIST1 syntax_modifier SEP ","; ")" -> mv8] ->
(s8,mv8)
| -> (* Means: rules are based on V7 rules *)
@@ -353,12 +358,12 @@ GEXTEND Gram
| None, Some mv8 -> Some (s,mv8) (* s like v7 *)
| Some s8, Some mv8 -> Some (s8,mv8) in
VernacNotation (local,c,Some(s,modl),smv8,sc)
- | IDENT "V8Notation"; local = locality; s = STRING; ":="; c = constr;
+ | IDENT "V8Notation"; local = locality; s = lstring; ":="; c = constr;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
sc = OPT [ ":"; sc = IDENT -> sc ] ->
VernacNotation (local,c,None,Some(s,modl),sc)
- | IDENT "V8Infix"; local = locality; op8 = STRING; p = global;
+ | IDENT "V8Infix"; local = locality; op8 = lstring; p = global;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
sc = OPT [ ":"; sc = IDENT -> sc] ->
let mv8 = Metasyntax.merge_modifiers None None modl in
@@ -385,7 +390,7 @@ GEXTEND Gram
| IDENT "no"; IDENT "associativity" -> SetAssoc Gramext.NonA
| x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ)
| IDENT "only"; IDENT "parsing" -> SetOnlyParsing
- | IDENT "format"; s = [s = STRING -> (loc,s)] -> SetFormat s ] ]
+ | IDENT "format"; s = [s = lstring -> (loc,s)] -> SetFormat s ] ]
;
syntax_extension_type:
[ [ IDENT "ident" -> ETIdent | IDENT "global" -> ETReference
@@ -409,7 +414,7 @@ GEXTEND Gram
| -> None ]]
;
grammar_tactic_rule:
- [[ name = rule_name; "["; s = STRING; pil = LIST0 production_item; "]";
+ [[ name = rule_name; "["; s = lstring; pil = LIST0 production_item; "]";
"->"; "["; t = Tactic.tactic; "]" -> (name, (s,pil), t) ]]
;
grammar_rule:
@@ -420,7 +425,7 @@ GEXTEND Gram
[[ name = IDENT -> name ]]
;
production_item:
- [[ s = STRING -> VTerm s
+ [[ s = lstring -> VTerm s
| nt = non_terminal; po = OPT [ "("; p = METAIDENT; ")" -> p ] ->
match po with
| Some p -> VNonTerm (loc,nt,Some (Names.id_of_string p))
@@ -452,7 +457,7 @@ GEXTEND Gram
next_hunks:
[ [ IDENT "FNL" -> UNP_FNL
| IDENT "TAB" -> UNP_TAB
- | c = STRING -> RO c
+ | c = lstring -> RO c
| "[";
x =
[ b = box; ll = LIST0 next_hunks -> UNP_BOX (b,ll)
@@ -478,7 +483,7 @@ GEXTEND Gram
paren_reln_or_extern:
[ [ IDENT "L" -> None, L
| IDENT "E" -> None, E
- | pprim = STRING; precrec = OPT [ ":"; p = precedence -> p ] ->
+ | pprim = lstring; precrec = OPT [ ":"; p = precedence -> p ] ->
match precrec with
| Some p -> Some pprim, Prec p
| None -> Some pprim, Any ] ]
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 51480a956..1e57506df 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -92,7 +92,7 @@ GEXTEND Gram
;
match_pattern:
[ [ id = Constr.constr_pattern; "["; pc = Constr.constr_pattern; "]" ->
- let s = coerce_to_id id in Subterm (Some s, pc)
+ let (_,s) = coerce_to_id id in Subterm (Some s, pc)
| "["; pc = Constr.constr_pattern; "]" -> Subterm (None,pc)
| pc = Constr.constr_pattern -> Term pc ] ]
;
diff --git a/parsing/g_module.ml4 b/parsing/g_module.ml4
index 7e2532c20..b3a281b64 100644
--- a/parsing/g_module.ml4
+++ b/parsing/g_module.ml4
@@ -31,9 +31,9 @@ GEXTEND Gram
;
with_declaration:
- [ [ "Definition"; id = base_ident; ":="; c = Constr.constr ->
+ [ [ "Definition"; id = identref; ":="; c = Constr.constr ->
CWith_Definition (id,c)
- | IDENT "Module"; id = base_ident; ":="; qid = qualid ->
+ | IDENT "Module"; id = identref; ":="; qid = qualid ->
CWith_Module (id,qid)
] ]
;
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 638591460..b011c8f33 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -45,11 +45,11 @@ GEXTEND Gram
| "Qed" -> VernacEndProof (Proved (true,None))
| IDENT "Save" -> VernacEndProof (Proved (true,None))
| IDENT "Defined" -> VernacEndProof (Proved (false,None))
- | IDENT "Defined"; id=base_ident ->
+ | IDENT "Defined"; id=identref ->
VernacEndProof (Proved (false,Some (id,None)))
- | IDENT "Save"; tok = thm_token; id = base_ident ->
+ | IDENT "Save"; tok = thm_token; id = identref ->
VernacEndProof (Proved (true,Some (id,Some tok)))
- | IDENT "Save"; id = base_ident ->
+ | IDENT "Save"; id = identref ->
VernacEndProof (Proved (true,Some (id,None)))
| IDENT "Suspend" -> VernacSuspend
| IDENT "Resume" -> VernacResume None
diff --git a/parsing/g_proofsnew.ml4 b/parsing/g_proofsnew.ml4
index 7d75cf4cb..28bf29b0e 100644
--- a/parsing/g_proofsnew.ml4
+++ b/parsing/g_proofsnew.ml4
@@ -46,12 +46,12 @@ GEXTEND Gram
| IDENT "Admitted" -> VernacEndProof Admitted
| IDENT "Qed" -> VernacEndProof (Proved (true,None))
| IDENT "Save" -> VernacEndProof (Proved (true,None))
- | IDENT "Save"; tok = thm_token; id = base_ident ->
+ | IDENT "Save"; tok = thm_token; id = identref ->
VernacEndProof (Proved (true,Some (id,Some tok)))
- | IDENT "Save"; id = base_ident ->
+ | IDENT "Save"; id = identref ->
VernacEndProof (Proved (true,Some (id,None)))
| IDENT "Defined" -> VernacEndProof (Proved (false,None))
- | IDENT "Defined"; id=base_ident ->
+ | IDENT "Defined"; id=identref ->
VernacEndProof (Proved (false,Some (id,None)))
| IDENT "Suspend" -> VernacSuspend
| IDENT "Resume" -> VernacResume None
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index cf10f0c45..e05ed48c5 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -32,7 +32,8 @@ let _ =
(* Functions overloaded by quotifier *)
let induction_arg_of_constr c =
- try ElimOnIdent (Topconstr.constr_loc c,coerce_to_id c) with _ -> ElimOnConstr c
+ try ElimOnIdent (Topconstr.constr_loc c,snd (coerce_to_id c))
+ with _ -> ElimOnConstr c
let local_compute = [FBeta;FIota;FDeltaBut [];FZeta]
@@ -154,7 +155,7 @@ GEXTEND Gram
bindings:
[ [ c1 = constr; ":="; c2 = constr; bl = LIST0 simple_binding ->
ExplicitBindings
- ((join_to_constr loc c2,NamedHyp (coerce_to_id c1), c2) :: bl)
+ ((join_to_constr loc c2,NamedHyp (snd(coerce_to_id c1)), c2) :: bl)
| n = natural; ":="; c = constr; bl = LIST0 simple_binding ->
ExplicitBindings ((join_to_constr loc c,AnonHyp n, c) :: bl)
| c1 = constr; bl = LIST0 constr ->
@@ -292,11 +293,11 @@ GEXTEND Gram
| IDENT "Cut"; c = constr -> TacCut c
| IDENT "Assert"; c = constr -> TacTrueCut (None,c)
| IDENT "Assert"; c = constr; ":"; t = constr ->
- TacTrueCut (Some (coerce_to_id c),t)
+ TacTrueCut (Some (snd(coerce_to_id c)),t)
| IDENT "Assert"; c = constr; ":="; b = constr ->
- TacForward (false,Names.Name (coerce_to_id c),b)
+ TacForward (false,Names.Name (snd (coerce_to_id c)),b)
| IDENT "Pose"; c = constr; ":="; b = constr ->
- TacForward (true,Names.Name (coerce_to_id c),b)
+ TacForward (true,Names.Name (snd(coerce_to_id c)),b)
| IDENT "Pose"; b = constr -> TacForward (true,Names.Anonymous,b)
| IDENT "Generalize"; lc = LIST1 constr -> TacGeneralize lc
| IDENT "Generalize"; IDENT "Dependent"; c = constr -> TacGeneralizeDep c
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 24f2be581..ccac2ae73 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -96,7 +96,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) =
(* Functions overloaded by quotifier *)
let induction_arg_of_constr c =
- try ElimOnIdent (Topconstr.constr_loc c,coerce_to_id c)
+ try ElimOnIdent (Topconstr.constr_loc c,snd(coerce_to_id c))
with _ -> ElimOnConstr c
let local_compute = [FBeta;FIota;FDeltaBut [];FZeta]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index a6d9c2420..fe8b462d8 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -135,7 +135,7 @@ GEXTEND Gram
| ":" -> false ] ]
;
params:
- [ [ idl = LIST1 base_ident SEP ","; coe = of_type_with_opt_coercion; c = constr
+ [ [ idl = LIST1 identref SEP ","; coe = of_type_with_opt_coercion; c = constr
-> List.map (fun c -> (coe,c)) (join_binders (idl,c))
] ]
;
@@ -146,7 +146,7 @@ GEXTEND Gram
[ [ ","; nal = LIST1 name SEP "," -> nal | -> [] ] ]
;
ident_comma_list_tail:
- [ [ ","; nal = LIST1 base_ident SEP "," -> nal | -> [] ] ]
+ [ [ ","; nal = LIST1 identref SEP "," -> nal | -> [] ] ]
;
decl_notation:
[ [ "where"; ntn = STRING; ":="; c = constr;
@@ -191,9 +191,9 @@ GEXTEND Gram
;
gallina:
(* Definition, Theorem, Variable, Axiom, ... *)
- [ [ thm = thm_token; id = base_ident; ":"; c = constr ->
+ [ [ thm = thm_token; id = identref; ":"; c = constr ->
VernacStartTheoremProof (thm, id, ([], c), false, (fun _ _ -> ()))
- | (f,d) = def_token; id = base_ident; b = def_body ->
+ | (f,d) = def_token; id = identref; b = def_body ->
VernacDefinition (d, id, b, f)
| stre = assumption_token; bl = ne_params_list ->
VernacAssumption (stre, bl)
@@ -211,7 +211,7 @@ GEXTEND Gram
[ [ IDENT "Record" -> true | IDENT "Structure" -> false ] ]
;
constructor:
- [ [ idl = LIST1 base_ident SEP ","; coe = of_type_with_opt_coercion;
+ [ [ idl = LIST1 identref SEP ","; coe = of_type_with_opt_coercion;
c = constr -> List.map (fun id -> (coe,(id,c))) idl ] ]
;
constructor_list:
@@ -224,11 +224,11 @@ GEXTEND Gram
| ind = oneind_old_style -> [ind] ] ]
;
oneind_old_style:
- [ [ id = base_ident; ":"; c = constr; ":="; lc = constructor_list ->
+ [ [ id = identref; ":"; c = constr; ":="; lc = constructor_list ->
(id,c,lc) ] ]
;
oneind:
- [ [ id = base_ident; indpar = simple_binders_list; ":"; c = constr;
+ [ [ id = identref; indpar = simple_binders_list; ":"; c = constr;
":="; lc = constructor_list; ntn = OPT decl_notation ->
(id,ntn,indpar,c,lc) ] ]
;
@@ -241,7 +241,7 @@ GEXTEND Gram
| -> false ] ]
;
onescheme:
- [ [ id = base_ident; ":="; dep = dep; ind = global; IDENT "Sort";
+ [ [ id = identref; ":="; dep = dep; ind = global; IDENT "Sort";
s = sort -> (id,dep,ind,s) ] ]
;
schemes:
@@ -271,12 +271,12 @@ GEXTEND Gram
[ [ l = LIST1 onecorec SEP "with" -> l ] ]
;
record_field:
- [ [ id = base_ident; oc = of_type_with_opt_coercion; t = constr ->
+ [ [ id = identref; oc = of_type_with_opt_coercion; t = constr ->
(oc,AssumExpr (id,t))
- | id = base_ident; oc = of_type_with_opt_coercion; t = constr;
+ | id = identref; oc = of_type_with_opt_coercion; t = constr;
":="; b = constr ->
(oc,DefExpr (id,b,Some t))
- | id = base_ident; ":="; b = constr ->
+ | id = identref; ":="; b = constr ->
(false,DefExpr (id,b,None)) ] ]
;
fields:
@@ -300,7 +300,7 @@ GEXTEND Gram
[ [ bll = LIST1 fix_binders -> List.flatten bll ] ]
;
rec_constructor:
- [ [ c = base_ident -> Some c
+ [ [ c = identref -> Some c
| -> None ] ]
;
gallina_ext:
@@ -308,7 +308,7 @@ GEXTEND Gram
indl = block_old_style ->
let indl' = List.map (fun (id,ar,c) -> (id,None,bl,ar,c)) indl in
VernacInductive (f,indl')
- | b = record_token; oc = opt_coercion; name = base_ident;
+ | b = record_token; oc = opt_coercion; name = identref;
ps = simple_binders_list; ":";
s = constr; ":="; c = rec_constructor; "{"; fs = fields; "}" ->
VernacRecord (b,(oc,name),ps,s,c,fs)
@@ -322,7 +322,7 @@ GEXTEND Gram
| "Fixpoint"; recs = specifrec -> VernacFixpoint recs
| "CoFixpoint"; corecs = specifcorec -> VernacCoFixpoint corecs
| IDENT "Scheme"; l = schemes -> VernacScheme l
- | f = finite_token; s = csort; id = base_ident;
+ | f = finite_token; s = csort; id = identref;
indpar = simple_binders_list; ":="; lc = constructor_list ->
VernacInductive (f,[id,None,indpar,s,lc]) ] ]
;
@@ -332,11 +332,11 @@ GEXTEND Gram
gallina_ext:
[ [
(* Sections *)
- IDENT "Section"; id = base_ident -> VernacBeginSection id
- | IDENT "Chapter"; id = base_ident -> VernacBeginSection id ] ]
+ IDENT "Section"; id = identref -> VernacBeginSection id
+ | IDENT "Chapter"; id = identref -> VernacBeginSection id ] ]
;
module_vardecls:
- [ [ id = base_ident; idl = ident_comma_list_tail; ":";
+ [ [ id = identref; idl = ident_comma_list_tail; ":";
mty = Module.module_type -> (id::idl,mty) ] ]
;
module_binders:
@@ -358,23 +358,23 @@ GEXTEND Gram
gallina_ext:
[ [
(* Interactive module declaration *)
- IDENT "Module"; id = base_ident;
+ IDENT "Module"; id = identref;
bl = module_binders_list; mty_o = OPT of_module_type;
mexpr_o = OPT is_module_expr ->
VernacDefineModule (id, bl, mty_o, mexpr_o)
- | IDENT "Module"; "Type"; id = base_ident;
+ | IDENT "Module"; "Type"; id = identref;
bl = module_binders_list; mty_o = OPT is_module_type ->
VernacDeclareModuleType (id, bl, mty_o)
- | IDENT "Declare"; IDENT "Module"; id = base_ident;
+ | IDENT "Declare"; IDENT "Module"; id = identref;
bl = module_binders_list; mty_o = OPT of_module_type;
mexpr_o = OPT is_module_expr ->
VernacDeclareModule (id, bl, mty_o, mexpr_o)
(* This end a Section a Module or a Module Type *)
- | IDENT "End"; id = base_ident -> VernacEndSegment id
+ | IDENT "End"; id = identref -> VernacEndSegment id
(* Transparent and Opaque *)
@@ -387,21 +387,21 @@ GEXTEND Gram
| IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body ->
let s = Ast.coerce_global_to_id qid in
VernacDefinition
- ((Global,CanonicalStructure),s,d,Recordobj.add_object_hook)
+ ((Global,CanonicalStructure),(dummy_loc,s),d,Recordobj.add_object_hook)
(* Rem: LOBJECT, OBJCOERCION, LOBJCOERCION have been removed
(they were unused and undocumented) *)
(* Coercions *)
| IDENT "Coercion"; qid = global; d = def_body ->
let s = Ast.coerce_global_to_id qid in
- VernacDefinition ((Global,Coercion),s,d,Class.add_coercion_hook)
+ VernacDefinition ((Global,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
| IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
let s = Ast.coerce_global_to_id qid in
- VernacDefinition ((Local,Coercion),s,d,Class.add_coercion_hook)
- | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = base_ident;
+ VernacDefinition ((Local,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
+ | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
":"; s = class_rawexpr; ">->"; t = class_rawexpr ->
VernacIdentityCoercion (Local, f, s, t)
- | IDENT "Identity"; IDENT "Coercion"; f = base_ident; ":";
+ | IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
s = class_rawexpr; ">->"; t = class_rawexpr ->
VernacIdentityCoercion (Global, f, s, t)
| IDENT "Coercion"; IDENT "Local"; qid = global; ":";
@@ -417,7 +417,7 @@ GEXTEND Gram
(* Implicit *)
(*
- | IDENT "Syntactic"; "Definition"; id = base_ident; ":="; c = constr;
+ | IDENT "Syntactic"; "Definition"; id = identref; ":="; c = constr;
n = OPT [ "|"; n = natural -> n ] ->
VernacSyntacticDefinition (id,c,n)
*)
@@ -435,7 +435,7 @@ GEXTEND Gram
| IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None)
| IDENT "Implicit"; ["Variable"; "Type" | IDENT "Variables"; "Type"];
- idl = LIST1 ident SEP ","; ":"; c = constr -> VernacReserve (idl,c)
+ idl = LIST1 identref SEP ","; ":"; c = constr -> VernacReserve (idl,c)
(* For compatibility *)
| IDENT "Implicit"; IDENT "Arguments"; IDENT "On" ->
@@ -486,7 +486,7 @@ GEXTEND Gram
| IDENT "Require"; export = export_token; specif = specif_token;
qidl = LIST1 global -> VernacRequire (Some export, specif, qidl)
(* | IDENT "Require"; export = export_token; specif = specif_token;
- id = base_ident; filename = STRING ->
+ id = identref; filename = STRING ->
VernacRequireFrom (export, specif, id, filename) *)
| IDENT "Require"; export = export_token; specif = specif_token;
filename = STRING ->
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 8c0b6ef73..5599f5880 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -97,11 +97,11 @@ GEXTEND Gram
gallina:
(* Definition, Theorem, Variable, Axiom, ... *)
- [ [ thm = thm_token; id = base_ident; (* bl = LIST0 binder; *) ":";
+ [ [ thm = thm_token; id = identref; (* bl = LIST0 binder; *) ":";
c = lconstr ->
let bl = [] in
VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ()))
- | (f,d) = def_token; id = base_ident; b = def_body ->
+ | (f,d) = def_token; id = identref; b = def_body ->
VernacDefinition (d, id, b, f)
| stre = assumption_token; bl = assum_list ->
VernacAssumption (stre, flatten_assum bl)
@@ -120,13 +120,13 @@ GEXTEND Gram
| IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l ] ]
;
gallina_ext:
- [ [ b = record_token; oc = opt_coercion; name = base_ident;
+ [ [ b = record_token; oc = opt_coercion; name = identref;
ps = LIST0 binder_let; ":";
- s = lconstr; ":="; cstr = OPT base_ident; "{";
+ s = lconstr; ":="; cstr = OPT identref; "{";
fs = LIST0 record_field SEP ";"; "}" ->
VernacRecord (b,(oc,name),ps,s,cstr,fs)
(* Non porté ?
- | f = finite_token; s = csort; id = base_ident;
+ | f = finite_token; s = csort; id = identref;
indpar = LIST0 simple_binder; ":="; lc = constructor_list ->
VernacInductive (f,[id,None,indpar,s,lc])
*)
@@ -186,7 +186,7 @@ GEXTEND Gram
;
(* Inductives and records *)
inductive_definition:
- [ [ id = base_ident; indpar = LIST0 binder_let; ":"; c = lconstr;
+ [ [ id = identref; indpar = LIST0 binder_let; ":"; c = lconstr;
":="; lc = constructor_list; ntn = decl_notation ->
(id,ntn,indpar,c,lc) ] ]
;
@@ -244,7 +244,7 @@ GEXTEND Gram
;
(* Inductive schemes *)
scheme:
- [ [ id = base_ident; ":="; dep = dep_scheme; "for"; ind = global;
+ [ [ id = identref; ":="; dep = dep_scheme; "for"; ind = global;
IDENT "Sort"; s = sort ->
(id,dep,ind,s) ] ]
;
@@ -266,12 +266,12 @@ GEXTEND Gram
*)
(* ... with coercions *)
record_field:
- [ [ id = base_ident -> (false,AssumExpr(id,CHole loc))
- | id = base_ident; oc = of_type_with_opt_coercion; t = lconstr ->
+ [ [ id = identref -> (false,AssumExpr(id,CHole loc))
+ | id = identref; oc = of_type_with_opt_coercion; t = lconstr ->
(oc,AssumExpr (id,t))
- | id = base_ident; oc = of_type_with_opt_coercion;
+ | id = identref; oc = of_type_with_opt_coercion;
t = lconstr; ":="; b = lconstr -> (oc,DefExpr (id,b,Some t))
- | id = base_ident; ":="; b = lconstr ->
+ | id = identref; ":="; b = lconstr ->
match b with
CCast(_,b,t) -> (false,DefExpr(id,b,Some t))
| _ -> (false,DefExpr(id,b,None)) ] ]
@@ -283,14 +283,14 @@ GEXTEND Gram
[ [ "("; a = simple_assum_coe; ")" -> a ] ]
;
simple_assum_coe:
- [ [ idl = LIST1 base_ident; oc = of_type_with_opt_coercion; c = lconstr ->
+ [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr ->
(oc,(idl,c)) ] ]
;
constructor:
- [ [ id = base_ident; l = LIST0 binder_let;
+ [ [ id = identref; l = LIST0 binder_let;
coe = of_type_with_opt_coercion; c = lconstr ->
(coe,(id,G_constrnew.mkCProdN loc l c))
- | id = base_ident; l = LIST0 binder_let ->
+ | id = identref; l = LIST0 binder_let ->
(false,(id,G_constrnew.mkCProdN loc l (CHole loc))) ] ]
;
of_type_with_opt_coercion:
@@ -308,25 +308,25 @@ GEXTEND Gram
gallina_ext:
[ [ (* Interactive module declaration *)
- IDENT "Module"; id = base_ident;
+ IDENT "Module"; id = identref;
bl = LIST0 module_binder; mty_o = OPT of_module_type;
mexpr_o = OPT is_module_expr ->
VernacDefineModule (id, bl, mty_o, mexpr_o)
- | IDENT "Module"; "Type"; id = base_ident;
+ | IDENT "Module"; "Type"; id = identref;
bl = LIST0 module_binder; mty_o = OPT is_module_type ->
VernacDeclareModuleType (id, bl, mty_o)
- | IDENT "Declare"; IDENT "Module"; id = base_ident;
+ | IDENT "Declare"; IDENT "Module"; id = identref;
bl = LIST0 module_binder; mty_o = OPT of_module_type;
mexpr_o = OPT is_module_expr ->
VernacDeclareModule (id, bl, mty_o, mexpr_o)
(* Section beginning *)
- | IDENT "Section"; id = base_ident -> VernacBeginSection id
- | IDENT "Chapter"; id = base_ident -> VernacBeginSection id
+ | IDENT "Section"; id = identref -> VernacBeginSection id
+ | IDENT "Chapter"; id = identref -> VernacBeginSection id
(* This end a Section a Module or a Module Type *)
- | IDENT "End"; id = base_ident -> VernacEndSegment id
+ | IDENT "End"; id = identref -> VernacEndSegment id
(* Requiring an already compiled module *)
| IDENT "Require"; export = export_token; specif = specif_token;
@@ -361,7 +361,7 @@ GEXTEND Gram
(* Module binder *)
module_binder:
- [ [ "("; idl = LIST1 base_ident; ":"; mty = module_type; ")" ->
+ [ [ "("; idl = LIST1 identref; ":"; mty = module_type; ")" ->
(idl,mty) ] ]
;
@@ -374,9 +374,9 @@ GEXTEND Gram
] ]
;
with_declaration:
- [ [ "Definition"; id = base_ident; ":="; c = Constr.lconstr ->
+ [ [ "Definition"; id = identref; ":="; c = Constr.lconstr ->
CWith_Definition (id,c)
- | IDENT "Module"; id = base_ident; ":="; qid = qualid ->
+ | IDENT "Module"; id = identref; ":="; qid = qualid ->
CWith_Module (id,qid)
] ]
;
@@ -404,19 +404,19 @@ GEXTEND Gram
| IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body ->
let s = Ast.coerce_global_to_id qid in
VernacDefinition
- ((Global,CanonicalStructure),s,d,Recordobj.add_object_hook)
+ ((Global,CanonicalStructure),(dummy_loc,s),d,Recordobj.add_object_hook)
(* Coercions *)
| IDENT "Coercion"; qid = global; d = def_body ->
let s = Ast.coerce_global_to_id qid in
- VernacDefinition ((Global,Coercion),s,d,Class.add_coercion_hook)
+ VernacDefinition ((Global,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
| IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
let s = Ast.coerce_global_to_id qid in
- VernacDefinition ((Local,Coercion),s,d,Class.add_coercion_hook)
- | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = base_ident;
+ VernacDefinition ((Local,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
+ | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
":"; s = class_rawexpr; ">->"; t = class_rawexpr ->
VernacIdentityCoercion (Local, f, s, t)
- | IDENT "Identity"; IDENT "Coercion"; f = base_ident; ":";
+ | IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
s = class_rawexpr; ">->"; t = class_rawexpr ->
VernacIdentityCoercion (Global, f, s, t)
| IDENT "Coercion"; IDENT "Local"; qid = global; ":";
@@ -433,7 +433,7 @@ GEXTEND Gram
VernacDeclareImplicits (qid,pos)
| IDENT "Implicit"; ["Type" | IDENT "Types"];
- idl = LIST1 ident; ":"; c = lconstr -> VernacReserve (idl,c)
+ idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c)
(* For compatibility *)
| IDENT "Implicit"; IDENT "Arguments"; IDENT "On" ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 57a187f13..44d1bfa1e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -250,8 +250,8 @@ let corecursive_message v =
let interp_mutual lparams lnamearconstrs finite =
let allnames =
- List.fold_left
- (fun acc (id,_,_,l) -> id::(List.map fst l)@acc) [] lnamearconstrs in
+ List.fold_left (fun acc (id,_,_,l) -> id::(List.map fst l)@acc)
+ [] lnamearconstrs in
if not (list_distinct allnames) then
error "Two inductive objects have the same name";
let nparams = local_binders_length lparams
@@ -288,7 +288,8 @@ let interp_mutual lparams lnamearconstrs finite =
let paramassums =
List.fold_right (fun d l -> match d with
(id,LocalAssum _) -> id::l | (_,LocalDef _) -> l) params' [] in
- let indnames = List.map (fun (id,_,_,_)-> id) lnamearconstrs @ paramassums in
+ let indnames =
+ List.map (fun (id,_,_,_)-> id) lnamearconstrs @ paramassums in
let nparamassums = List.length paramassums in
let (ind_env,ind_impls,arityl) =
List.fold_left
@@ -327,7 +328,6 @@ let interp_mutual lparams lnamearconstrs finite =
List.map2
(fun ar (name,_,_,lname_constr) ->
let constrnames, bodies = List.split lname_constr in
-
(* Compute the conclusions of constructor types *)
(* for inductive given in ML syntax *)
let nar =
@@ -377,15 +377,15 @@ let eq_la d1 d2 = match d1,d2 with
let extract_coe lc =
List.fold_right
- (fun (addcoe,(id,t)) (l1,l2) ->
+ (fun (addcoe,((_,(id:identifier)),t)) (l1,l2) ->
((if addcoe then id::l1 else l1), (id,t)::l2)) lc ([],[])
let extract_coe_la_lc = function
| [] -> anomaly "Vernacentries: empty list of inductive types"
- | (id,ntn,la,ar,lc)::rest ->
+ | ((_,id),ntn,la,ar,lc)::rest ->
let rec check = function
| [] -> [],[]
- | (id,ntn,la',ar,lc)::rest ->
+ | ((_,id),ntn,la',ar,lc)::rest ->
if (List.length la = List.length la') &&
(List.for_all2 eq_la la la')
then
@@ -401,7 +401,7 @@ let extract_coe_la_lc = function
(coes,la,(id,ntn,ar,lc'):: mspec)
let build_mutual lind finite =
- let (coes,lparams,lnamearconstructs) = extract_coe_la_lc lind in
+ let ((coes:identifier list),lparams,lnamearconstructs) = extract_coe_la_lc lind in
let notations,mie = interp_mutual lparams lnamearconstructs finite in
let kn = declare_mutual_with_eliminations mie in
(* Declare the notations now bound to the inductive types *)
@@ -578,7 +578,7 @@ let build_corecursive lnameardef =
in ()
let build_scheme lnamedepindsort =
- let lrecnames = List.map (fun (f,_,_,_) -> f) lnamedepindsort
+ let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort
and sigma = Evd.empty
and env0 = Global.env() in
let lrecspec =
diff --git a/toplevel/command.mli b/toplevel/command.mli
index c12a49485..07faea0b0 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -47,7 +47,7 @@ val build_recursive : (fixpoint_expr * decl_notation) list -> unit
val build_corecursive : cofixpoint_expr list -> unit
-val build_scheme : (identifier * bool * reference * rawsort) list -> unit
+val build_scheme : (identifier located * bool * reference * rawsort) list -> unit
val generalize_rawconstr : constr_expr -> local_binder list -> constr_expr
diff --git a/toplevel/record.ml b/toplevel/record.ml
index aab5bc337..a2a679cb1 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -35,8 +35,8 @@ open Topconstr
let name_of id = if id = wildcard then Anonymous else Name id
let interp_decl sigma env = function
- | Vernacexpr.AssumExpr(id,t) -> (name_of id,None,interp_type Evd.empty env t)
- | Vernacexpr.DefExpr(id,c,t) ->
+ | Vernacexpr.AssumExpr((_,id),t) -> (name_of id,None,interp_type Evd.empty env t)
+ | Vernacexpr.DefExpr((_,id),c,t) ->
let c = match t with
| None -> c
| Some t -> mkCastC (c,t)
@@ -207,10 +207,12 @@ let declare_projections indsp coers fields =
(* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean
list telling if the corresponding fields must me declared as coercion *)
-let definition_structure ((is_coe,idstruc),ps,cfs,idbuild,s) =
+let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
let coers,fs = List.split cfs in
let nparams = local_binders_length ps in
- let extract_name = function Vernacexpr.AssumExpr(id,_) -> id | Vernacexpr.DefExpr (id,_,_) -> id in
+ let extract_name = function
+ Vernacexpr.AssumExpr((_,id),_) -> id
+ | Vernacexpr.DefExpr ((_,id),_,_) -> id in
let allnames = idstruc::(List.map extract_name fs) in
if not (list_distinct allnames) then error "Two objects have the same name";
(* Now, younger decl in params and fields is on top *)
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 45d6e69ba..5837b5a4c 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -24,5 +24,5 @@ val declare_projections :
inductive -> bool list -> rel_context -> constant option list
val definition_structure :
- identifier with_coercion * local_binder list *
+ lident with_coercion * local_binder list *
(local_decl_expr with_coercion) list * identifier * sorts -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f0efb9db8..58eb42b6d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -286,8 +286,8 @@ let vernac_end_proof = function
if_verbose show_script ();
match idopt with
| None -> save_named is_opaque
- | Some (id,None) -> save_anonymous is_opaque id
- | Some (id,Some kind) -> save_anonymous_with_strength kind is_opaque id
+ | Some ((_,id),None) -> save_anonymous is_opaque id
+ | Some ((_,id),Some kind) -> save_anonymous_with_strength kind is_opaque id
(* A stupid macro that should be replaced by ``Exact c. Save.'' all along
the theories [??] *)
@@ -297,7 +297,8 @@ let vernac_exact_proof c =
save_named true
let vernac_assumption kind l =
- List.iter (fun (is_coe,(id,c)) -> declare_assumption id is_coe kind [] c) l
+ List.iter (fun (is_coe,((_,id),c)) ->
+ declare_assumption id is_coe kind [] c) l
let vernac_inductive f indl = build_mutual indl f
@@ -441,8 +442,8 @@ let vernac_end_modtype id =
let vernac_record struc binders sort nameopt cfs =
let const = match nameopt with
- | None -> add_prefix "Build_" (snd struc)
- | Some id -> id in
+ | None -> add_prefix "Build_" (snd (snd struc))
+ | Some (_,id) -> id in
let sigma = Evd.empty in
let env = Global.env() in
let s = interp_constr sigma env sort in
@@ -1142,8 +1143,8 @@ let interp c = match c with
vernac_notation local c infpl mv8 sc
(* Gallina *)
- | VernacDefinition (k,id,d,f) -> vernac_definition k id d f
- | VernacStartTheoremProof (k,id,t,top,f) ->
+ | VernacDefinition (k,(_,id),d,f) -> vernac_definition k id d f
+ | VernacStartTheoremProof (k,(_,id),t,top,f) ->
vernac_start_proof k (Some id) t top f
| VernacEndProof e -> vernac_end_proof e
| VernacExactProof c -> vernac_exact_proof c
@@ -1154,24 +1155,24 @@ let interp c = match c with
| VernacScheme l -> vernac_scheme l
(* Modules *)
- | VernacDeclareModule (id,bl,mtyo,mexpro) ->
+ | VernacDeclareModule ((_,id),bl,mtyo,mexpro) ->
vernac_declare_module id bl mtyo mexpro
- | VernacDefineModule (id,bl,mtyo,mexpro) ->
+ | VernacDefineModule ((_,id),bl,mtyo,mexpro) ->
vernac_define_module id bl mtyo mexpro
- | VernacDeclareModuleType (id,bl,mtyo) ->
+ | VernacDeclareModuleType ((_,id),bl,mtyo) ->
vernac_declare_module_type id bl mtyo
(* Gallina extensions *)
- | VernacBeginSection id -> vernac_begin_section id
+ | VernacBeginSection (_,id) -> vernac_begin_section id
- | VernacEndSegment id -> vernac_end_segment id
+ | VernacEndSegment (_,id) -> vernac_end_segment id
| VernacRecord (_,id,bl,s,idopt,fs) -> vernac_record id bl s idopt fs
| VernacRequire (export,spec,qidl) -> vernac_require export spec qidl
| VernacImport (export,qidl) -> vernac_import export qidl
| VernacCanonical qid -> vernac_canonical qid
| VernacCoercion (str,r,s,t) -> vernac_coercion str r s t
- | VernacIdentityCoercion (str,id,s,t) -> vernac_identity_coercion str id s t
+ | VernacIdentityCoercion (str,(_,id),s,t) -> vernac_identity_coercion str id s t
(* Solving *)
| VernacSolve (n,tac,b) -> vernac_solve n tac b
@@ -1197,7 +1198,7 @@ let interp c = match c with
(* Commands *)
| VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l
| VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints
- | VernacSyntacticDefinition (id,c,n) -> vernac_syntactic_definition id c n
+ | VernacSyntacticDefinition ((_,id),c,n) -> vernac_syntactic_definition id c n
| VernacDeclareImplicits (qid,l) -> vernac_declare_implicits qid l
| VernacReserve (idl,c) -> vernac_reserve idl c
| VernacSetOpacity (opaq, qidl) -> List.iter (vernac_set_opacity opaq) qidl
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 76d16862a..fe07a53d5 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -25,6 +25,10 @@ exception Quit
open Libnames
open Nametab
+type lident = identifier located
+type lstring = string
+type lreference = reference
+
type class_rawexpr = FunClass | SortClass | RefClass of reference
type printable =
@@ -131,11 +135,11 @@ type inductive_flag = bool (* true = Inductive; false = CoInductive *)
type sort_expr = Rawterm.rawsort
type decl_notation = (string * constr_expr * scope_name option) option
-type simple_binder = identifier * constr_expr
+type simple_binder = lident * constr_expr
type 'a with_coercion = coercion_flag * 'a
type constructor_expr = simple_binder with_coercion
type inductive_expr =
- identifier * decl_notation * local_binder list * constr_expr
+ lident * decl_notation * local_binder list * constr_expr
* constructor_expr list
type definition_expr =
| ProveBody of local_binder list * constr_expr
@@ -143,47 +147,47 @@ type definition_expr =
* constr_expr option
type local_decl_expr =
- | AssumExpr of identifier * constr_expr
- | DefExpr of identifier * constr_expr * constr_expr option
+ | AssumExpr of lident * constr_expr
+ | DefExpr of lident * constr_expr * constr_expr option
-type module_binder = identifier list * module_type_ast
+type module_binder = lident list * module_type_ast
type proof_end =
| Admitted
- | Proved of opacity_flag * (identifier * theorem_kind option) option
+ | Proved of opacity_flag * (lident * theorem_kind option) option
type vernac_expr =
(* Control *)
| VernacList of located_vernac_expr list
- | VernacLoad of verbose_flag * string
+ | VernacLoad of verbose_flag * lstring
| VernacTime of vernac_expr
- | VernacVar of identifier
+ | VernacVar of lident
(* Syntax *)
- | VernacGrammar of string * raw_grammar_entry list
+ | VernacGrammar of lstring * raw_grammar_entry list
| VernacTacticGrammar of
- (string * (string * grammar_production list) * raw_tactic_expr) list
- | VernacSyntax of string * raw_syntax_entry list
+ (lstring * (lstring * grammar_production list) * raw_tactic_expr) list
+ | VernacSyntax of lstring * raw_syntax_entry list
| VernacSyntaxExtension of locality_flag *
- (string * syntax_modifier list) option
- * (string * syntax_modifier list) option
+ (lstring * syntax_modifier list) option
+ * (lstring * syntax_modifier list) option
| VernacDistfix of locality_flag *
- grammar_associativity * precedence * string * reference *
+ grammar_associativity * precedence * lstring * lreference *
scope_name option
| VernacOpenCloseScope of (locality_flag * bool * scope_name)
- | VernacDelimiters of scope_name * string
+ | VernacDelimiters of scope_name * lstring
| VernacBindScope of scope_name * class_rawexpr list
- | VernacArgumentsScope of reference * scope_name option list
- | VernacInfix of locality_flag * (string * syntax_modifier list) *
- reference * (string * syntax_modifier list) option * scope_name option
+ | VernacArgumentsScope of lreference * scope_name option list
+ | VernacInfix of locality_flag * (lstring * syntax_modifier list) *
+ lreference * (lstring * syntax_modifier list) option * scope_name option
| VernacNotation of
- locality_flag * constr_expr * (string * syntax_modifier list) option *
- (string * syntax_modifier list) option * scope_name option
+ locality_flag * constr_expr * (lstring * syntax_modifier list) option *
+ (lstring * syntax_modifier list) option * scope_name option
(* Gallina *)
- | VernacDefinition of definition_kind * identifier * definition_expr *
+ | VernacDefinition of definition_kind * lident * definition_expr *
declaration_hook
- | VernacStartTheoremProof of theorem_kind * identifier *
+ | VernacStartTheoremProof of theorem_kind * lident *
(local_binder list * constr_expr) * bool * declaration_hook
| VernacEndProof of proof_end
| VernacExactProof of constr_expr
@@ -191,28 +195,28 @@ type vernac_expr =
| VernacInductive of inductive_flag * inductive_expr list
| VernacFixpoint of (fixpoint_expr * decl_notation) list
| VernacCoFixpoint of cofixpoint_expr list
- | VernacScheme of (identifier * bool * reference * sort_expr) list
+ | VernacScheme of (lident * bool * lreference * sort_expr) list
(* Gallina extensions *)
| VernacRecord of bool (* = Record or Structure *)
- * identifier with_coercion * local_binder list
- * constr_expr * identifier option * local_decl_expr with_coercion list
- | VernacBeginSection of identifier
- | VernacEndSegment of identifier
+ * lident with_coercion * local_binder list
+ * constr_expr * lident option * local_decl_expr with_coercion list
+ | VernacBeginSection of lident
+ | VernacEndSegment of lident
| VernacRequire of
- export_flag option * specif_flag option * reference list
- | VernacImport of export_flag * reference list
- | VernacCanonical of reference
- | VernacCoercion of strength * reference * class_rawexpr * class_rawexpr
- | VernacIdentityCoercion of strength * identifier *
+ export_flag option * specif_flag option * lreference list
+ | VernacImport of export_flag * lreference list
+ | VernacCanonical of lreference
+ | VernacCoercion of strength * lreference * class_rawexpr * class_rawexpr
+ | VernacIdentityCoercion of strength * lident *
class_rawexpr * class_rawexpr
(* Modules and Module Types *)
- | VernacDeclareModule of identifier *
+ | VernacDeclareModule of lident *
module_binder list * (module_type_ast * bool) option * module_ast option
- | VernacDefineModule of identifier *
+ | VernacDefineModule of lident *
module_binder list * (module_type_ast * bool) option * module_ast option
- | VernacDeclareModuleType of identifier *
+ | VernacDeclareModuleType of lident *
module_binder list * module_type_ast option
(* Solving *)
@@ -220,30 +224,30 @@ type vernac_expr =
| VernacSolveExistential of int * constr_expr
(* Auxiliary file and library management *)
- | VernacRequireFrom of export_flag option * specif_flag option * string
- | VernacAddLoadPath of rec_flag * string * dir_path option
- | VernacRemoveLoadPath of string
- | VernacAddMLPath of rec_flag * string
- | VernacDeclareMLModule of string list
- | VernacChdir of string option
+ | VernacRequireFrom of export_flag option * specif_flag option * lstring
+ | VernacAddLoadPath of rec_flag * lstring * dir_path option
+ | VernacRemoveLoadPath of lstring
+ | VernacAddMLPath of rec_flag * lstring
+ | VernacDeclareMLModule of lstring list
+ | VernacChdir of lstring option
(* State management *)
- | VernacWriteState of string
- | VernacRestoreState of string
+ | VernacWriteState of lstring
+ | VernacRestoreState of lstring
(* Resetting *)
- | VernacResetName of identifier located
+ | VernacResetName of lident
| VernacResetInitial
| VernacBack of int
(* Commands *)
| VernacDeclareTacticDefinition of
- rec_flag * (identifier located * raw_tactic_expr) list
- | VernacHints of locality_flag * string list * hints
- | VernacSyntacticDefinition of identifier * constr_expr * int option
- | VernacDeclareImplicits of reference * explicitation list option
- | VernacReserve of identifier list * constr_expr
- | VernacSetOpacity of opacity_flag * reference list
+ rec_flag * (lident * raw_tactic_expr) list
+ | VernacHints of locality_flag * lstring list * hints
+ | VernacSyntacticDefinition of lident * constr_expr * int option
+ | VernacDeclareImplicits of lreference * explicitation list option
+ | VernacReserve of lident list * constr_expr
+ | VernacSetOpacity of opacity_flag * lreference list
| VernacUnsetOption of Goptions.option_name
| VernacSetOption of Goptions.option_name * option_value
| VernacAddOption of Goptions.option_name * option_ref_value list
@@ -260,11 +264,11 @@ type vernac_expr =
(* Proof management *)
| VernacGoal of constr_expr
- | VernacAbort of identifier located option
+ | VernacAbort of lident option
| VernacAbortAll
| VernacRestart
| VernacSuspend
- | VernacResume of identifier located option
+ | VernacResume of lident option
| VernacUndo of int
| VernacFocus of int option
| VernacUnfocus
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 128cd148f..8e7128715 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -23,7 +23,6 @@ open Term
open Pattern
(*i*)
-let sep = fun _ -> brk(1,0)
let sep_p = fun _ -> str"."
let sep_v = fun _ -> str"," ++ spc()
let sep_pp = fun _ -> str":"
@@ -77,11 +76,28 @@ let pr_delimiters key strm =
let surround p = str"(" ++ p ++ str")"
+let pr_located pr ((b,e),x) =
+ if Options.do_translate() && (b,e)<>dummy_loc then
+ comment b ++ pr x ++ comment e
+ else pr x
+
+let pr_com_at n =
+ if Options.do_translate() && n <> 0 then comment n
+ else mt()
+
+let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
+
+let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
+
open Rawterm
let pr_opt pr = function
| None -> mt ()
- | Some x -> spc () ++ pr x
+ | Some x -> spc() ++ pr x
+
+let pr_optc pr = function
+ | None -> mt ()
+ | Some x -> pr_sep_com spc pr x
let pr_universe u = str "<univ>"
@@ -93,9 +109,10 @@ let pr_sort = function
let pr_expl_args pr (a,expl) =
match expl with
| None -> pr (lapp,L) a
- | Some (_,ExplByPos n) -> str "@" ++ int n ++ str ":=" ++ pr (lapp,L) a
+ | Some (_,ExplByPos n) ->
+ anomaly("Explicitation by position not implemented")
| Some (_,ExplByName id) ->
- str "(" ++ pr_id id ++ str ":=" ++ pr (lapp,L) a ++ str ")"
+ str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
let pr_opt_type pr = function
| CHole _ -> mt ()
@@ -103,55 +120,70 @@ let pr_opt_type pr = function
let pr_opt_type_spc pr = function
| CHole _ -> mt ()
- | t -> str " :" ++ brk(1,2) ++ pr ltop t
+ | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
let pr_name = function
| Anonymous -> str"_"
| Name id -> pr_id (Constrextern.v7_to_v8_id id)
-let pr_located pr ((b,e),x) =
- if Options.do_translate() then comment b ++ pr x ++ comment e
- else pr x
+let pr_lident (b,_ as loc,id) =
+ if loc <> dummy_loc then
+ pr_located pr_id ((b,b+String.length(string_of_id id)),id)
+ else pr_id id
-let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
+let pr_lname = function
+ (loc,Name id) -> pr_lident (loc,id)
+ | lna -> pr_located pr_name lna
let pr_or_var pr = function
| Genarg.ArgArg x -> pr x
- | Genarg.ArgVar (loc,s) -> pr_with_comments loc (pr_id s)
+ | Genarg.ArgVar (loc,s) -> pr_lident (loc,s)
let las = lapp
-let rec pr_patt inh p =
+let rec pr_patt sep inh p =
let (strm,prec) = match p with
| CPatAlias (_,p,id) ->
- pr_patt (las,E) p ++ str " as " ++ pr_id id, las
+ pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las
| CPatCstr (_,c,[]) -> pr_reference c, latom
| CPatCstr (_,c,args) ->
- pr_reference c ++ spc() ++
- prlist_with_sep sep (pr_patt (lapp,L)) args, lapp
+ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
| CPatAtom (_,None) -> str "_", latom
| CPatAtom (_,Some r) -> pr_reference r, latom
| CPatNotation (_,"( _ )",[p]) ->
- str"("++ pr_patt (max_int,E) p ++ str")", latom
- | CPatNotation (_,s,env) -> pr_notation pr_patt s env
+ pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
+ | CPatNotation (_,s,env) -> pr_notation (pr_patt mt) s env
| CPatNumeral (_,i) -> Bignat.pr_bigint i, latom
- | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt lsimple p), 1
+ | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1
in
let loc = cases_pattern_loc p in
- pr_with_comments loc (if prec_less prec inh then strm else surround strm)
+ pr_with_comments loc
+ (sep() ++ if prec_less prec inh then strm else surround strm)
+
+let pr_patt = pr_patt mt
+
let pr_eqn pr (loc,pl,rhs) =
spc() ++ hov 4
(pr_with_comments loc
(str "| " ++
hov 0 (prlist_with_sep sep_v (pr_patt ltop) pl ++ str " =>") ++
- spc() ++ pr ltop rhs))
+ pr_sep_com spc (pr ltop) rhs))
+
+let begin_of_binder = function
+ LocalRawDef(((b,_),_),_) -> b
+ | LocalRawAssum(((b,_),_)::_,_) -> b
+ | _ -> assert false
+
+let begin_of_binders = function
+ | b::_ -> begin_of_binder b
+ | _ -> 0
let pr_binder many pr (nal,t) =
match t with
- | CHole _ -> prlist_with_sep sep (pr_located pr_name) nal
+ | CHole _ -> prlist_with_sep spc pr_lname nal
| _ ->
- let s = prlist_with_sep sep (pr_located pr_name) nal ++ str" : " ++ pr t in
+ let s = prlist_with_sep spc pr_lname nal ++ str" : " ++ pr t in
hov 1 (if many then surround s else s)
let pr_binder_among_many pr_c = function
@@ -162,19 +194,24 @@ let pr_binder_among_many pr_c = function
| CCast(_,c,t) -> c, t
| _ -> c, CHole dummy_loc in
hov 1 (surround
- (pr_located pr_name na ++ pr_opt_type pr_c topt ++
+ (pr_lname na ++ pr_opt_type pr_c topt ++
str":=" ++ cut() ++ pr_c c))
let pr_undelimited_binders pr_c =
- prlist_with_sep sep (pr_binder_among_many pr_c)
+ prlist_with_sep spc (pr_binder_among_many pr_c)
-let pr_delimited_binders pr_c = function
- | [LocalRawAssum (nal,t)] -> pr_binder false pr_c (nal,t)
- | LocalRawAssum _ :: _ as bdl -> pr_undelimited_binders pr_c bdl
+let pr_delimited_binders kw pr_c bl =
+ let n = begin_of_binders bl in
+ match bl with
+ | [LocalRawAssum (nal,t)] ->
+ pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,t)
+ | LocalRawAssum _ :: _ as bdl ->
+ pr_com_at n ++ kw() ++ pr_undelimited_binders pr_c bdl
| _ -> assert false
let pr_let_binder pr x a =
- hov 0 (hov 0 (pr_name x ++ brk(0,1) ++ str ":=") ++ brk(0,1) ++ pr ltop a)
+ hov 0 (hov 0 (pr_name x ++ brk(0,1) ++ str ":=") ++
+ pr_sep_com (fun () -> brk(0,1)) (pr ltop) a)
let rec extract_prod_binders = function
| CLetIn (loc,na,b,c) as x ->
@@ -306,7 +343,7 @@ let pr_recursive_decl pr id bl annot t c =
pr_id id ++ str" " ++
hov 0 (pr_undelimited_binders (pr ltop) bl ++ annot) ++
pr_opt_type_spc pr t ++ str " :=" ++
- brk(1,2) ++ pr ltop c
+ pr_sep_com (fun () -> brk(1,2)) (pr ltop) c
let name_of_binder = function
| LocalRawAssum (nal,_) -> nal
@@ -377,7 +414,8 @@ let pr_case_item pr (tm,(na,indnalopt)) =
let pr_case_type pr po =
match po with
| None | Some (CHole _) -> mt()
- | Some p -> spc() ++ hov 2 (str "return" ++ spc () ++ pr (lcast,E) p)
+ | Some p ->
+ spc() ++ hov 2 (str "return" ++ pr_sep_com spc (pr lsimple) p)
let pr_return_type pr po = pr_case_type pr po
@@ -393,80 +431,85 @@ let pr_proj pr pr_app a f l =
let pr_appexpl pr f l =
hov 2 (
str "@" ++ pr_reference f ++
- prlist (fun a -> spc () ++ pr (lapp,L) a) l)
+ prlist (pr_sep_com spc (pr (lapp,L))) l)
let pr_app pr a l =
hov 2 (
pr (lapp,L) a ++
prlist (fun a -> spc () ++ pr_expl_args pr a) l)
-let rec pr inherited a =
+let rec pr sep inherited a =
let (strm,prec) = match a with
| CRef r -> pr_reference r, latom
| CFix (_,id,fix) ->
- let p = hov 0 (str"fix " ++ pr_recursive (pr_fixdecl pr) (snd id) fix) in
+ let p = hov 0 (str"fix " ++
+ pr_recursive (pr_fixdecl (pr mt)) (snd id) fix) in
if List.length fix = 1 & prec_less (fst inherited) ltop
then surround p, latom else p, lfix
| CCoFix (_,id,cofix) ->
let p =
hov 0 (str "cofix " ++
- pr_recursive (pr_cofixdecl pr) (snd id) cofix) in
+ pr_recursive (pr_cofixdecl (pr mt)) (snd id) cofix) in
if List.length cofix = 1 & prec_less (fst inherited) ltop
then surround p, latom else p, lfix
| CArrow (_,a,b) ->
- hov 0 (pr (larrow,L) a ++ str " ->" ++ brk(1,0) ++ pr (-larrow,E) b),
+ hov 0 (pr mt (larrow,L) a ++ str " ->" ++
+ pr (fun () ->brk(1,0)) (-larrow,E) b),
larrow
| CProdN _ ->
let (bl,a) = extract_prod_binders a in
- hov 2 (
- str"forall" ++ spc() ++ pr_delimited_binders (pr ltop) bl ++
- str "," ++ spc() ++ pr ltop a),
+ hov 0 (
+ hov 2 (pr_delimited_binders (fun () -> str"forall" ++ spc())
+ (pr mt ltop) bl) ++
+ str "," ++ pr spc ltop a),
lprod
| CLambdaN _ ->
let (bl,a) = extract_lam_binders a in
- hov 2 (
- str"fun" ++ spc() ++ pr_delimited_binders (pr ltop) bl ++
- str " =>" ++ spc() ++ pr ltop a),
+ hov 0 (
+ hov 2 (pr_delimited_binders (fun () -> str"fun" ++ spc())
+ (pr mt ltop) bl) ++
+
+ str " =>" ++ pr spc ltop a),
llambda
| CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b)
when x=x' ->
hv 0 (
- hov 2 (str "let " ++ pr ltop fx ++ str " in") ++
- spc () ++ pr ltop b),
+ hov 2 (str "let " ++ pr mt ltop fx ++ str " in") ++
+ pr spc ltop b),
lletin
| CLetIn (_,x,a,b) ->
hv 0 (
- hov 2 (str "let " ++ pr_located pr_name x ++ str " :=" ++ spc() ++
- pr ltop a ++ str " in") ++
- spc () ++ pr ltop b),
+ hov 2 (str "let " ++ pr_lname x ++ str " :=" ++
+ pr spc ltop a ++ str " in") ++
+ pr spc ltop b),
lletin
| CAppExpl (_,(Some i,f),l) ->
let l1,l2 = list_chop i l in
let c,l1 = list_sep_last l1 in
- let p = pr_proj pr pr_appexpl c f l1 in
+ let p = pr_proj (pr mt) pr_appexpl c f l1 in
if l2<>[] then
- p ++ prlist (fun a -> spc () ++ pr (lapp,L) a) l2, lapp
+ p ++ prlist (pr spc (lapp,L)) l2, lapp
else
p, lproj
- | CAppExpl (_,(None,f),l) -> pr_appexpl pr f l, lapp
+ | CAppExpl (_,(None,f),l) -> pr_appexpl (pr mt) f l, lapp
| CApp (_,(Some i,f),l) ->
let l1,l2 = list_chop i l in
let c,l1 = list_sep_last l1 in
assert (snd c = None);
- let p = pr_proj pr pr_app (fst c) f l1 in
+ let p = pr_proj (pr mt) pr_app (fst c) f l1 in
if l2<>[] then
- p ++ prlist (fun a -> spc () ++ pr_expl_args pr a) l2, lapp
+ p ++ prlist (fun a -> spc () ++ pr_expl_args (pr mt) a) l2, lapp
else
p, lproj
- | CApp (_,(None,a),l) -> pr_app pr a l, lapp
+ | CApp (_,(None,a),l) -> pr_app (pr mt) a l, lapp
| CCases (_,(po,rtntypopt),c,eqns) ->
v 0
(hv 0 (str "match" ++ brk (1,2) ++
hov 0 (
- prlist_with_sep sep_v (pr_case_item pr) c
- ++ pr_case_type pr rtntypopt) ++
+ prlist_with_sep sep_v (pr_case_item (pr mt)) c
+ ++ pr_case_type (pr mt) rtntypopt) ++
spc () ++ str "with") ++
- prlist (pr_eqn pr) eqns ++ spc() ++ str "end"),
+ prlist (pr_eqn (pr mt)) eqns ++ spc() ++ str "end"),
latom
| CLetTuple (_,nal,(na,po),c,b) ->
hv 0 (
@@ -474,27 +517,28 @@ let rec pr inherited a =
hov 0 (str "(" ++
prlist_with_sep sep_v pr_name nal ++
str ")" ++
- pr_simple_return_type pr na po ++ str " :=" ++
- spc() ++ pr ltop c ++ str " in") ++
- spc() ++ pr ltop b),
+ pr_simple_return_type (pr mt) na po ++ str " :=" ++
+ pr spc ltop c ++ str " in") ++
+ pr spc ltop b),
lletin
| CIf (_,c,(na,po),b1,b2) ->
(* On force les parenthèses autour d'un "if" sous-terme (même si le
parsing est lui plus tolérant) *)
hv 0 (
- hov 1 (str "if " ++ pr ltop c ++ pr_simple_return_type pr na po) ++
+ hov 1 (str "if " ++ pr mt ltop c ++ pr_simple_return_type (pr mt) na po) ++
spc () ++
- hov 0 (str "then" ++ brk (1,1) ++ pr ltop b1) ++ spc () ++
- hov 0 (str "else" ++ brk (1,1) ++ pr ltop b2)),
+ hov 0 (str "then" ++ pr (fun () -> brk (1,1)) ltop b1) ++ spc () ++
+ hov 0 (str "else" ++ pr (fun () -> brk (1,1)) ltop b2)),
lif
| COrderedCase (_,st,po,c,[b1;b2]) when st = IfStyle ->
(* On force les parenthèses autour d'un "if" sous-terme (même si le
parsing est lui plus tolérant) *)
hv 0 (
- hov 1 (str "if " ++ pr ltop c ++ pr_return_type pr po) ++ spc () ++
- hov 0 (str "then" ++ brk (1,1) ++ pr ltop b1) ++ spc () ++
- hov 0 (str "else" ++ brk (1,1) ++ pr ltop b2)),
+ hov 1 (str "if " ++ pr mt ltop c ++
+ pr_return_type (pr mt) po) ++ spc () ++
+ hov 0 (str "then" ++ pr (fun () -> brk (1,1)) ltop b1) ++ spc () ++
+ hov 0 (str "else" ++ pr (fun () -> brk (1,1)) ltop b2)),
lif
| COrderedCase (_,st,po,c,[CLambdaN(_,[nal,_],b)]) when st = LetStyle ->
hv 0 (
@@ -502,18 +546,18 @@ let rec pr inherited a =
hov 0 (str "(" ++
prlist_with_sep sep_v (fun (_,n) -> pr_name n) nal ++
str ")" ++
- pr_return_type pr po ++ str " :=" ++
- spc() ++ pr ltop c ++ str " in") ++
- spc() ++ pr ltop b),
+ pr_return_type (pr mt) po ++ str " :=" ++
+ pr spc ltop c ++ str " in") ++
+ pr spc ltop b),
lletin
| COrderedCase (_,style,po,c,bl) ->
hv 0 (
str (if style=MatchStyle then "old_match " else "match ") ++
- pr ltop c ++
- pr_return_type pr po ++
+ pr mt ltop c ++
+ pr_return_type (pr mt) po ++
str " with" ++ brk (1,0) ++
hov 0 (prlist
- (fun b -> str "| ??? =>" ++ spc() ++ pr ltop b ++ fnl ()) bl) ++
+ (fun b -> str "| ??? =>" ++ pr spc ltop b ++ fnl ()) bl) ++
str "end"),
latom
| CHole _ -> str "_", latom
@@ -521,18 +565,21 @@ let rec pr inherited a =
| CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
| CSort (_,s) -> pr_sort s, latom
| CCast (_,a,b) ->
- hv 0 (pr (lcast,L) a ++ cut () ++ str ":" ++ pr (-lcast,E) b), lcast
+ hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":" ++ pr mt (-lcast,E) b),
+ lcast
| CNotation (_,"( _ )",[t]) ->
- str"("++ pr (max_int,L) t ++ str")", latom
- | CNotation (_,s,env) -> pr_notation pr s env
+ pr (fun()->str"(") (max_int,L) t ++ str")", latom
+ | CNotation (_,s,env) -> pr_notation (pr mt) s env
| CNumeral (_,(Bignat.POS _ as p)) -> Bignat.pr_bigint p, lposint
| CNumeral (_,(Bignat.NEG _ as p)) -> Bignat.pr_bigint p, lnegint
- | CDelimiters (_,sc,a) -> pr_delimiters sc (pr lsimple a), 1
+ | CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt lsimple a), 1
| CDynamic _ -> str "<dynamic>", latom
in
let loc = constr_loc a in
pr_with_comments loc
- (if prec_less prec inherited then strm else surround strm)
+ (sep() ++ if prec_less prec inherited then strm else surround strm)
+
+let pr = pr mt
let rec strip_context n iscast t =
if n = 0 then
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli
index 968464f65..51c6f8b7f 100644
--- a/translate/ppconstrnew.mli
+++ b/translate/ppconstrnew.mli
@@ -40,7 +40,15 @@ 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_lident : identifier located -> std_ppcmds
+val pr_lname : name located -> std_ppcmds
+
val pr_with_comments : loc -> std_ppcmds -> std_ppcmds
+val pr_com_at : int -> std_ppcmds
+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_name : name -> std_ppcmds
val pr_qualid : qualid -> std_ppcmds
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 9ff326b52..2373f7371 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -40,10 +40,6 @@ let strip_prod_binders_expr n ty =
| _ -> error "Cannot translate fix tactic: not enough products" in
strip_ty [] n ty
-let is_ident_expr = function
- Topconstr.CRef(Ident _) -> true
- | _ -> false
-
(* In v8 syntax only double quote char is escaped by repeating it *)
let rec escape_string_v8 s =
@@ -290,7 +286,7 @@ let pr_match_pattern pr_pat = function
str "context " ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
let pr_match_hyps pr_pat = function
- | Hyp (nal,mp) -> pr_located pr_name nal ++ str ":" ++ pr_match_pattern pr_pat mp
+ | Hyp (nal,mp) -> pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp
let pr_match_rule m pr pr_pat = function
| Pat ([],mp,t) when m ->
@@ -308,10 +304,10 @@ let pr_funvar = function
let pr_let_clause k pr = function
| (id,None,t) ->
- hov 0 (str k ++ pr_located pr_id id ++ str " :=" ++ brk (1,1) ++
+ hov 0 (str k ++ pr_lident id ++ str " :=" ++ brk (1,1) ++
pr (TacArg t))
| (id,Some c,t) ->
- hv 0 (str k ++ pr_located pr_id id ++ str" :" ++ brk(1,2) ++
+ hv 0 (str k ++ pr_lident id ++ str" :" ++ brk(1,2) ++
pr c ++
str " :=" ++ brk (1,1) ++ pr (TacArg t))
@@ -324,7 +320,7 @@ let pr_let_clauses pr = function
let pr_rec_clause pr (id,(l,t)) =
hov 0
- (pr_located pr_id id ++ prlist pr_funvar l ++ str " :=") ++ spc () ++ pr t
+ (pr_lident id ++ prlist pr_funvar l ++ str " :=") ++ spc () ++ pr t
let pr_rec_clauses pr l =
prlist_with_sep (fun () -> fnl () ++ str "with ") (pr_rec_clause pr) l
@@ -374,7 +370,7 @@ let pr_then () = str ";"
open Closure
-let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_lconstr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend,strip_prod_binders,is_ident) =
+let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_lconstr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend,strip_prod_binders) =
let pr_bindings env = pr_bindings (pr_lconstr env) (pr_constr env) in
let pr_ex_bindings env = pr_bindings_gen true (pr_lconstr env) (pr_constr env) in
@@ -387,10 +383,10 @@ let pr_intarg n = spc () ++ int n in
let pr_binder_fix env (nal,t) =
(* match t with
- | CHole _ -> spc() ++ prlist_with_sep spc (pr_located pr_name) nal
+ | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
| _ ->*)
let s =
- prlist_with_sep spc (pr_located pr_name) nal ++ str ":" ++
+ prlist_with_sep spc (pr_lname) nal ++ str ":" ++
pr_lconstr env t in
spc() ++ hov 1 (str"(" ++ s ++ str")") in
@@ -469,7 +465,7 @@ and pr_atom1 env = function
| TacIntroMove (ido1,Some id2) ->
hov 1
(str "intro" ++ pr_opt pr_id ido1 ++ spc () ++ str "after " ++
- pr_located pr_id id2)
+ pr_lident id2)
| TacAssumption as t -> pr_atom0 env t
| TacExact c -> hov 1 (str "exact" ++ pr_constrarg env c)
| TacApply cb -> hov 1 (str "apply" ++ spc () ++ pr_with_bindings env cb)
@@ -578,9 +574,9 @@ and pr_atom1 env = function
(* | TacAutoTDB None as x -> pr_atom0 env x
| TacAutoTDB (Some n) -> hov 0 (str "autotdb" ++ spc () ++ int n)
| TacDestructHyp (true,id) ->
- hov 0 (str "cdhyp" ++ spc () ++ pr_located pr_id id)
+ hov 0 (str "cdhyp" ++ spc () ++ pr_lident id)
| TacDestructHyp (false,id) ->
- hov 0 (str "dhyp" ++ spc () ++ pr_located pr_id id)
+ hov 0 (str "dhyp" ++ spc () ++ pr_lident id)
| TacDestructConcl as x -> pr_atom0 env x
| TacSuperAuto (n,l,b1,b2) ->
hov 1 (str "superauto" ++ pr_opt int n ++ pr_autoarg_adding l ++
@@ -749,8 +745,7 @@ let rec pr_tac env inherited tac =
pr_with_comments loc (hov 1 (pr_atom1 env t)), ltatom
| TacArg(Tacexp e) -> pr_tac0 env e, latom
| TacArg(ConstrMayEval (ConstrTerm c)) ->
- if is_ident c then pr_constr env c, latom
- else str "constr:" ++ pr_constr env c, latom
+ str "constr:" ++ pr_constr env c, latom
| TacArg(ConstrMayEval c) ->
pr_may_eval (pr_constr env) (pr_lconstr env) (pr_cst env) c, leval
| TacArg(TacFreshId sopt) -> str "fresh" ++ pr_opt qsnew sopt, latom
@@ -795,10 +790,6 @@ let strip_prod_binders_rawterm n (ty,_) =
| _ -> error "Cannot translate fix tactic: not enough products" in
strip_ty [] n ty
-let is_ident_rawterm = function
- (Rawterm.RRef(_,VarRef _),_) -> true
- | _ -> false
-
let strip_prod_binders_constr n ty =
let rec strip_ty acc n ty =
if n=0 then (List.rev acc, ty) else
@@ -818,9 +809,9 @@ let rec raw_printers =
(fun _ -> pr_reference),
(fun _ -> pr_reference),
pr_reference,
- pr_or_metaid (pr_located pr_id),
+ pr_or_metaid pr_lident,
Pptactic.pr_raw_extend,
- strip_prod_binders_expr, is_ident_expr)
+ strip_prod_binders_expr)
and pr_raw_tactic env (t:raw_tactic_expr) =
pi1 (make_pr_tac raw_printers) env t
@@ -843,9 +834,9 @@ let rec glob_printers =
(fun env -> pr_or_var (pr_and_short_name (pr_evaluable_reference_env env))),
(fun vars -> pr_or_var (pr_inductive vars)),
pr_ltac_or_var (pr_located pr_ltac_constant),
- pr_located pr_id,
+ pr_lident,
Pptactic.pr_glob_extend,
- strip_prod_binders_rawterm, is_ident_rawterm)
+ strip_prod_binders_rawterm)
and pr_glob_tactic env (t:glob_tactic_expr) =
pi1 (make_pr_tac glob_printers) env t
@@ -868,5 +859,5 @@ let (pr_tactic,_,_) =
pr_ltac_constant,
pr_id,
Pptactic.pr_extend,
- strip_prod_binders_constr,Term.isVar)
+ strip_prod_binders_constr)
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 2612a5925..78d8f1bf7 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -28,9 +28,20 @@ open Topconstr
open Decl_kinds
open Tacinterp
+let pr_spc_type = pr_sep_com spc pr_type
+
(* Copie de Nameops *)
let pr_id id = pr_id (Constrextern.v7_to_v8_id id)
+let pr_lident (b,_ as loc,id) =
+ if loc <> dummy_loc then
+ pr_located pr_id ((b,b+String.length(string_of_id id)),id)
+ else pr_id id
+
+let pr_lname = function
+ (loc,Name id) -> pr_lident (loc,id)
+ | lna -> pr_located pr_name lna
+
let pr_ltac_id id = pr_id (id_of_ltac_v7_id id)
let pr_module r =
@@ -99,8 +110,6 @@ let sep_v = fun _ -> str","
let sep_v2 = fun _ -> str"," ++ spc()
let sep_pp = fun _ -> str":"
-let pr_located pr (loc,x) = pr x
-
let pr_ne_sep sep pr = function
[] -> mt()
| l -> sep() ++ pr l
@@ -228,9 +237,9 @@ let pr_hints local db h pr_c pr_pat =
let pr_with_declaration pr_c = function
| CWith_Definition (id,c) ->
let p = pr_c c in
- str"Definition" ++ spc() ++ pr_id id ++ str" := " ++ p
+ str"Definition" ++ spc() ++ pr_lident id ++ str" := " ++ p
| CWith_Module (id,qid) ->
- str"Module" ++ spc() ++ pr_id id ++ str" := " ++
+ str"Module" ++ spc() ++ pr_lident id ++ str" := " ++
pr_located pr_qualid qid
let rec pr_module_type pr_c = function
@@ -248,12 +257,12 @@ let pr_module_vardecls pr_c (idl,mty) =
let m = pr_module_type pr_c mty in
(* Update the Nametab for interpreting the body of module/modtype *)
let lib_dir = Lib.library_dp() in
- List.iter (fun id ->
+ List.iter (fun (_,id) ->
Declaremods.process_module_bindings [id]
[make_mbid lib_dir (string_of_id id),
Modintern.interp_modtype (Global.env()) mty]) idl;
(* Builds the stream *)
- spc() ++ str"(" ++ prlist_with_sep spc pr_id idl ++ str":" ++ m ++ str")"
+ spc() ++ str"(" ++ prlist_with_sep spc pr_lident idl ++ str":" ++ m ++ str")"
let pr_module_binders l pr_c =
(* Effet de bord complexe pour garantir la declaration des noms des
@@ -320,11 +329,15 @@ let pr_and_type_binders_arg bl =
pr_binders_arg bl
let pr_onescheme (id,dep,ind,s) =
- hov 0 (pr_id id ++ str" :=") ++ spc() ++
+ hov 0 (pr_lident id ++ str" :=") ++ spc() ++
hov 0 ((if dep then str"Induction for" else str"Minimality for")
++ spc() ++ pr_reference ind) ++ spc() ++
hov 0 (str"Sort" ++ spc() ++ pr_sort s)
+let begin_of_inductive = function
+ [] -> 0
+ | (_,(((b,_),_),_))::_ -> b
+
let pr_class_rawexpr = function
| FunClass -> str"Funclass"
| SortClass -> str"Sortclass"
@@ -344,7 +357,7 @@ let pr_assumption_token many = function
anomaly "Don't know how to translate a local conjecture"
let pr_params pr_c (xl,(c,t)) =
- hov 2 (prlist_with_sep sep pr_id xl ++ spc() ++
+ hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++
(if c then str":>" else str":" ++
spc() ++ pr_c t))
@@ -467,8 +480,8 @@ let rec pr_vernac = function
| VernacSuspend -> str"Suspend"
| VernacUnfocus -> str"Unfocus"
| VernacGoal c -> str"Goal" ++ pr_lconstrarg c
- | VernacAbort id -> str"Abort" ++ pr_opt (pr_located pr_id) id
- | VernacResume id -> str"Resume" ++ pr_opt (pr_located pr_id) id
+ | VernacAbort id -> str"Abort" ++ pr_opt pr_lident id
+ | VernacResume id -> str"Resume" ++ pr_opt pr_lident id
| VernacUndo i -> if i=1 then str"Undo" else str"Undo" ++ pr_intarg i
| VernacFocus i -> str"Focus" ++ pr_opt int i
| VernacGo g ->
@@ -496,7 +509,7 @@ let rec pr_vernac = function
| VernacDebug b -> pr_topcmd b
(* Resetting *)
- | VernacResetName id -> str"Reset" ++ spc() ++ pr_located pr_id id
+ | VernacResetName id -> str"Reset" ++ spc() ++ pr_lident id
| VernacResetInitial -> str"Reset Initial"
| VernacBack i -> if i=1 then str"Back" else str"Back" ++ pr_intarg i
@@ -512,7 +525,7 @@ let rec pr_vernac = function
| VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose"
++ spc()) else spc() ++ qsnew s
| VernacTime v -> str"Time" ++ spc() ++ pr_vernac v
- | VernacVar id -> pr_id id
+ | VernacVar id -> pr_lident id
(* Syntax *)
| VernacGrammar _ ->
@@ -607,9 +620,10 @@ let rec pr_vernac = function
| Some ty ->
let bl2,body,ty' = extract_def_binders c ty in
(bl2,CCast (dummy_loc,body,ty'),
- spc() ++ str":" ++ spc () ++
- pr_type_env_n (Global.env())
- (local_binders_length bl + local_binders_length bl2)
+ spc() ++ str":" ++
+ pr_sep_com spc
+ (pr_type_env_n (Global.env())
+ (local_binders_length bl + local_binders_length bl2))
(prod_rawconstr ty bl)) in
let n = local_binders_length bl + local_binders_length bl2 in
let iscast = d <> None in
@@ -618,26 +632,26 @@ let rec pr_vernac = function
(abstract_rawconstr (abstract_rawconstr body bl2) bl) in
(pr_binders_arg bindings,ty,Some (pr_reduce red ++ ppred))
| ProveBody (bl,t) ->
- (pr_and_type_binders_arg bl, str" :" ++ spc () ++ pr_type t, None)
+ (pr_and_type_binders_arg bl, str" :" ++ pr_spc_type t, None)
in
let (binds,typ,c) = pr_def_body b in
- hov 2 (pr_def_token d ++ spc() ++ pr_id id ++ binds ++ typ ++
+ hov 2 (pr_def_token d ++ spc() ++ pr_lident id ++ binds ++ typ ++
(match c with
| None -> mt()
| Some cc -> str" :=" ++ spc() ++ cc))
| VernacStartTheoremProof (ki,id,(bl,c),b,d) ->
- hov 1 (pr_thm_token ki ++ spc() ++ pr_id id ++ spc() ++
+ hov 1 (pr_thm_token ki ++ spc() ++ pr_lident id ++ spc() ++
(match bl with
| [] -> mt()
| _ -> error "Statements with local binders no longer supported")
- ++ str":" ++ spc() ++ pr_type (rename_bound_variables id c))
+ ++ str":" ++ pr_spc_type (rename_bound_variables (snd id) c))
| VernacEndProof Admitted -> str"Admitted"
| VernacEndProof (Proved (opac,o)) -> (match o with
| None -> if opac then str"Qed" else str"Defined"
| Some (id,th) -> (match th with
- | None -> (if opac then str"Save" else str"Defined") ++ spc() ++ pr_id id
- | Some tok -> str"Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_id id))
+ | None -> (if opac then str"Save" else str"Defined") ++ spc() ++ pr_lident id
+ | Some tok -> str"Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id))
| VernacExactProof c ->
hov 2 (str"Proof" ++ pr_lconstrarg c)
| VernacAssumption (stre,l) ->
@@ -668,7 +682,7 @@ let rec pr_vernac = function
let (ind_env,ind_impls,arityl) =
List.fold_left
- (fun (env, ind_impls, arl) (recname, _, _, arityc, _) ->
+ (fun (env, ind_impls, arl) ((_,recname), _, _, arityc, _) ->
let arity = Constrintern.interp_type sigma env_params arityc in
let fullarity = Termops.it_mkProd_or_LetIn arity params in
let env' = Termops.push_rel_assum (Name recname,fullarity) env in
@@ -686,7 +700,7 @@ let rec pr_vernac = function
let lparnames = List.map (fun (na,_,_) -> na) params in
let impl = List.map
- (fun (recname,_,_,arityc,_) ->
+ (fun ((_,recname),_,_,arityc,_) ->
let arity = Constrintern.interp_type sigma env_params arityc in
let fullarity =
Termops.prod_it arity (List.map (fun (id,_,ty) -> (id,ty)) params)
@@ -707,18 +721,20 @@ let rec pr_vernac = function
(* Fin calcul implicites *)
let pr_constructor (coe,(id,c)) =
- hov 2 (pr_id id ++ str" " ++
- (if coe then str":>" else str":") ++ spc () ++
- pr_type_env_n ind_env_params 0 c) in
+ hov 2 (pr_lident id ++ str" " ++
+ (if coe then str":>" else str":") ++
+ pr_sep_com spc (pr_type_env_n ind_env_params 0) c) in
let pr_constructor_list l = match l with
| [] -> mt()
| _ ->
- fnl() ++ str (if List.length l = 1 then " " else " | ") ++
+ pr_com_at (begin_of_inductive l) ++
+ fnl() ++
+ str (if List.length l = 1 then " " else " | ") ++
prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l in
let pr_oneind key (id,ntn,indpar,s,lc) =
hov 0 (
str key ++ spc() ++
- pr_id id ++ pr_and_type_binders_arg indpar ++ spc() ++ str":" ++
+ pr_lident id ++ pr_and_type_binders_arg indpar ++ spc() ++ str":" ++
spc() ++ pr_type s ++
str" :=") ++ pr_constructor_list lc ++
pr_decl_notation pr_constr ntn in
@@ -811,29 +827,29 @@ let rec pr_vernac = function
| VernacRecord (b,(oc,name),ps,s,c,fs) ->
let pr_record_field = function
| (oc,AssumExpr (id,t)) ->
- hov 1 (pr_id id ++
+ hov 1 (pr_lident id ++
(if oc then str" :>" else str" :") ++ spc() ++
pr_type t)
| (oc,DefExpr(id,b,opt)) -> (match opt with
| Some t ->
- hov 1 (pr_id id ++
+ hov 1 (pr_lident id ++
(if oc then str" :>" else str" :") ++ spc() ++
pr_type t ++ str" :=" ++ pr_lconstr b)
| None ->
- hov 1 (pr_id id ++ str" :=" ++ spc() ++
+ hov 1 (pr_lident id ++ str" :=" ++ spc() ++
pr_lconstr b)) in
hov 2
(str (if b then "Record" else "Structure") ++
- (if oc then str" > " else str" ") ++ pr_id name ++
+ (if oc then str" > " else str" ") ++ pr_lident name ++
pr_and_type_binders_arg ps ++ str" :" ++ spc() ++ pr_type s ++
str" := " ++
(match c with
| None -> mt()
- | Some sc -> pr_id sc) ++
+ | Some sc -> pr_lident sc) ++
spc() ++ str"{" ++
hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}"))
- | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_id id)
- | VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_id id)
+ | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_lident id)
+ | VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_lident id)
| VernacRequire (exp,spe,l) -> hov 2
(str "Require" ++ pr_require_token exp ++ spc() ++
(match spe with
@@ -855,24 +871,24 @@ let rec pr_vernac = function
| VernacIdentityCoercion (s,id,c1,c2) ->
hov 1 (
str"Identity Coercion" ++ (match s with | Local -> spc() ++
- str"Local" ++ spc() | Global -> spc()) ++ pr_id id ++
+ str"Local" ++ spc() | Global -> spc()) ++ pr_lident id ++
spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++
spc() ++ pr_class_rawexpr c2)
(* Modules and Module Types *)
| VernacDefineModule (m,bl,ty,bd) ->
let b = pr_module_binders_list bl pr_lconstr in
- hov 2 (str"Module " ++ pr_id m ++ b ++
+ hov 2 (str"Module " ++ pr_lident m ++ b ++
pr_opt (pr_of_module_type pr_lconstr) ty ++
pr_opt (fun me -> str ":= " ++ pr_module_expr me) bd)
| VernacDeclareModule (id,bl,m1,m2) ->
let b = pr_module_binders_list bl pr_lconstr in
- hov 2 (str"Declare Module " ++ pr_id id ++ b ++
+ hov 2 (str"Declare Module " ++ pr_lident id ++ b ++
pr_opt (pr_of_module_type pr_lconstr) m1 ++
pr_opt (fun me -> str ":= " ++ pr_module_expr me) m2)
| VernacDeclareModuleType (id,bl,m) ->
let b = pr_module_binders_list bl pr_lconstr in
- hov 2 (str"Module Type " ++ pr_id id ++ b ++
+ hov 2 (str"Module Type " ++ pr_lident id ++ b ++
pr_opt (fun mt -> str ":= " ++ pr_module_type pr_lconstr mt) m)
(* Solving *)
@@ -919,7 +935,8 @@ let rec pr_vernac = function
| Tacexpr.TacFun (idl,b) -> idl,b
| _ -> [], body in
pr_located pr_ltac_id id ++
- prlist (function None -> str " _" | Some id -> spc () ++ pr_id id) idl
+ prlist (function None -> str " _"
+ | Some id -> spc () ++ pr_id id) idl
++ str" :=" ++ brk(1,1) ++
let idl = List.map out_some (List.filter (fun x -> not (x=None)) idl)in
pr_raw_tactic_env
@@ -935,10 +952,10 @@ let rec pr_vernac = function
| VernacHints (local,dbnames,h) ->
pr_hints local dbnames h pr_constr pr_pattern
| VernacSyntacticDefinition (id,c,None) ->
- hov 2 (str"Syntactic Definition " ++ pr_id id ++ str" :=" ++
+ hov 2 (str"Syntactic Definition " ++ pr_lident id ++ str" :=" ++
pr_lconstrarg c)
| VernacSyntacticDefinition (id,c,Some n) ->
- hov 2 (str"Syntactic Definition " ++ pr_id id ++ str" :=" ++
+ hov 2 (str"Syntactic Definition " ++ pr_lident id ++ str" :=" ++
pr_lconstrarg c ++ spc() ++ str"|" ++ int n)
| VernacDeclareImplicits (q,None) ->
hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q)
@@ -951,7 +968,7 @@ 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_id idl ++ str " :" ++ spc () ++ pr_type c)
+ prlist_with_sep spc pr_lident idl ++ str " :" ++ spc () ++ pr_type c)
| VernacSetOpacity (fl,l) ->
hov 1 ((if fl then str"Opaque" else str"Transparent") ++
spc() ++ prlist_with_sep sep pr_reference l)