From c70bdc0f7ddfca7055d1af4d81086485518056af Mon Sep 17 00:00:00 2001 From: filliatr Date: Sun, 5 Dec 1999 18:46:38 +0000 Subject: premier debugage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@210 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend | 94 +++++++++++++++++++++-------------------- .depend.camlp4 | 24 ++++++----- Makefile | 19 ++++++++- dev/changements.txt | 14 +++++++ proofs/clenv.ml | 2 +- proofs/pfedit.ml | 2 +- proofs/pfedit.mli | 2 + tactics/auto.mli | 8 +--- tactics/pattern.ml | 11 ++--- tactics/pattern.mli | 4 +- tactics/tacticals.ml | 3 +- toplevel/class.ml | 11 +++-- toplevel/command.ml | 22 +++++++--- toplevel/errors.ml | 3 ++ toplevel/himsg.ml | 104 +++++++++++++++++++++++++++++++++++++--------- toplevel/himsg.mli | 5 ++- toplevel/metasyntax.ml | 17 ++++---- toplevel/mltop.ml4 | 2 +- toplevel/toplevel.ml | 5 ++- toplevel/vernacentries.ml | 4 +- 20 files changed, 232 insertions(+), 124 deletions(-) diff --git a/.depend b/.depend index b5035826f..6f95ece8c 100644 --- a/.depend +++ b/.depend @@ -109,8 +109,8 @@ proofs/logic.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \ proofs/macros.cmi: parsing/ast.cmi parsing/coqast.cmi kernel/names.cmi \ proofs/proof_trees.cmi proofs/tacmach.cmi proofs/pfedit.cmi: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \ - lib/pp.cmi proofs/proof_trees.cmi kernel/sign.cmi proofs/tacmach.cmi \ - kernel/term.cmi + kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi kernel/sign.cmi \ + proofs/tacmach.cmi kernel/term.cmi proofs/proof_trees.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi lib/pp.cmi kernel/sign.cmi lib/stamps.cmi \ kernel/term.cmi lib/util.cmi @@ -154,8 +154,8 @@ toplevel/command.cmi: parsing/coqast.cmi library/declare.cmi kernel/names.cmi \ toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi toplevel/fhimsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi -toplevel/himsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ - kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi +toplevel/himsg.cmi: kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \ + kernel/sign.cmi kernel/type_errors.cmi toplevel/metasyntax.cmi: parsing/coqast.cmi parsing/extend.cmi toplevel/mltop.cmi: library/libobject.cmi toplevel/protectedtoplevel.cmi: lib/pp.cmi @@ -193,7 +193,7 @@ dev/top_printers.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \ tactics/elim.cmx kernel/environ.cmx parsing/esyntax.cmx kernel/evd.cmx \ kernel/generic.cmx kernel/inductive.cmx parsing/lexer.cmx \ library/libobject.cmx library/library.cmx toplevel/metasyntax.cmx \ - toplevel/mltop.cmx kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx \ + toplevel/mltop.cmi kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx \ parsing/pretty.cmx parsing/printer.cmx proofs/proof_trees.cmx \ kernel/reduction.cmx proofs/refiner.cmx kernel/sign.cmx kernel/sosub.cmx \ library/states.cmx library/summary.cmx lib/system.cmx \ @@ -405,7 +405,7 @@ library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \ parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi lib/hashcons.cmi \ kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx lib/hashcons.cmx \ - kernel/names.cmx parsing/pcoq.cmi lib/pp.cmx lib/util.cmx parsing/ast.cmi + kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/ast.cmi parsing/astterm.cmo: parsing/ast.cmi kernel/closure.cmi parsing/coqast.cmi \ library/declare.cmi kernel/environ.cmi pretyping/evarutil.cmi \ kernel/evd.cmi kernel/generic.cmi library/global.cmi library/impargs.cmi \ @@ -416,7 +416,7 @@ parsing/astterm.cmo: parsing/ast.cmi kernel/closure.cmi parsing/coqast.cmi \ parsing/astterm.cmx: parsing/ast.cmx kernel/closure.cmx parsing/coqast.cmx \ library/declare.cmx kernel/environ.cmx pretyping/evarutil.cmx \ kernel/evd.cmx kernel/generic.cmx library/global.cmx library/impargs.cmx \ - kernel/names.cmx library/nametab.cmx parsing/pcoq.cmi lib/pp.cmx \ + kernel/names.cmx library/nametab.cmx parsing/pcoq.cmx lib/pp.cmx \ pretyping/pretyping.cmx pretyping/rawterm.cmi kernel/reduction.cmx \ kernel/sign.cmx pretyping/syntax_def.cmx pretyping/tacred.cmx \ kernel/term.cmx pretyping/typing.cmx lib/util.cmx parsing/astterm.cmi @@ -425,27 +425,35 @@ parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx parsing/coqast.cmi parsing/egrammar.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \ parsing/lexer.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi \ parsing/egrammar.cmi -parsing/egrammar.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmi \ - parsing/lexer.cmx parsing/pcoq.cmi lib/pp.cmx lib/util.cmx \ +parsing/egrammar.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmx \ + parsing/lexer.cmx parsing/pcoq.cmx lib/pp.cmx lib/util.cmx \ parsing/egrammar.cmi parsing/esyntax.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \ lib/gmap.cmi lib/gmapl.cmi lib/pp.cmi lib/util.cmi parsing/esyntax.cmi -parsing/esyntax.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmi \ +parsing/esyntax.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmx \ lib/gmap.cmx lib/gmapl.cmx lib/pp.cmx lib/util.cmx parsing/esyntax.cmi +parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/lexer.cmi \ + parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/extend.cmi +parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/lexer.cmx \ + parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/extend.cmi parsing/g_natsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \ parsing/coqast.cmi parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi \ lib/pp.cmi lib/util.cmi parsing/g_natsyntax.cmi parsing/g_natsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \ - parsing/coqast.cmx parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmi \ + parsing/coqast.cmx parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmx \ lib/pp.cmx lib/util.cmx parsing/g_natsyntax.cmi parsing/g_zsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \ parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \ - lib/util.cmi + lib/util.cmi parsing/g_zsyntax.cmi parsing/g_zsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \ - parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmi lib/pp.cmx \ - lib/util.cmx + parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx \ + lib/util.cmx parsing/g_zsyntax.cmi parsing/lexer.cmo: lib/util.cmi parsing/lexer.cmi parsing/lexer.cmx: lib/util.cmx parsing/lexer.cmi +parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \ + lib/util.cmi parsing/pcoq.cmi +parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \ + lib/util.cmx parsing/pcoq.cmi parsing/pretty.cmo: pretyping/classops.cmi kernel/constant.cmi \ library/declare.cmi kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \ library/global.cmi library/impargs.cmi kernel/inductive.cmi \ @@ -468,7 +476,7 @@ parsing/printer.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \ kernel/sign.cmi kernel/term.cmi parsing/termast.cmi lib/util.cmi \ parsing/printer.cmi parsing/printer.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \ - parsing/esyntax.cmx parsing/extend.cmi library/global.cmx \ + parsing/esyntax.cmx parsing/extend.cmx library/global.cmx \ kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \ kernel/sign.cmx kernel/term.cmx parsing/termast.cmx lib/util.cmx \ parsing/printer.cmi @@ -612,7 +620,7 @@ proofs/macros.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \ kernel/term.cmi lib/util.cmi proofs/macros.cmi proofs/macros.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ library/libobject.cmx library/library.cmx kernel/names.cmx \ - parsing/pcoq.cmi lib/pp.cmx proofs/proof_trees.cmx library/summary.cmx \ + parsing/pcoq.cmx lib/pp.cmx proofs/proof_trees.cmx library/summary.cmx \ kernel/term.cmx lib/util.cmx proofs/macros.cmi proofs/pfedit.cmo: parsing/astterm.cmi kernel/constant.cmi \ library/declare.cmi lib/edit.cmi kernel/environ.cmi kernel/evd.cmi \ @@ -727,7 +735,7 @@ tactics/pattern.cmo: proofs/clenv.cmi kernel/environ.cmi kernel/evd.cmi \ lib/pp.cmi proofs/proof_trees.cmi kernel/reduction.cmi kernel/sosub.cmi \ tactics/stock.cmi kernel/term.cmi lib/util.cmi tactics/pattern.cmi tactics/pattern.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \ - kernel/generic.cmx library/global.cmx kernel/names.cmx parsing/pcoq.cmi \ + kernel/generic.cmx library/global.cmx kernel/names.cmx parsing/pcoq.cmx \ lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx kernel/sosub.cmx \ tactics/stock.cmx kernel/term.cmx lib/util.cmx tactics/pattern.cmi tactics/stock.cmo: lib/bij.cmi lib/gmap.cmi lib/gmapl.cmi library/library.cmi \ @@ -787,7 +795,7 @@ toplevel/class.cmo: pretyping/classops.cmi kernel/constant.cmi \ toplevel/class.cmx: pretyping/classops.cmx kernel/constant.cmx \ library/declare.cmx kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \ library/global.cmx kernel/inductive.cmx kernel/instantiate.cmx \ - library/lib.cmx toplevel/metasyntax.cmx kernel/names.cmx parsing/pcoq.cmi \ + library/lib.cmx toplevel/metasyntax.cmx kernel/names.cmx parsing/pcoq.cmx \ lib/pp.cmx pretyping/retyping.cmx kernel/term.cmx pretyping/typing.cmx \ lib/util.cmx toplevel/class.cmi toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/constant.cmi \ @@ -807,7 +815,7 @@ toplevel/command.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/constant.cmx \ toplevel/coqinit.cmo: config/coq_config.cmi toplevel/mltop.cmi \ lib/options.cmi lib/pp.cmi lib/system.cmi toplevel/toplevel.cmi \ toplevel/vernac.cmi toplevel/coqinit.cmi -toplevel/coqinit.cmx: config/coq_config.cmx toplevel/mltop.cmx \ +toplevel/coqinit.cmx: config/coq_config.cmx toplevel/mltop.cmi \ lib/options.cmx lib/pp.cmx lib/system.cmx toplevel/toplevel.cmx \ toplevel/vernac.cmx toplevel/coqinit.cmi toplevel/coqtop.cmo: config/coq_config.cmi toplevel/coqinit.cmi \ @@ -816,14 +824,16 @@ toplevel/coqtop.cmo: config/coq_config.cmi toplevel/coqinit.cmi \ library/states.cmi lib/system.cmi toplevel/toplevel.cmi \ toplevel/usage.cmi lib/util.cmi toplevel/vernac.cmi toplevel/coqtop.cmx: config/coq_config.cmx toplevel/coqinit.cmx \ - toplevel/errors.cmx library/library.cmx toplevel/mltop.cmx \ + toplevel/errors.cmx library/library.cmx toplevel/mltop.cmi \ lib/options.cmx lib/pp.cmx parsing/printer.cmx lib/profile.cmx \ library/states.cmx lib/system.cmx toplevel/toplevel.cmx \ toplevel/usage.cmx lib/util.cmx toplevel/vernac.cmx -toplevel/errors.cmo: parsing/ast.cmi toplevel/himsg.cmi lib/options.cmi \ - lib/pp.cmi kernel/type_errors.cmi lib/util.cmi toplevel/errors.cmi -toplevel/errors.cmx: parsing/ast.cmx toplevel/himsg.cmx lib/options.cmx \ - lib/pp.cmx kernel/type_errors.cmx lib/util.cmx toplevel/errors.cmi +toplevel/errors.cmo: parsing/ast.cmi toplevel/himsg.cmi kernel/inductive.cmi \ + lib/options.cmi lib/pp.cmi kernel/type_errors.cmi lib/util.cmi \ + toplevel/errors.cmi +toplevel/errors.cmx: parsing/ast.cmx toplevel/himsg.cmx kernel/inductive.cmx \ + lib/options.cmx lib/pp.cmx kernel/type_errors.cmx lib/util.cmx \ + toplevel/errors.cmi toplevel/fhimsg.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \ lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \ kernel/type_errors.cmi lib/util.cmi toplevel/fhimsg.cmi @@ -831,22 +841,24 @@ toplevel/fhimsg.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \ lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \ kernel/type_errors.cmx lib/util.cmx toplevel/fhimsg.cmi toplevel/himsg.cmo: parsing/ast.cmi kernel/environ.cmi kernel/generic.cmi \ - kernel/names.cmi lib/options.cmi lib/pp.cmi parsing/printer.cmi \ - kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/type_errors.cmi lib/util.cmi toplevel/himsg.cmi + kernel/inductive.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \ + parsing/pretty.cmi parsing/printer.cmi kernel/reduction.cmi \ + kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi lib/util.cmi \ + toplevel/himsg.cmi toplevel/himsg.cmx: parsing/ast.cmx kernel/environ.cmx kernel/generic.cmx \ - kernel/names.cmx lib/options.cmx lib/pp.cmx parsing/printer.cmx \ - kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \ - kernel/type_errors.cmx lib/util.cmx toplevel/himsg.cmi + kernel/inductive.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \ + parsing/pretty.cmx parsing/printer.cmx kernel/reduction.cmx \ + kernel/sign.cmx kernel/term.cmx kernel/type_errors.cmx lib/util.cmx \ + toplevel/himsg.cmi toplevel/metasyntax.cmo: parsing/ast.cmi parsing/coqast.cmi \ parsing/egrammar.cmi parsing/esyntax.cmi parsing/extend.cmi \ library/lib.cmi library/libobject.cmi library/library.cmi \ parsing/pcoq.cmi lib/pp.cmi library/summary.cmi lib/util.cmi \ toplevel/metasyntax.cmi toplevel/metasyntax.cmx: parsing/ast.cmx parsing/coqast.cmx \ - parsing/egrammar.cmx parsing/esyntax.cmx parsing/extend.cmi \ + parsing/egrammar.cmx parsing/esyntax.cmx parsing/extend.cmx \ library/lib.cmx library/libobject.cmx library/library.cmx \ - parsing/pcoq.cmi lib/pp.cmx library/summary.cmx lib/util.cmx \ + parsing/pcoq.cmx lib/pp.cmx library/summary.cmx lib/util.cmx \ toplevel/metasyntax.cmi toplevel/minicoq.cmo: kernel/constant.cmi toplevel/fhimsg.cmi \ parsing/g_minicoq.cmi kernel/generic.cmi kernel/inductive.cmi \ @@ -856,16 +868,10 @@ toplevel/minicoq.cmx: kernel/constant.cmx toplevel/fhimsg.cmx \ parsing/g_minicoq.cmi kernel/generic.cmx kernel/inductive.cmx \ kernel/names.cmx lib/pp.cmx kernel/safe_typing.cmx kernel/sign.cmx \ kernel/term.cmx kernel/type_errors.cmx lib/util.cmx -toplevel/mltop.cmo: library/lib.cmi library/libobject.cmi library/library.cmi \ - lib/pp.cmi library/summary.cmi lib/system.cmi lib/util.cmi \ - toplevel/vernacinterp.cmi toplevel/mltop.cmi -toplevel/mltop.cmx: library/lib.cmx library/libobject.cmx library/library.cmx \ - lib/pp.cmx library/summary.cmx lib/system.cmx lib/util.cmx \ - toplevel/vernacinterp.cmx toplevel/mltop.cmi toplevel/protectedtoplevel.cmo: toplevel/errors.cmi parsing/pcoq.cmi \ lib/pp.cmi toplevel/vernac.cmi toplevel/vernacinterp.cmi \ toplevel/protectedtoplevel.cmi -toplevel/protectedtoplevel.cmx: toplevel/errors.cmx parsing/pcoq.cmi \ +toplevel/protectedtoplevel.cmx: toplevel/errors.cmx parsing/pcoq.cmx \ lib/pp.cmx toplevel/vernac.cmx toplevel/vernacinterp.cmx \ toplevel/protectedtoplevel.cmi toplevel/record.cmo: parsing/ast.cmi toplevel/class.cmi parsing/coqast.cmi \ @@ -878,8 +884,8 @@ toplevel/toplevel.cmo: parsing/ast.cmi toplevel/errors.cmi toplevel/mltop.cmi \ lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \ toplevel/protectedtoplevel.cmi lib/util.cmi toplevel/vernac.cmi \ toplevel/vernacinterp.cmi toplevel/toplevel.cmi -toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmx \ - lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmx lib/pp.cmx \ +toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmi \ + lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \ toplevel/protectedtoplevel.cmx lib/util.cmx toplevel/vernac.cmx \ toplevel/vernacinterp.cmx toplevel/toplevel.cmi toplevel/usage.cmo: toplevel/usage.cmi @@ -889,7 +895,7 @@ toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/library.cmi \ library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \ toplevel/vernac.cmi toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \ - lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmx lib/pp.cmx \ + lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \ library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \ toplevel/vernac.cmi toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \ @@ -908,10 +914,10 @@ toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \ toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \ toplevel/class.cmx toplevel/command.cmx parsing/coqast.cmx \ library/declare.cmx library/discharge.cmx kernel/environ.cmx \ - kernel/evd.cmx parsing/extend.cmi library/global.cmx library/goptions.cmx \ + kernel/evd.cmx parsing/extend.cmx library/global.cmx library/goptions.cmx \ library/impargs.cmx library/lib.cmx library/libobject.cmx \ library/library.cmx proofs/macros.cmx toplevel/metasyntax.cmx \ - kernel/names.cmx library/nametab.cmx lib/options.cmx parsing/pcoq.cmi \ + kernel/names.cmx library/nametab.cmx lib/options.cmx parsing/pcoq.cmx \ proofs/pfedit.cmx lib/pp.cmx lib/pp_control.cmx parsing/pretty.cmx \ parsing/printer.cmx proofs/proof_trees.cmx kernel/reduction.cmx \ proofs/refiner.cmx lib/stamps.cmx library/states.cmx lib/system.cmx \ diff --git a/.depend.camlp4 b/.depend.camlp4 index 21f83048d..68d5393d3 100644 --- a/.depend.camlp4 +++ b/.depend.camlp4 @@ -1,19 +1,17 @@ parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/lexer.cmi \ - parsing/pcoq.cmi lib/pp.cmi lib/util.cmi toplevel/vernac.cmi \ - parsing/extend.cmi + parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/extend.cmi parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/lexer.cmx \ - parsing/pcoq.cmi lib/pp.cmx lib/util.cmx toplevel/vernac.cmx \ - parsing/extend.cmi + parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/extend.cmi parsing/g_basevernac.cmo: parsing/ast.cmi toplevel/command.cmi \ parsing/coqast.cmi parsing/pcoq.cmi toplevel/vernac.cmi parsing/g_basevernac.cmx: parsing/ast.cmx toplevel/command.cmx \ - parsing/coqast.cmx parsing/pcoq.cmi toplevel/vernac.cmx + parsing/coqast.cmx parsing/pcoq.cmx toplevel/vernac.cmx parsing/g_cases.cmo: toplevel/command.cmi parsing/coqast.cmi parsing/pcoq.cmi -parsing/g_cases.cmx: toplevel/command.cmx parsing/coqast.cmx parsing/pcoq.cmi +parsing/g_cases.cmx: toplevel/command.cmx parsing/coqast.cmx parsing/pcoq.cmx parsing/g_command.cmo: parsing/ast.cmi toplevel/command.cmi \ parsing/coqast.cmi parsing/pcoq.cmi parsing/g_command.cmx: parsing/ast.cmx toplevel/command.cmx \ - parsing/coqast.cmx parsing/pcoq.cmi + parsing/coqast.cmx parsing/pcoq.cmx parsing/g_minicoq.cmo: kernel/generic.cmi parsing/lexer.cmi kernel/names.cmi \ lib/pp.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \ parsing/g_minicoq.cmi @@ -21,18 +19,24 @@ parsing/g_minicoq.cmx: kernel/generic.cmx parsing/lexer.cmx kernel/names.cmx \ lib/pp.cmx kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \ parsing/g_minicoq.cmi parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi -parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmi +parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmx parsing/g_tactic.cmo: parsing/ast.cmi toplevel/command.cmi parsing/coqast.cmi \ parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/g_tactic.cmx: parsing/ast.cmx toplevel/command.cmx parsing/coqast.cmx \ - parsing/pcoq.cmi lib/pp.cmx lib/util.cmx + parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/g_vernac.cmo: toplevel/command.cmi parsing/coqast.cmi \ parsing/pcoq.cmi toplevel/vernac.cmi parsing/g_vernac.cmx: toplevel/command.cmx parsing/coqast.cmx \ - parsing/pcoq.cmi toplevel/vernac.cmx + parsing/pcoq.cmx toplevel/vernac.cmx parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \ lib/util.cmi parsing/pcoq.cmi parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \ lib/util.cmx parsing/pcoq.cmi parsing/q_coqast.cmo: parsing/coqast.cmi parsing/pcoq.cmi parsing/q_coqast.cmx: parsing/coqast.cmx parsing/pcoq.cmi +toplevel/mltop.cmo: library/lib.cmi library/libobject.cmi library/library.cmi \ + lib/pp.cmi library/summary.cmi lib/system.cmi lib/util.cmi \ + toplevel/vernacinterp.cmi toplevel/mltop.cmi +toplevel/mltop.cmx: library/lib.cmx library/libobject.cmx library/library.cmx \ + lib/pp.cmx library/summary.cmx lib/system.cmx lib/util.cmx \ + toplevel/vernacinterp.cmx toplevel/mltop.cmi diff --git a/Makefile b/Makefile index 15d3839b0..05659ece6 100644 --- a/Makefile +++ b/Makefile @@ -154,6 +154,13 @@ parsing: $(PARSING) pretyping: $(PRETYPING) toplevel: $(TOPLEVEL) +# states + +SYNTAXPP=syntax/PPCommand.v syntax/PPTactic.v syntax/PPMultipleCase.v + +states/barestate.coq: $(SYNTAXPP) coqtop.byte + ./coqtop.byte -q -batch -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate states/barestate.coq + ########################################################################### # minicoq ########################################################################### @@ -256,7 +263,14 @@ parsing/extend.cmx: parsing/extend.ml4 parsing/grammar.cma beforedepend:: $(GRAMMARCMO) -# toplevel/mltop.ml4 (ifdef Opt) +parsing/pcoq.ml: parsing/pcoq.ml4 + $(CAMLP4EXTEND) pr_o.cmo -impl $< -o $@ +parsing/extend.ml: parsing/extend.ml4 parsing/grammar.cma + $(CAMLP4GRAMMAR) pr_o.cmo -impl $< -o $@ + +beforedepend:: parsing/pcoq.ml parsing/extend.ml + +# toplevel/mltop.ml4 (ifdef Byte) CAMLP4IFDEF=camlp4o pa_ifdef.cmo @@ -303,6 +317,7 @@ archclean:: rm -f parsing/*.cmx parsing/*.[so] rm -f pretyping/*.cmx pretyping/*.[so] rm -f toplevel/*.cmx toplevel/*.[so] + rm -f coqtop coqtop.byte minicoq cleanall:: archclean rm -f *~ @@ -333,7 +348,7 @@ dependcamlp4: beforedepend rm -f .depend.camlp4 for f in */*.ml4; do \ file=`dirname $$f`/`basename $$f .ml4`; \ - camlp4o $(INCLUDES) pa_extend.cmo q_MLast.cmo $(GRAMMARCMO) pr_o.cmo -impl $$f > $$file.ml; \ + camlp4o $(INCLUDES) pa_ifdef.cmo pa_extend.cmo q_MLast.cmo $(GRAMMARCMO) pr_o.cmo -impl $$f > $$file.ml; \ ocamldep $(DEPFLAGS) $$file.ml >> .depend.camlp4; \ rm -f $$file.ml; \ done diff --git a/dev/changements.txt b/dev/changements.txt index 92251833f..538424d7f 100644 --- a/dev/changements.txt +++ b/dev/changements.txt @@ -71,3 +71,17 @@ Changements dans les grammaires casse particulière dans Coq) +Changements divers +------------------ + + . il n'y a plus de script coqtop => coqtop et coqtop.byte sont + directement le résultat du link du code + => debuggage et profiling directs + + . il n'y a plus d'installation locale dans bin/ + + . #use "include.ml" => #use "include" + go() => loop() + + . il y "make depend" et "make dependcamlp4" car ce dernier prend beaucoup + de temps diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 0131df8b9..c53c46233 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -881,7 +881,7 @@ let clenv_type_of ce c = | (n,Cltyp typ) -> (n,typ.rebus)) (intmap_to_list ce.env) in - failwith "TODO" + failwith "clenv_type_of: TODO" (*** (Pretyping.ise_resolve true (w_Underlying ce.hook) metamap (gLOB(w_hyps ce.hook)) c).uj_type diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 9fc376855..6e6114f90 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -228,7 +228,7 @@ let abort_refine f x = f x (* used to be: error "Must save or abort current goal first" *) -let reset_name = abort_refine reset_to +let reset_name = abort_refine reset_name (*** TODO and reset_keeping_name = abort_refine reset_keeping and reset_section = abort_refine raw_reset_section diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 966630eae..9a528f555 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -3,6 +3,7 @@ (*i*) open Pp +open Names open Term open Sign open Environ @@ -50,6 +51,7 @@ val proof_term : unit -> constr val start_proof : string -> strength -> Coqast.t -> unit val start_proof_constr : string -> strength -> constr -> unit +val reset_name : identifier -> unit val save_named : bool -> unit val save_anonymous : bool -> string -> 'a -> unit diff --git a/tactics/auto.mli b/tactics/auto.mli index 01a2d5f6d..333aca134 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -17,9 +17,7 @@ type auto_tactic = | Give_exact of constr | Res_pf_THEN_trivial_fail of constr * unit clausenv (* Hint Immediate *) | Unfold_nth of constr (* Hint Unfold *) - (***TODO - | Extern of CoqAst.t (* Hint Extern *) - ***) + | Extern of Coqast.t (* Hint Extern *) type pri_auto_tactic = { hname : identifier; (* name of the hint *) @@ -87,10 +85,8 @@ val make_resolve_hyp : identifier -> constr -> (constr * pri_auto_tactic) list (* [make_extern name pri pattern tactic_ast] *) -(***TODO val make_extern : - identifier -> int -> constr -> CoqAst.t -> constr * pri_auto_tactic -***) + identifier -> int -> constr -> Coqast.t -> constr * pri_auto_tactic (* Create a Hint database from the pairs (name, constr). Useful to take the current goal hypotheses as hints *) diff --git a/tactics/pattern.ml b/tactics/pattern.ml index 52b6586b5..5ff9a6294 100644 --- a/tactics/pattern.ml +++ b/tactics/pattern.ml @@ -28,12 +28,9 @@ let rec whd_replmeta = function | DOP2(Cast,c,_) -> whd_replmeta c | c -> c -let raw_sopattern_of_compattern sign com = - failwith "raw_sopattern_of_compattern: TODO" - (*** - let c = Astterm.raw_constr_of_compattern Evd.empty (gLOB sign) com in - strong whd_replmeta c - ***) +let raw_sopattern_of_compattern env com = + let c = Astterm.constr_of_com_pattern Evd.empty env com in + strong (fun _ _ -> whd_replmeta) env Evd.empty c let parse_pattern s = let com = @@ -42,7 +39,7 @@ let parse_pattern s = with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) -> error "Malformed pattern" in - raw_sopattern_of_compattern (Global.context()) com + raw_sopattern_of_compattern (Global.env()) com let (pattern_stock : constr Stock.stock) = Stock.make_stock {name="PATTERN";proc=parse_pattern} diff --git a/tactics/pattern.mli b/tactics/pattern.mli index fc9d07ef7..afe1ec848 100644 --- a/tactics/pattern.mli +++ b/tactics/pattern.mli @@ -47,9 +47,7 @@ val put_pat : module_mark -> string -> marked_term val get_pat : marked_term -> constr val pattern_stock : constr Stock.stock -(*i** -val raw_sopattern_of_compattern : typed_type signature -> CoqAst.t -> constr -**i*) +val raw_sopattern_of_compattern : Environ.env -> Coqast.t -> constr (*s Second part : Given a term with second-order variables in it, represented by Meta's, and possibly applied using \verb!XTRA[$SOAPP]! to diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 6fb962f2c..ff5d324a3 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -16,6 +16,7 @@ open Proof_trees open Clenv open Pattern open Wcclausenv +open Pretty (******************************************) (* Basic Tacticals *) @@ -197,7 +198,7 @@ let conclPattern concl pat tacast gl = List.map (fun (i,c) -> (i, Termast.bdize false (assumptions_for_print []) c)) constr_bindings in - let tacast' = CoqAst.subst_meta ast_bindings tacast in + let tacast' = Coqast.subst_meta ast_bindings tacast in Tacinterp.interp tacast' gl ***) diff --git a/toplevel/class.ml b/toplevel/class.ml index dbd088555..35e8e5b87 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -328,12 +328,11 @@ let coercion_syntax idf ps clt = | _ -> coercion_syntax_entry idf ps let add_new_coercion_in_graph1 (coef,v,stre,isid,cls,clt) idf ps = - let _ = add_anonymous_leaf - (inCoercion - ((coef, - {cOE_VALUE=v;cOE_STRE=stre;cOE_ISID=isid;cOE_PARAM=ps}), - cls,clt)) - in + add_anonymous_leaf + (inCoercion + ((coef, + {cOE_VALUE=v;cOE_STRE=stre;cOE_ISID=isid;cOE_PARAM=ps}), + cls,clt)); coercion_syntax idf ps clt (* diff --git a/toplevel/command.ml b/toplevel/command.ml index c4f4622d7..7ce0d13e8 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -72,19 +72,24 @@ let parameter_def_var ident c = declare_parameter (id_of_string ident) c let hypothesis_def_var is_refining ident n c = + let warning () = + mSGERRNL [< 'sTR"Warning: "; 'sTR ident; + 'sTR" is declared as a parameter"; + 'sTR" because it is at a global level" >] + in match n with - | NeverDischarge -> parameter_def_var ident c + | NeverDischarge -> + warning(); + parameter_def_var ident c | DischargeAt disch_sp -> if Lib.is_section_p disch_sp then begin declare_variable (id_of_string ident) (constr_of_com1 true Evd.empty (Global.env()) c,n,false); if is_refining then - mSGERRNL [< 'sTR"Warning: Variable " ; 'sTR ident ; + mSGERRNL [< 'sTR"Warning: Variable "; 'sTR ident; 'sTR" is not visible from current goals" >] end else begin - mSGERRNL [< 'sTR"Warning: Declaring " ; 'sTR ident ; - 'sTR" as a parameter rather than a variable " ; - 'sTR" because it is at a global level" >]; + warning(); parameter_def_var ident c end @@ -109,6 +114,11 @@ let corecursive_message = function 'sPC; 'sTR "are corecursively defined">] let build_mutual lparams lnamearconstrs finite = + let allnames = + 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 lrecnames = List.map (fun (x,_,_)->x) lnamearconstrs and nparams = List.length lparams and sigma = Evd.empty @@ -142,8 +152,8 @@ let build_mutual lparams lnamearconstrs finite = mind_entry_finite = finite; mind_entry_inds = mispecvec } in - declare_mind mie; States.unfreeze fs; + declare_mind mie; pPNL(minductive_message lrecnames) with e -> States.unfreeze fs; raise e diff --git a/toplevel/errors.ml b/toplevel/errors.ml index 4029437bf..444d18b42 100644 --- a/toplevel/errors.ml +++ b/toplevel/errors.ml @@ -4,6 +4,7 @@ open Pp open Util open Ast +open Inductive open Type_errors let print_loc loc = @@ -48,6 +49,8 @@ let rec explain_exn_default = function | TypeError(k,ctx,te) -> Himsg.explain_type_error k ctx te + | InductiveError e -> Himsg.explain_inductive_error e + | Stdpp.Exc_located (loc,exc) -> hOV 0 [< if loc = Ast.dummy_loc then [<>] else [< 'sTR"At location "; print_loc loc; 'sTR":"; 'fNL >]; diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index c47c0abc4..97d61ef38 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -7,10 +7,12 @@ open Options open Names open Generic open Term +open Inductive open Sign open Environ open Type_errors open Reduction +open Pretty open Printer open Ast @@ -176,28 +178,28 @@ let explain_cant_find_case_type k ctx c = let pe = gentermpr k ctx c in hOV 3 [<'sTR "Cannot infer type of whole Case expression on"; 'wS 1; pe >] +(*** let explain_cant_find_case_type_loc loc k ctx c = let pe = gentermpr k ctx c in user_err_loc (loc,"pretype", hOV 3 [<'sTR "Cannot infer type of whole Case expression on"; 'wS 1; pe >]) +***) let explain_occur_check k ctx ev rhs = let id = "?" ^ string_of_int ev in let pt = gentermpr k ctx rhs in - errorlabstrm "Trad.occur_check" - [< 'sTR"Occur check failed: tried to define "; 'sTR id; - 'sTR" with term"; 'bRK(1,1); pt >] + [< 'sTR"Occur check failed: tried to define "; 'sTR id; + 'sTR" with term"; 'bRK(1,1); pt >] let explain_not_clean k ctx ev t = let c = Rel (Intset.choose (free_rels t)) in let id = "?" ^ string_of_int ev in let var = gentermpr k ctx c in - errorlabstrm "Trad.not_clean" - [< 'sTR"Tried to define "; 'sTR id; - 'sTR" with a term using variable "; var; 'sPC; - 'sTR"which is not in its scope." >] + [< 'sTR"Tried to define "; 'sTR id; + 'sTR" with a term using variable "; var; 'sPC; + 'sTR"which is not in its scope." >] let explain_type_error k ctx = function | UnboundRel n -> @@ -240,20 +242,82 @@ let explain_type_error k ctx = function explain_not_clean k ctx n c let explain_refiner_bad_type k ctx arg ty conclty = - errorlabstrm "Logic.conv_leq_goal" - [< 'sTR"refiner was given an argument"; 'bRK(1,1); - gentermpr k ctx arg; 'sPC; - 'sTR"of type"; 'bRK(1,1); gentermpr k ctx ty; 'sPC; - 'sTR"instead of"; 'bRK(1,1); gentermpr k ctx conclty >] + [< 'sTR"refiner was given an argument"; 'bRK(1,1); + gentermpr k ctx arg; 'sPC; + 'sTR"of type"; 'bRK(1,1); gentermpr k ctx ty; 'sPC; + 'sTR"instead of"; 'bRK(1,1); gentermpr k ctx conclty >] let explain_refiner_occur_meta k ctx t = - errorlabstrm "Logic.mk_refgoals" - [< 'sTR"cannot refine with term"; 'bRK(1,1); gentermpr k ctx t; - 'sPC; 'sTR"because there are metavariables, and it is"; - 'sPC; 'sTR"neither an application nor a Case" >] + [< 'sTR"cannot refine with term"; 'bRK(1,1); gentermpr k ctx t; + 'sPC; 'sTR"because there are metavariables, and it is"; + 'sPC; 'sTR"neither an application nor a Case" >] let explain_refiner_cannot_applt k ctx t harg = - errorlabstrm "Logic.mkARGGOALS" - [< 'sTR"in refiner, a term of type "; 'bRK(1,1); - gentermpr k ctx t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1); - gentermpr k ctx harg >] + [< 'sTR"in refiner, a term of type "; 'bRK(1,1); + gentermpr k ctx t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1); + gentermpr k ctx harg >] + +let explain_refiner_error e = + [< 'sTR "TODO: EXPLAIN REFINER ERROR" >] + +let error_non_strictly_positive k lna c v = + let env = assumptions_for_print lna in + let pc = gentermpr k env c in + let pv = gentermpr k env v in + [< 'sTR "Non strictly positive occurrence of "; pv; 'sTR " in"; + 'bRK(1,1); pc >] + +let error_ill_formed_inductive k lna c v = + let env = assumptions_for_print lna in + let pc = gentermpr k env c in + let pv = gentermpr k env v in + [< 'sTR "Not enough arguments applied to the "; pv; + 'sTR " in"; 'bRK(1,1); pc >] + +let error_ill_formed_constructor k lna c v = + let env = assumptions_for_print lna in + let pc = gentermpr k env c in + let pv = gentermpr k env v in + [< 'sTR "The conclusion of"; 'bRK(1,1); pc; 'bRK(1,1); + 'sTR "is not valid;"; 'bRK(1,1); 'sTR "it must be built from "; pv >] + +let str_of_nth n = + (string_of_int n)^ + (match n mod 10 with + | 1 -> "st" + | 2 -> "nd" + | 3 -> "rd" + | _ -> "th") + +let error_bad_ind_parameters k lna c n v1 v2 = + let env = assumptions_for_print lna in + let pc = gentermpr k env c in + let pv1 = gentermpr k env v1 in + let pv2 = gentermpr k env v2 in + [< 'sTR ("The "^(str_of_nth n)^" argument of "); pv2; 'bRK(1,1); + 'sTR "must be "; pv1; 'sTR " in"; 'bRK(1,1); pc >] + +let error_same_names_types id = + [< 'sTR "The name"; 'sPC; print_id id; 'sPC; + 'sTR "is used twice is the inductive types definition." >] + +let error_same_names_constructors id cid = + [< 'sTR "The constructor name"; 'sPC; print_id cid; 'sPC; + 'sTR "is used twice is the definition of type"; 'sPC; + print_id id >] + +let error_not_an_arity id = + [< 'sTR "The type of"; 'sPC; print_id id; 'sPC; 'sTR "is not an arity." >] + +let error_bad_entry () = + [< 'sTR "Bad inductive definition." >] + +let explain_inductive_error = function + | NonPos (lna,c,v) -> error_non_strictly_positive CCI lna c v + | NotEnoughArgs (lna,c,v) -> error_ill_formed_inductive CCI lna c v + | NotConstructor (lna,c,v) -> error_ill_formed_constructor CCI lna c v + | NonPar (lna,c,n,v1,v2) -> error_bad_ind_parameters CCI lna c n v1 v2 + | SameNamesTypes id -> error_same_names_types id + | SameNamesConstructors (id,cid) -> error_same_names_constructors id cid + | NotAnArity id -> error_not_an_arity id + | BadEntry -> error_bad_entry () diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index ea4c10637..d12d7963e 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -4,12 +4,13 @@ (*i*) open Pp open Names -open Term +open Inductive open Sign -open Environ open Type_errors (*i*) (* This module provides functions to explain the type errors. *) val explain_type_error : path_kind -> context -> type_error -> std_ppcmds + +val explain_inductive_error : inductive_error -> std_ppcmds diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index fbbc48a95..e53dea4de 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -27,7 +27,7 @@ let _ = let (inPPSyntax,outPPSyntax) = declare_object ("PPSYNTAX", - { load_function = (fun _ -> ()); + { load_function = (fun (_,ppobj) -> Esyntax.add_ppobject ppobj); open_function = (fun _ -> ()); cache_function = (fun (_,ppobj) -> Esyntax.add_ppobject ppobj); specification_function = (fun x -> x) }) @@ -42,8 +42,8 @@ let ppobj_of_ast whatfor sel = (whatfor, List.flatten (List.map (Extend.level_of_ast whatfor) sel)) let add_syntax_obj whatfor sel = - let _ = Lib.add_anonymous_leaf (inPPSyntax (ppobj_of_ast whatfor sel)) in - () + let ppobj = ppobj_of_ast whatfor sel in + Lib.add_anonymous_leaf (inPPSyntax ppobj) (************************ @@ -66,7 +66,7 @@ let (inToken, outToken) = cache_function = (fun (_, s) -> Pcoq.lexer.Token.using ("", s)); specification_function = (fun x -> x)}) -let add_token_obj s = let _ = Lib.add_anonymous_leaf (inToken s) in () +let add_token_obj s = Lib.add_anonymous_leaf (inToken s) (* Grammar rules *) let (inGrammar, outGrammar) = @@ -78,8 +78,7 @@ let (inGrammar, outGrammar) = specification_function = (fun x -> x)}) let add_grammar_obj univ al = - let _ = Lib.add_anonymous_leaf (inGrammar (Extend.gram_of_ast univ al)) in - () + Lib.add_anonymous_leaf (inGrammar (Extend.gram_of_ast univ al)) (* printing grammar entries *) let print_grammar univ entry = @@ -201,8 +200,7 @@ let add_infix assoc n inf pr = let gram_rule = gram_infix assoc n (split inf) pr in (* check the syntax entry *) let syntax_rule = infix_syntax_entry assoc n inf pr in - let _ = Lib.add_anonymous_leaf (inInfix(gram_rule,syntax_rule)) in - () + Lib.add_anonymous_leaf (inInfix(gram_rule,syntax_rule)) (* Distfix *) (* Distfix LEFTA 7 "/ _ / _ /" app.*) @@ -246,6 +244,5 @@ let distfix assoc n sl f = } let add_distfix a n df f = - let _ = Lib.add_anonymous_leaf (inInfix(distfix a n (split df) f, [])) in - () + Lib.add_anonymous_leaf (inInfix(distfix a n (split df) f, [])) diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 5329becae..d2a240075 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -224,7 +224,7 @@ let (inMLModule,outMLModule) = specification_function = specification_ml_module_object }) let declare_ml_modules l = - let _ = Lib.add_anonymous_leaf (inMLModule {mnames=l}) in () + Lib.add_anonymous_leaf (inMLModule {mnames=l}) let print_ml_path () = let l = !coq_mlpath_copy in diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index e78a4b92a..6d2ebf57a 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -203,10 +203,11 @@ let print_toplevel_error exc = if valid_buffer_loc top_buffer dloc loc then (print_highlight_location top_buffer loc, ie) else - (print_command_location top_buffer dloc, ie) + ([<>] (* print_command_location top_buffer dloc *), ie) | Error_in_file (s, (fname, loc), ie) -> (print_location_in_file s fname loc, ie) - | _ -> (print_command_location top_buffer dloc, exc) + | _ -> + ([<>] (* print_command_location top_buffer dloc *), exc) in match exc with | End_of_input -> diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index a01e701bc..17127518c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -254,12 +254,12 @@ let _ = (fun () -> reset_section (string_of_id id)) | _ -> bad_vernac_args "ResetSection") +***) let _ = add "ResetName" (function - | [VARG_IDENTIFIER id] -> (fun () -> reset_name id) + | [VARG_IDENTIFIER id] -> (fun () -> Pfedit.reset_name id) | _ -> bad_vernac_args "ResetName") -***) (* Modules *) -- cgit v1.2.3