diff options
33 files changed, 567 insertions, 463 deletions
@@ -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) |