diff options
105 files changed, 1028 insertions, 771 deletions
@@ -1,3 +1,51 @@ +Changes from V8.5beta2 to ... +=================================== + +Vernacular commands + +- New command "Redirect" to redirect the output of a command to a file. + + +Changes from V8.5beta1 to V8.5beta2 +=================================== + +Logic + +- The VM now supports inductive types with up to 8388851 non-constant + constructors and up to 8388607 constant ones. + +Tactics + +- A script using the admit tactic can no longer be concluded by either + Qed or Defined. In the first case, Admitted can be used instead. In + the second case, a subproof should be used. + +- The easy tactic and the now tactical now have a more predictable + behavior, but they might now discharge some previously unsolved goals. + +Extraction + +- Definitions extracted to Haskell GHC should no longer randomly + segfault when some Coq types cannot be represented by Haskell types. + +- Definitions can now be extracted to Json for post-processing. + +Tools + +- Option -I -as has been removed, and option -R -as has been + deprecated. In both cases, option -R can be used instead. + +- coq_makefile now generates double-colon rules for rules such as clean. + +API + +- The interface of [change] has changed to take a [change_arg], which + can be built from a [constr] using [make_change_arg]. + +- [pattern_of_constr] now returns a triplet including the cleaned-up + [evar_map], removing the evars that were turned into metas. + + Changes from V8.4 to V8.5beta1 ============================== diff --git a/checker/checker.ml b/checker/checker.ml index 9a1007acb..0f7ed8df5 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -67,13 +67,13 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = Check.add_load_path (dir,coq_dirpath) end else - msg_warning (str ("Cannot open " ^ dir)) + msg_warning (str "Cannot open " ++ str dir) let convert_string d = try Id.of_string d with Errors.UserError _ -> if_verbose msg_warning - (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); + (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); raise Exit let add_rec_path ~unix_path ~coq_root = @@ -90,7 +90,7 @@ let add_rec_path ~unix_path ~coq_root = List.iter Check.add_load_path dirs; Check.add_load_path (unix_path, coq_root) else - msg_warning (str ("Cannot open " ^ unix_path)) + msg_warning (str "Cannot open " ++ str unix_path) (* By the option -include -I or -R of the command line *) let includes = ref [] @@ -221,7 +221,7 @@ let print_loc loc = else let loc = Loc.unloc loc in (int (fst loc) ++ str"-" ++ int (snd loc)) -let guill s = "\""^s^"\"" +let guill s = str "\"" ++ str s ++ str "\"" let where s = if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) @@ -232,7 +232,7 @@ let rec explain_exn = function | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt) | Sys_error msg -> - hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report() ) + hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ guill msg ++ report() ) | UserError(s,pps) -> hov 1 (str "User error: " ++ where s ++ pps) | Out_of_memory -> @@ -241,14 +241,14 @@ let rec explain_exn = function hov 0 (str "Stack overflow") | Match_failure(filename,pos1,pos2) -> hov 1 (anomaly_string () ++ str "Match failure in file " ++ - str (guill filename) ++ str " at line " ++ int pos1 ++ + guill filename ++ str " at line " ++ int pos1 ++ str " character " ++ int pos2 ++ report ()) | Not_found -> hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report ()) | Failure s -> hov 0 (str "Failure: " ++ str s ++ report ()) | Invalid_argument s -> - hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report ()) + hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ guill s ++ report ()) | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.") | Univ.UniverseInconsistency (o,u,v) -> @@ -294,7 +294,7 @@ let rec explain_exn = function Format.printf "@\n====== universes ====@\n"; Pp.pp (Univ.pr_universes (ctx.Environ.env_stratification.Environ.env_universes)); - str("\nCantApplyBadType at argument " ^ string_of_int n) + str "\nCantApplyBadType at argument " ++ int n | CantApplyNonFunctional _ -> str"CantApplyNonFunctional" | IllFormedRecBody _ -> str"IllFormedRecBody" | IllTypedRecBody _ -> str"IllTypedRecBody" @@ -309,7 +309,7 @@ let rec explain_exn = function hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++ (if s = "" then mt () else - (str ("(file \"" ^ s ^ "\", line ") ++ int b ++ + (str "(file \"" ++ str s ++ str "\", line " ++ int b ++ str ", characters " ++ int e ++ str "-" ++ int (e+6) ++ str ")")) ++ report ()) @@ -323,7 +323,7 @@ let parse_args argv = | "-coqlib" :: s :: rem -> if not (exists_dir s) then - fatal_error (str ("Directory '"^s^"' does not exist")) false; + fatal_error (str "Directory '" ++ str s ++ str "' does not exist") false; Flags.coqlib := s; Flags.coqlib_spec := true; parse rem diff --git a/configure.ml b/configure.ml index 3cf462ebe..267d556a2 100644 --- a/configure.ml +++ b/configure.ml @@ -27,7 +27,7 @@ let die msg = eprintf "%s\nConfiguration script failed!\n" msg; exit 1 let s2i = int_of_string let i2s = string_of_int -let (/) = Filename.concat +let (/) x y = x ^ "/" ^ y (** Remove the final '\r' that may exists on Win32 *) @@ -396,8 +396,7 @@ let coq_annotate_flag = then if program_in_path "ocamlmerlin" then "-bin-annot" else "-dtypes" else "" -let cflags = "-Wall -Wno-unused" - +let cflags = "-Wall -Wno-unused -g " ^ (if !Prefs.debug then "-O1" else "-O2") (** * Architecture *) diff --git a/dev/base_include b/dev/base_include index e086c64cd..197528acd 100644 --- a/dev/base_include +++ b/dev/base_include @@ -87,6 +87,7 @@ open Cbv open Classops open Clenv open Clenvtac +open Constr_matching open Glob_term open Glob_ops open Coercion diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 4952ed778..739a89af4 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -680,7 +680,8 @@ should use the command \texttt{Locate File} (see Section~\ref{Locate File}) Loadpaths are preferably managed using {\Coq} command line options (see Section~\ref{loadpath}) but there remain vernacular commands to -manage them. +manage them for practical purposes. Such commands are only meant to be issued in +the toplevel, and using them in source files is discouraged. \subsection[\tt Pwd.]{\tt Pwd.\comindex{Pwd}\label{Pwd}} This command displays the current working directory. @@ -876,6 +877,9 @@ go();; This command executes the vernacular command \textrm{\textsl{command}} and display the time needed to execute it. +\subsection[\tt Redirect "\textrm{\textsl{file}}" \textrm{\textsl{command}}.]{\tt Redirect "\textrm{\textsl{file}}" \textrm{\textsl{command}}.\comindex{Redirect} +\label{redirect}} +This command executes the vernacular command \textrm{\textsl{command}}, redirecting its output to ``\textrm{\textsl{file}}.out''. \subsection[\tt Timeout \textrm{\textsl{int}} \textrm{\textsl{command}}.]{\tt Timeout \textrm{\textsl{int}} \textrm{\textsl{command}}.\comindex{Timeout} \label{timeout}} diff --git a/engine/evd.ml b/engine/evd.ml index bf519fb7c..f414d71dc 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1304,9 +1304,6 @@ let e_eq_constr_univs evdref t u = let evd, b = eq_constr_univs !evdref t u in evdref := evd; b -let eq_constr_univs_test evd t u = - snd (eq_constr_univs evd t u) - (**********************************************************) (* Accessing metas *) diff --git a/engine/evd.mli b/engine/evd.mli index fe785a831..eca6d60ad 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -562,10 +562,6 @@ val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool val e_eq_constr_univs : evar_map ref -> constr -> constr -> bool (** Syntactic equality up to universes. *) -val eq_constr_univs_test : evar_map -> constr -> constr -> bool -(** Syntactic equality up to universes, throwing away the (consistent) constraints - in case of success. *) - (********************************************************************) (* constr with holes and pending resolution of classes, conversion *) (* problems, candidates, etc. *) diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml index d509670ec..cb3e5a186 100644 --- a/engine/logic_monad.ml +++ b/engine/logic_monad.ml @@ -208,118 +208,110 @@ struct type rich_exn = Exninfo.iexn type 'a iolist = - { iolist : 'r. (rich_exn -> 'r NonLogical.t) -> - ('a -> (rich_exn -> 'r NonLogical.t) -> 'r NonLogical.t) -> - 'r NonLogical.t } + { iolist : 'r. state -> (rich_exn -> 'r NonLogical.t) -> + ('a -> state -> (rich_exn -> 'r NonLogical.t) -> 'r NonLogical.t) -> + 'r NonLogical.t } include Monad.Make(struct - type 'a t = state -> ('a * state) iolist - let return x : 'a t = (); fun s -> - { iolist = fun nil cons -> cons (x, s) nil } + type 'a t = 'a iolist - let (>>=) (m : 'a t) (f : 'a -> 'b t) : 'b t = (); fun s -> - let m = m s in - { iolist = fun nil cons -> - m.iolist nil (fun (x, s) next -> (f x s).iolist next cons) } + let return x = + { iolist = fun s nil cons -> cons x s nil } - let (>>) (m : unit t) (f : 'a t) : 'a t = (); fun s -> - let m = m s in - { iolist = fun nil cons -> - m.iolist nil (fun ((), s) next -> (f s).iolist next cons) } + let (>>=) m f = + { iolist = fun s nil cons -> + m.iolist s nil (fun x s next -> (f x).iolist s next cons) } - let map (f : 'a -> 'b) (m : 'a t) : 'b t = (); fun s -> - let m = m s in - { iolist = fun nil cons -> m.iolist nil (fun (x, s) next -> cons (f x, s) next) } + let (>>) m f = + { iolist = fun s nil cons -> + m.iolist s nil (fun () s next -> f.iolist s next cons) } + + let map f m = + { iolist = fun s nil cons -> m.iolist s nil (fun x s next -> cons (f x) s next) } end) - let zero e : 'a t = (); fun s -> - { iolist = fun nil cons -> nil e } + let zero e = + { iolist = fun _ nil cons -> nil e } - let plus m1 m2 : 'a t = (); fun s -> - let m1 = m1 s in - { iolist = fun nil cons -> m1.iolist (fun e -> (m2 e s).iolist nil cons) cons } + let plus m1 m2 = + { iolist = fun s nil cons -> m1.iolist s (fun e -> (m2 e).iolist s nil cons) cons } - let ignore (m : 'a t) : unit t = (); fun s -> - let m = m s in - { iolist = fun nil cons -> m.iolist nil (fun (_, s) next -> cons ((), s) next) } + let ignore m = + { iolist = fun s nil cons -> m.iolist s nil (fun _ s next -> cons () s next) } - let lift (m : 'a NonLogical.t) : 'a t = (); fun s -> - { iolist = fun nil cons -> NonLogical.(m >>= fun x -> cons (x, s) nil) } + let lift m = + { iolist = fun s nil cons -> NonLogical.(m >>= fun x -> cons x s nil) } (** State related *) - let get : P.s t = (); fun s -> - { iolist = fun nil cons -> cons (s.sstate, s) nil } + let get = + { iolist = fun s nil cons -> cons s.sstate s nil } - let set (sstate : P.s) : unit t = (); fun s -> - { iolist = fun nil cons -> cons ((), { s with sstate }) nil } + let set (sstate : P.s) = + { iolist = fun s nil cons -> cons () { s with sstate } nil } - let modify (f : P.s -> P.s) : unit t = (); fun s -> - { iolist = fun nil cons -> cons ((), { s with sstate = f s.sstate }) nil } + let modify (f : P.s -> P.s) = + { iolist = fun s nil cons -> cons () { s with sstate = f s.sstate } nil } - let current : P.e t = (); fun s -> - { iolist = fun nil cons -> cons (s.rstate, s) nil } + let current = + { iolist = fun s nil cons -> cons s.rstate s nil } - let local (type a) (e:P.e) (m:a t) : a t = (); fun s -> - let m = m { s with rstate = e } in - { iolist = fun nil cons -> - m.iolist nil (fun (x,s') next -> cons (x,{s' with rstate=s.rstate}) next) } + let local e m = + { iolist = fun s nil cons -> + m.iolist { s with rstate = e } nil + (fun x s' next -> cons x {s' with rstate = s.rstate} next) } - let put (w : P.w) : unit t = (); fun s -> - { iolist = fun nil cons -> cons ((), { s with wstate = P.wprod s.wstate w }) nil } + let put w = + { iolist = fun s nil cons -> cons () { s with wstate = P.wprod s.wstate w } nil } - let update (f : P.u -> P.u) : unit t = (); fun s -> - { iolist = fun nil cons -> cons ((), { s with ustate = f s.ustate }) nil } + let update (f : P.u -> P.u) = + { iolist = fun s nil cons -> cons () { s with ustate = f s.ustate } nil } (** List observation *) - let once (m : 'a t) : 'a t = (); fun s -> - let m = m s in - { iolist = fun nil cons -> m.iolist nil (fun x _ -> cons x nil) } + let once m = + { iolist = fun s nil cons -> m.iolist s nil (fun x s _ -> cons x s nil) } - let break (f : rich_exn -> rich_exn option) (m : 'a t) : 'a t = (); fun s -> - let m = m s in - { iolist = fun nil cons -> - m.iolist nil (fun x next -> cons x (fun e -> match f e with None -> next e | Some e -> nil e)) + let break f m = + { iolist = fun s nil cons -> + m.iolist s nil (fun x s next -> cons x s (fun e -> match f e with None -> next e | Some e -> nil e)) } (** For [reflect] and [split] see the "Backtracking, Interleaving, and Terminating Monad Transformers" paper. *) type 'a reified = ('a, rich_exn -> 'a reified) list_view NonLogical.t - let rec reflect (m : 'a reified) : 'a iolist = - { iolist = fun nil cons -> + let rec reflect (m : ('a * state) reified) : 'a iolist = + { iolist = fun s0 nil cons -> let next = function | Nil e -> nil e - | Cons (x, l) -> cons x (fun e -> (reflect (l e)).iolist nil cons) + | Cons ((x, s), l) -> cons x s (fun e -> (reflect (l e)).iolist s0 nil cons) in NonLogical.(m >>= next) } - let split (m : 'a t) : ('a, rich_exn -> 'a t) list_view t = (); fun s -> - let m = m s in + let split m : ('a, rich_exn -> 'a t) list_view t = let rnil e = NonLogical.return (Nil e) in - let rcons p l = NonLogical.return (Cons (p, l)) in - { iolist = fun nil cons -> + let rcons p s l = NonLogical.return (Cons ((p, s), l)) in + { iolist = fun s nil cons -> let open NonLogical in - m.iolist rnil rcons >>= begin function - | Nil e -> cons (Nil e, s) nil + m.iolist s rnil rcons >>= begin function + | Nil e -> cons (Nil e) s nil | Cons ((x, s), l) -> - let l e = (); fun _ -> reflect (l e) in - cons (Cons (x, l), s) nil + let l e = reflect (l e) in + cons (Cons (x, l)) s nil end } let run m r s = let s = { wstate = P.wunit; ustate = P.uunit; rstate = r; sstate = s } in - let m = m s in let rnil e = NonLogical.return (Nil e) in - let rcons (x, s) l = + let rcons x s l = let p = (x, s.sstate, s.wstate, s.ustate) in NonLogical.return (Cons (p, l)) in - m.iolist rnil rcons + m.iolist s rnil rcons let repr x = x diff --git a/ide/coq.lang b/ide/coq.lang index 65150d6a9..35dff85e6 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -5,7 +5,7 @@ <property name="block-comment-start">\(\*</property> <property name="block-comment-stop">\*\)</property> </metadata> - + <styles> <style id="comment" _name="Comment" map-to="def:comment"/> <style id="coqdoc" _name="Coqdoc text" map-to="def:note"/> @@ -20,15 +20,15 @@ <style id="safe" _name="Checked Part"/> <style id="sentence" _name="Sentence terminator"/> </styles> - + <definitions> <define-regex id="space">\s+</define-regex> <define-regex id="first_ident_char">[_\p{L}]</define-regex> <define-regex id="ident_char">[_\p{L}'\pN]</define-regex> <define-regex id="ident">\%{first_ident_char}\%{ident_char}*</define-regex> <define-regex id="qualit">(\%{ident}\.)*\%{ident}</define-regex> - <define-regex id="undotted_sep">[-+*{}]</define-regex> <define-regex id="dot_sep">\.(\s|\z)</define-regex> + <define-regex id="bullet">([-+*]+|{)(\s|\z)|}(\s*})*</define-regex> <define-regex id="single_decl">Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion</define-regex> <define-regex id="mult_decl">Hypothes[ie]s|Axiom(s)?|Variable(s)?|Parameter(s)?|Context|Implicit\%{space}Type(s)?</define-regex> <define-regex id="locality">((Local|Global)\%{space})?</define-regex> @@ -36,185 +36,197 @@ <define-regex id="end_proof">Qed|Defined|Admitted|Abort|Save</define-regex> <define-regex id="decl_head">((?'gal'\%{locality}(Program\%{space})?(\%{single_decl}|\%{begin_proof}))\%{space}(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}\%{ident})*))|(?'gal2'Goal)</define-regex> - <context id="escape-seq" style-ref="escape"> - <match>""</match> - </context> - <context id="string" style-ref="string"> + <!-- Strings, with '""' an escape sequence --> + <context id="string" style-ref="string" class="string"> <start>"</start> <end>"</end> <include> - <context ref="escape-seq"/> + <context id="string-escape" style-ref="escape"> + <match>""</match> + </context> + </include> + </context> + + <!-- Coqdoc comments --> + <context id="coqdoc" style-ref="coqdoc" class="comment" class-disabled="no-spell-check"> + <start>\(\*\*(\s|\z)</start> + <end>\*\)</end> + <include> + <context ref="comment"/> + <context ref="string"/> + <context ref="def:in-comment"/> </include> </context> + + <!-- Regular comments, possibly nested --> + <context id="comment" style-ref="comment" class="comment" class-disabled="no-spell-check"> + <start>\(\*</start> + <end>\*\)</end> + <include> + <context ref="comment"/> + <context ref="string"/> + <context ref="def:in-comment"/> + </include> + </context> + + <!-- Keywords for constr --> + <context id="constr-keyword" style-ref="constr-keyword"> + <keyword>forall</keyword> + <keyword>fun</keyword> + <keyword>match</keyword> + <keyword>fix</keyword> + <keyword>cofix</keyword> + <keyword>with</keyword> + <keyword>for</keyword> + <keyword>end</keyword> + <keyword>as</keyword> + <keyword>let</keyword> + <keyword>in</keyword> + <keyword>if</keyword> + <keyword>then</keyword> + <keyword>else</keyword> + <keyword>return</keyword> + </context> + + <!-- Sort keywords --> + <context id="constr-sort" style-ref="constr-sort"> + <keyword>Prop</keyword> + <keyword>Set</keyword> + <keyword>Type</keyword> + </context> + <context id="coq" class="no-spell-check"> <include> <context ref="string"/> - <context id="coqdoc" style-ref="coqdoc" class-disabled="no-spell-check"> - <start>\(\*\*(\s|\z)</start> - <end>\*\)</end> - <include> - <context ref="comment-in-comment"/> - <context ref="string"/> - </include> - </context> - <context id="comment" style-ref="comment" class="comment" class-disabled="no-spell-check"> - <start>\(\*</start> - <end>\*\)</end> - <include> - <context id="comment-in-comment" style-ref="comment" class="comment" class-disabled="no-spell-check"> - <start>\(\*</start> - <end>\*\)</end> - <include> - <context ref="comment-in-comment"/> - <context ref="string"/> - </include> - </context> - <context ref="string"/> - </include> - </context> - <context id="declaration"> - <start>\%{decl_head}</start> - <end>\%{dot_sep}</end> - <include> - <context sub-pattern="id" where="start" style-ref="identifier"/> - <context sub-pattern="gal" where="start" style-ref="gallina-keyword"/> - <context sub-pattern="gal2" where="start" style-ref="gallina-keyword"/> - <context sub-pattern="id_list" where="start" style-ref="identifier"/> - <context sub-pattern="gal4list" where="start" style-ref="gallina-keyword"/> - <context id="constr-keyword" style-ref="constr-keyword"> - <keyword>forall</keyword> - <keyword>fun</keyword> - <keyword>match</keyword> - <keyword>fix</keyword> - <keyword>cofix</keyword> - <keyword>with</keyword> - <keyword>for</keyword> - <keyword>end</keyword> - <keyword>as</keyword> - <keyword>let</keyword> - <keyword>in</keyword> - <keyword>if</keyword> - <keyword>then</keyword> - <keyword>else</keyword> - <keyword>return</keyword> - </context> - <context id="constr-sort" style-ref="constr-sort"> - <keyword>Prop</keyword> - <keyword>Set</keyword> - <keyword>Type</keyword> - </context> - <context id="dot-nosep"> - <match>\.\.</match> - </context> - <context ref="comment"/> - <context ref="string"/> - <context ref="coqdoc"/> - </include> - </context> - <context id="proof"> - <start>Proof(\%{dot_sep}|\%{space}using|\%{space}with)</start> - <end>\%{end_proof}\%{dot_sep}</end> - <include> - <context sub-pattern="0" where="start" style-ref="vernac-keyword"/> - <context sub-pattern="0" where="end" style-ref="vernac-keyword"/> - <context ref="command"/> - <context ref="scope-command"/> - <context ref="hint-command"/> - <context ref="command-for-qualit"/> - <context ref="declaration"/> - <context ref="comment"/> - <context ref="string"/> - <context ref="coqdoc"/> - <context ref="proof"/> - <context ref="undotted-sep"/> - <context id="tactic" extend-parent="false"> - <start>\b[^-+*{}]</start> - <end>\%{dot_sep}</end> - <include> - <context ref="dot-nosep"/> - <context ref="constr-keyword"/> - <context ref="constr-sort"/> - </include> - </context> - </include> - </context> - <context id="exact-proof"> - <start>Proof</start> - <end>\%{dot_sep}</end> - <include> - <context sub-pattern="0" where="start" style-ref="vernac-keyword"/> - <context ref="constr-keyword"/> - <context ref="constr-sort"/> - </include> - </context> - <context id="undotted-sep" style-ref="vernac-keyword"> - <match>\%{undotted_sep}</match> - </context> - <context id="command" style-ref="vernac-keyword"> - <keyword>Add</keyword> - <keyword>Check</keyword> - <keyword>Eval</keyword> - <keyword>Load</keyword> - <keyword>Undo</keyword> - <keyword>(Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist)</keyword> - <keyword>Print</keyword> - <keyword>Comments</keyword> - <keyword>Solve\%{space}Obligation</keyword> - <keyword>(Uns|S)et(\%{space}\%{ident})+</keyword> - <keyword>(\%{locality}|(Reserved|Tactic)\%{space})?Notation</keyword> - <keyword>\%{locality}Infix</keyword> - <keyword>Declare\%{space}ML\%{space}Module</keyword> - <keyword>Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme|JSON)</keyword> - </context> - <context id="hint-command" style-ref="vernac-keyword"> - <prefix>\%{locality}Hint\%{space}</prefix> - <keyword>Resolve</keyword> - <keyword>Immediate</keyword> - <keyword>Constructors</keyword> - <keyword>Unfold</keyword> - <keyword>Opaque</keyword> - <keyword>Transparent</keyword> - <keyword>Extern</keyword> - <keyword>Rewrite</keyword> - </context> - <context id="scope-command" style-ref="vernac-keyword"> - <suffix>\%{space}Scope</suffix> - <keyword>\%{locality}Open</keyword> - <keyword>\%{locality}Close</keyword> - <keyword>Bind</keyword> - <keyword>Delimit</keyword> - </context> - <context id="command-for-qualit"> - <suffix>\%{space}(?'qua'\%{qualit})</suffix> - <keyword>Chapter</keyword> - <keyword>Combined\%{space}Scheme</keyword> - <keyword>Scheme\%{space}(Induction|Minimality|Elimination|Case|Equality)\%{space}for</keyword> - <keyword>End</keyword> - <keyword>Section</keyword> - <keyword>Module(\%{space}Type)?</keyword> - <keyword>Declare\%{space}Module(\%{space}(Import|Export))?</keyword> - <keyword>About</keyword> - <keyword>Arguments</keyword> - <keyword>Implicit\%{space}Arguments</keyword> - <keyword>Include</keyword> - <keyword>Extract\%{space}((Inlined\%{space})?Constant|Inductive)</keyword> - <include> - <context sub-pattern="1" style-ref="vernac-keyword"/> - <context sub-pattern="qua" style-ref="identifier"/> - </include> - </context> - <context id="command-for-qualit-list"> - <suffix>(?'qua_list'(\%{space}\%{qualit})+)</suffix> - <keyword>Typeclasses (Transparent|Opaque)</keyword> - <keyword>Require(\%{space}(Import|Export))?</keyword> - <keyword>Import</keyword> - <keyword>Export</keyword> - <keyword>((Recursive|Separate)\%{space})?Extraction(\%{space}(Library|(No)?Inline|Blacklist))?</keyword> - <include> - <context sub-pattern="1" style-ref="vernac-keyword"/> - <context sub-pattern="qua_list" style-ref="identifier"/> - </include> - </context> + <context ref="coqdoc"/> + <context ref="comment"/> + + <context id="declaration"> + <start>\%{decl_head}</start> + <end>\%{dot_sep}</end> + <include> + <context sub-pattern="id" where="start" style-ref="identifier"/> + <context sub-pattern="gal" where="start" style-ref="gallina-keyword"/> + <context sub-pattern="gal2" where="start" style-ref="gallina-keyword"/> + <context sub-pattern="id_list" where="start" style-ref="identifier"/> + <context sub-pattern="gal4list" where="start" style-ref="gallina-keyword"/> + <context ref="constr-keyword"/> + <context ref="constr-sort"/> + <context id="dot-nosep"> + <match>\.\.</match> + </context> + <context ref="string"/> + <context ref="coqdoc"/> + <context ref="comment"/> + </include> + </context> + + <context id="proof"> + <start>Proof(\%{dot_sep}|\%{space}using|\%{space}with)</start> + <end>\%{end_proof}\%{dot_sep}</end> + <include> + <context sub-pattern="0" where="start" style-ref="vernac-keyword"/> + <context sub-pattern="0" where="end" style-ref="vernac-keyword"/> + <context ref="command-in-proof"/> + <context ref="string"/> + <context ref="coqdoc"/> + <context ref="comment"/> + <context ref="constr-keyword"/> + <context ref="constr-sort"/> + <context id="bullet" extend-parent="false"> + <match>\%{dot_sep}\s*(?'bul'\%{bullet})</match> + <include> + <context sub-pattern="bul" style-ref="vernac-keyword"/> + </include> + </context> + <context id="bullet-sol" style-ref="vernac-keyword"> + <match>^\s*\%{bullet}</match> + </context> + </include> + </context> + + <context id="exact-proof"> + <start>Proof</start> + <end>\%{dot_sep}</end> + <include> + <context sub-pattern="0" where="start" style-ref="vernac-keyword"/> + <context ref="constr-keyword"/> + <context ref="constr-sort"/> + </include> + </context> + + <context id="command-in-proof" style-ref="vernac-keyword"> + <keyword>About</keyword> + <keyword>Check</keyword> + <keyword>Print</keyword> + <keyword>Eval</keyword> + <keyword>Undo</keyword> + <keyword>Opaque</keyword> + <keyword>Transparent</keyword> + </context> + + <context id="command" style-ref="vernac-keyword"> + <keyword>Add</keyword> + <keyword>Load</keyword> + <keyword>(Print|Reset)\%{space}+Extraction\%{space}+(Inline|Blacklist)</keyword> + <keyword>Comments</keyword> + <keyword>Solve\%{space}Obligation</keyword> + <keyword>(Uns|S)et(\%{space}\%{ident})+</keyword> + <keyword>(\%{locality}|(Reserved|Tactic)\%{space})?Notation</keyword> + <keyword>\%{locality}Infix</keyword> + <keyword>Declare\%{space}ML\%{space}Module</keyword> + <keyword>Extraction\%{space}Language\%{space}(Ocaml|Haskell|Scheme|JSON)</keyword> + </context> + + <context id="hint-command" style-ref="vernac-keyword"> + <prefix>\%{locality}Hint\%{space}</prefix> + <keyword>Resolve</keyword> + <keyword>Immediate</keyword> + <keyword>Constructors</keyword> + <keyword>Unfold</keyword> + <keyword>Extern</keyword> + <keyword>Rewrite</keyword> + </context> + + <context id="scope-command" style-ref="vernac-keyword"> + <suffix>\%{space}Scope</suffix> + <keyword>\%{locality}Open</keyword> + <keyword>\%{locality}Close</keyword> + <keyword>Bind</keyword> + <keyword>Delimit</keyword> + </context> + + <context id="command-for-qualit"> + <suffix>\%{space}(?'qua'\%{qualit})</suffix> + <keyword>Chapter</keyword> + <keyword>Combined\%{space}Scheme</keyword> + <keyword>Scheme\%{space}(Induction|Minimality|Elimination|Case|Equality)\%{space}for</keyword> + <keyword>End</keyword> + <keyword>Section</keyword> + <keyword>Module(\%{space}Type)?</keyword> + <keyword>Declare\%{space}Module(\%{space}(Import|Export))?</keyword> + <keyword>Arguments</keyword> + <keyword>Implicit\%{space}Arguments</keyword> + <keyword>Include</keyword> + <keyword>Extract\%{space}((Inlined\%{space})?Constant|Inductive)</keyword> + <include> + <context sub-pattern="1" style-ref="vernac-keyword"/> + <context sub-pattern="qua" style-ref="identifier"/> + </include> + </context> + + <context id="command-for-qualit-list"> + <suffix>(?'qua_list'(\%{space}\%{qualit})+)</suffix> + <keyword>Typeclasses (Transparent|Opaque)</keyword> + <keyword>Require(\%{space}(Import|Export))?</keyword> + <keyword>Import</keyword> + <keyword>Export</keyword> + <keyword>((Recursive|Separate)\%{space})?Extraction(\%{space}(Library|(No)?Inline|Blacklist))?</keyword> + <include> + <context sub-pattern="1" style-ref="vernac-keyword"/> + <context sub-pattern="qua_list" style-ref="identifier"/> + </include> + </context> </include> </context> </definitions> diff --git a/ide/coqide.ml b/ide/coqide.ml index 0f4cb7b07..c0e228125 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -253,14 +253,14 @@ let newfile _ = !refresh_editor_hook (); notebook#goto_page index -let load sn = - let filename = sn.fileops#filename in +let load _ = + let filename = + try notebook#current_term.fileops#filename + with Invalid_argument _ -> None in match select_file_for_open ~title:"Load file" ?filename () with | None -> () | Some f -> FileAux.load_file f -let load = cb_on_current_term load - let save _ = on_current_term (FileAux.check_save ~saveas:false) let saveas sn = diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 5151d2a10..982d9bfe3 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1893,7 +1893,7 @@ let intern_context global_level env impl_env binders = with InternalizationError (loc,e) -> user_err_loc (loc,"internalize", explain_internalization_error e) -let interp_rawcontext_evars env evdref bl = +let interp_rawcontext_evars env evdref k bl = let (env, par, _, impls) = List.fold_left (fun (env,params,n,impls) (na, k, b, t) -> @@ -1913,12 +1913,12 @@ let interp_rawcontext_evars env evdref bl = | Some b -> let c = understand_judgment_tcc env evdref b in let d = (na, Some c.uj_val, c.uj_type) in - (push_rel d env, d::params, succ n, impls)) - (env,[],1,[]) (List.rev bl) + (push_rel d env, d::params, n, impls)) + (env,[],k+1,[]) (List.rev bl) in (env, par), impls -let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) env evdref params = +let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env evdref params = let int_env,bl = intern_context global_level env impl_env params in - let x = interp_rawcontext_evars env evdref bl in + let x = interp_rawcontext_evars env evdref shift bl in int_env, x diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 0d33d4334..4d2c99467 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -157,7 +157,7 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types (** Interpret contexts: returns extended env and context *) val interp_context_evars : - ?global_level:bool -> ?impl_env:internalization_env -> + ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> env -> evar_map ref -> local_binder list -> internalization_env * ((env * rel_context) * Impargs.manual_implicits) diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 02504c920..5ac718e3b 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -54,15 +54,15 @@ let gen_reference_in_modules locstr dirs s = match these with | [x] -> x | [] -> - anomaly ~label:locstr (str ("cannot find "^s^ - " in module"^(if List.length dirs > 1 then "s " else " ")) ++ + anomaly ~label:locstr (str "cannot find " ++ str s ++ + str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ prlist_with_sep pr_comma pr_dirpath dirs) | l -> anomaly ~label:locstr - (str ("ambiguous name "^s^" can represent ") ++ + (str "ambiguous name " ++ str s ++ str " can represent " ++ prlist_with_sep pr_comma (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++ - str (" in module"^(if List.length dirs > 1 then "s " else " ")) ++ + str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ prlist_with_sep pr_comma pr_dirpath dirs) let gen_constant_in_modules locstr dirs s = @@ -86,7 +86,8 @@ let check_required_library d = (Loc.ghost,make_qualid (DirPath.make (List.rev prefix)) m) *) (* or failing ...*) - error ("Library "^(DirPath.to_string dir)^" has to be required first.") + errorlabstrm "Coqlib.check_required_library" + (str "Library " ++ str (DirPath.to_string dir) ++ str " has to be required first.") (************************************************************************) (* Specific Coq objects *) diff --git a/interp/notation.ml b/interp/notation.ml index 80db2cb39..555dfa804 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -91,7 +91,9 @@ let declare_scope scope = (* Flags.if_warn message ("Creating scope "^scope);*) scope_map := String.Map.add scope empty_scope !scope_map -let error_unknown_scope sc = error ("Scope "^sc^" is not declared.") +let error_unknown_scope sc = + errorlabstrm "Notation" + (str "Scope " ++ str sc ++ str " is not declared.") let find_scope scope = try String.Map.find scope !scope_map @@ -186,14 +188,14 @@ let declare_delimiters scope key = | Some oldkey when String.equal oldkey key -> () | Some oldkey -> msg_warning - (strbrk ("Overwriting previous delimiting key "^oldkey^" in scope "^scope)); + (str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope); scope_map := String.Map.add scope newsc !scope_map end; try let oldscope = String.Map.find key !delimiters_map in if String.equal oldscope scope then () else begin - msg_warning (strbrk ("Hiding binding of key "^key^" to "^oldscope)); + msg_warning (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope); delimiters_map := String.Map.add key scope !delimiters_map end with Not_found -> delimiters_map := String.Map.add key scope !delimiters_map @@ -202,7 +204,7 @@ let find_delimiters_scope loc key = try String.Map.find key !delimiters_map with Not_found -> user_err_loc - (loc, "find_delimiters", str ("Unknown scope delimiting key "^key^".")) + (loc, "find_delimiters", str "Unknown scope delimiting key " ++ str key ++ str ".") (* Uninterpretation tables *) @@ -317,8 +319,7 @@ let check_required_module loc sc (sp,d) = try let _ = Nametab.global_of_path sp in () with Not_found -> user_err_loc (loc,"prim_token_interpreter", - str ("Cannot interpret in "^sc^" without requiring first module " - ^(List.last d)^".")) + str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".") (* Look if some notation or numeral printer in [scope] can be used in the scope stack [scopes], and if yes, using delimiters or not *) @@ -373,10 +374,9 @@ let declare_notation_interpretation ntn scopt pat df = let () = if String.Map.mem ntn sc.notations then let which_scope = match scopt with - | None -> "" - | Some _ -> " in scope " ^ scope in - let message = "Notation " ^ ntn ^ " was already used" ^ which_scope in - msg_warning (strbrk message) + | None -> mt () + | Some _ -> str " in scope " ++ str scope in + msg_warning (str "Notation " ++ str ntn ++ str " was already used" ++ which_scope) in let sc = { sc with notations = String.Map.add ntn (pat,df) sc.notations } in let () = scope_map := String.Map.add scope sc !scope_map in @@ -452,7 +452,7 @@ let interp_notation loc ntn local_scopes = try find_interpretation ntn (find_notation ntn) scopes with Not_found -> user_err_loc - (loc,"",str ("Unknown interpretation for notation \""^ntn^"\".")) + (loc,"",str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".") let uninterp_notations c = List.map_append (fun key -> keymap_find key !notations_key_table) @@ -784,8 +784,8 @@ let pr_scope_classes sc = match l with | [] -> mt () | _ :: l -> - let opt_s = match l with [] -> "" | _ -> "es" in - hov 0 (str ("Bound to class" ^ opt_s) ++ + let opt_s = match l with [] -> mt () | _ -> str "es" in + hov 0 (str "Bound to class" ++ opt_s ++ spc() ++ prlist_with_sep spc pr_scope_class l) ++ fnl() let pr_notation_info prglob ntn c = diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 9be7abcfe..d2709d5e3 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -99,7 +99,7 @@ let verbose_compat kn def = function | [], NRef r -> str " is " ++ pr_global_env Id.Set.empty r | _ -> str " is a compatibility notation" in - let since = str (" since Coq > " ^ Flags.pr_version v ^ ".") in + let since = str " since Coq > " ++ str (Flags.pr_version v) ++ str "." in act (pr_syndef kn ++ pp_def ++ since) | _ -> () diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 450b1af0f..d7b269a1d 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -273,6 +273,7 @@ type vernac_expr = (* Control *) | VernacLoad of verbose_flag * string | VernacTime of vernac_list + | VernacRedirect of string * vernac_list | VernacTimeout of int * vernac_expr | VernacFail of vernac_expr | VernacError of exn (* always fails *) diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 0ab9f89ff..ddbde9d38 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -77,9 +77,11 @@ sp is a local copy of the global variable extern_sp. */ #ifdef _COQ_DEBUG_ # define print_instr(s) /*if (drawinstr)*/ printf("%s\n",s) # define print_int(i) /*if (drawinstr)*/ printf("%d\n",i) +# define print_lint(i) /*if (drawinstr)*/ printf("%ld\n",i) # else # define print_instr(s) # define print_int(i) +# define print_lint(i) #endif /* GC interface */ @@ -795,12 +797,12 @@ value coq_interprete if (Is_block(accu)) { long index = Tag_val(accu); print_instr("block"); - print_int(index); + print_lint(index); pc += pc[(sizes & 0xFFFFFF) + index]; } else { long index = Long_val(accu); print_instr("constant"); - print_int(index); + print_lint(index); pc += pc[index]; } Next; @@ -957,7 +959,7 @@ value coq_interprete sp -= nargs; for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2); *--sp = accu; - print_int(nargs); + print_lint(nargs); coq_extra_args = nargs; pc = Code_val(coq_env); goto check_stacks; diff --git a/kernel/constr.ml b/kernel/constr.ml index e823c01b1..e2b1d3fd9 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -475,7 +475,7 @@ let map_with_binders g f l c0 = match kind c0 with optimisation that physically equal arrays are equals (hence the calls to {!Array.equal_norefl}). *) -let compare_head_gen_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 = +let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 = match kind1 t1, kind2 t2 with | Rel n1, Rel n2 -> Int.equal n1 n2 | Meta m1, Meta m2 -> Int.equal m1 m2 @@ -512,13 +512,19 @@ let compare_head_gen_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 = not taken into account *) let compare_head_gen_leq eq_universes leq_sorts eq leq t1 t2 = - compare_head_gen_with kind kind eq_universes leq_sorts eq leq t1 t2 + compare_head_gen_leq_with kind kind eq_universes leq_sorts eq leq t1 t2 -(* [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare - the immediate subterms of [c1] of [c2] if needed, [u] to compare universe - instances and [s] to compare sorts; Cast's, +(* [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to + compare the immediate subterms of [c1] of [c2] if needed, [u] to + compare universe instances and [s] to compare sorts; Cast's, application associativity, binders name and Cases annotations are - not taken into account *) + not taken into account. + + [compare_head_gen_with] is a variant taking kind-of-term functions, + to expose subterms of [c1] and [c2], as arguments. *) + +let compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq t1 t2 = + compare_head_gen_leq_with kind1 kind2 eq_universes eq_sorts eq eq t1 t2 let compare_head_gen eq_universes eq_sorts eq t1 t2 = compare_head_gen_leq eq_universes eq_sorts eq eq t1 t2 @@ -536,14 +542,6 @@ let rec eq_constr m n = let equal m n = eq_constr m n (* to avoid tracing a recursive fun *) -let rec equal_with kind1 kind2 m n = - (* note that pointer equality is not sufficient to ensure equality - up to [eq_evars], because we may evaluates evars of [m] and [n] - in different evar contexts. *) - let req_constr m n = equal_with kind1 kind2 m n in - compare_head_gen_with kind1 kind2 - (fun _ -> Instance.equal) Sorts.equal req_constr req_constr m n - let eq_constr_univs univs m n = if m == n then true else @@ -567,7 +565,7 @@ let leq_constr_univs univs m n = let rec compare_leq m n = compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n and leq_constr' m n = m == n || compare_leq m n in - compare_leq m n + compare_leq m n let eq_constr_univs_infer univs m n = if m == n then true, Constraint.empty @@ -578,16 +576,16 @@ let eq_constr_univs_infer univs m n = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_eq univs u1 u2 then true - else - (cstrs := Univ.enforce_eq u1 u2 !cstrs; - true) + if Univ.check_eq univs u1 u2 then true + else + (cstrs := Univ.enforce_eq u1 u2 !cstrs; + true) in let rec eq_constr' m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n in let res = compare_head_gen eq_universes eq_sorts eq_constr' m n in - res, !cstrs + res, !cstrs let leq_constr_univs_infer univs m n = if m == n then true, Constraint.empty @@ -598,18 +596,18 @@ let leq_constr_univs_infer univs m n = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_eq univs u1 u2 then true - else (cstrs := Univ.enforce_eq u1 u2 !cstrs; - true) + if Univ.check_eq univs u1 u2 then true + else (cstrs := Univ.enforce_eq u1 u2 !cstrs; + true) in let leq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_leq univs u1 u2 then true - else - (cstrs := Univ.enforce_leq u1 u2 !cstrs; - true) + if Univ.check_leq univs u1 u2 then true + else + (cstrs := Univ.enforce_leq u1 u2 !cstrs; + true) in let rec eq_constr' m n = m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n @@ -618,7 +616,7 @@ let leq_constr_univs_infer univs m n = compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n and leq_constr' m n = m == n || compare_leq m n in let res = compare_leq m n in - res, !cstrs + res, !cstrs let always_true _ _ = true diff --git a/kernel/constr.mli b/kernel/constr.mli index 67d1adedf..e6a3e71f8 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -203,14 +203,6 @@ val kind : constr -> (constr, types) kind_of_term and application grouping *) val equal : constr -> constr -> bool -(** [equal_with_evars k1 k2 a b] is true when [a] equals [b] modulo - alpha, casts, application grouping, and using [k1] to expose the - head of [a] and [k2] to expose the head of [b]. *) -val equal_with : - (constr -> (constr,types) kind_of_term) -> - (constr -> (constr,types) kind_of_term) -> - constr -> constr -> bool - (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts, application grouping and the universe equalities in [u]. *) val eq_constr_univs : constr Univ.check_function @@ -293,6 +285,18 @@ val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> (constr -> constr -> bool) -> constr -> constr -> bool +(** [compare_head_gen_with k1 k2 u s f c1 c2] compares [c1] and [c2] + like [compare_head_gen u s f c1 c2], except that [k1] (resp. [k2]) + is used,rather than {!kind}, to expose the immediate subterms of + [c1] (resp. [c2]). *) +val compare_head_gen_with : + (constr -> (constr,types) kind_of_term) -> + (constr -> (constr,types) kind_of_term) -> + (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> + (Sorts.t -> Sorts.t -> bool) -> + (constr -> constr -> bool) -> + constr -> constr -> bool + (** [compare_head_gen_leq u s f fle c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] for conversion, [fle] for cumulativity, [u] to compare universe diff --git a/kernel/names.ml b/kernel/names.ml index 4ccf5b60a..480b37e89 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -33,9 +33,9 @@ struct let hash = String.hash - let check_soft x = + let check_soft ?(warn = true) x = let iter (fatal, x) = - if fatal then Errors.error x else Pp.msg_warning (str x) + if fatal then Errors.error x else if warn then Pp.msg_warning (str x) in Option.iter iter (Unicode.ident_refutation x) @@ -48,6 +48,11 @@ struct let s = String.copy s in String.hcons s + let of_string_soft s = + let () = check_soft ~warn:false s in + let s = String.copy s in + String.hcons s + let to_string id = String.copy id let print id = str id diff --git a/kernel/names.mli b/kernel/names.mli index d82043da1..92ee58f26 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -29,7 +29,11 @@ sig val of_string : string -> t (** Converts a string into an identifier. May raise [UserError _] if the - string is not valid. *) + string is not valid, or echo a warning if it contains invalid identifier + characters. *) + + val of_string_soft : string -> t + (** Same as {!of_string} except that no warning is ever issued. *) val to_string : t -> string (** Converts a identifier into an string. *) diff --git a/lib/dyn.ml b/lib/dyn.ml index a5e8fb9c2..056b68731 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -7,6 +7,7 @@ (************************************************************************) open Errors +open Pp (* Dynamics, programmed with DANGER !!! *) @@ -23,7 +24,7 @@ let create (s : string) = let () = if Int.Map.mem hash !dyntab then let old = Int.Map.find hash !dyntab in - let msg = Pp.str ("Dynamic tag collision: " ^ s ^ " vs. " ^ old) in + let msg = str "Dynamic tag collision: " ++ str s ++ str " vs. " ++ str old in anomaly ~label:"Dyn.create" msg in let () = dyntab := Int.Map.add hash s !dyntab in @@ -31,8 +32,7 @@ let create (s : string) = let outfun (nh, rv) = if Int.equal hash nh then Obj.magic rv else - let msg = (Pp.str ("dyn_out: expected " ^ s)) in - anomaly msg + anomaly (str "dyn_out: expected " ++ str s) in (infun, outfun) @@ -43,8 +43,7 @@ let has_tag (s, _) tag = let tag (s,_) = try Int.Map.find s !dyntab with Not_found -> - let msg = Pp.str ("Unknown dynamic tag " ^ (string_of_int s)) in - anomaly msg + anomaly (str "Unknown dynamic tag " ++ int s) let pointer_equal (t1,o1) (t2,o2) = t1 = t2 && o1 == o2 diff --git a/lib/errors.ml b/lib/errors.ml index a4ec357ee..999d99ee0 100644 --- a/lib/errors.ml +++ b/lib/errors.ml @@ -69,12 +69,12 @@ let rec print_gen bottom stk e = let where = function | None -> mt () | Some s -> - if !Flags.debug then str ("in "^s^":") ++ spc () else mt () + if !Flags.debug then str "in " ++ str s ++ str ":" ++ spc () else mt () let raw_anomaly e = match e with | Anomaly (s, pps) -> where s ++ pps ++ str "." - | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e ^ ".") - | _ -> str ("Uncaught exception " ^ Printexc.to_string e ^ ".") + | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e) ++ str "." + | _ -> str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "." let print_backtrace e = match Backtrace.get_backtrace e with | None -> mt () @@ -99,6 +99,8 @@ let iprint (e, info) = print ~info e (** Same as [print], except that the "Please report" part of an anomaly isn't printed (used in Ltac debugging). *) let print_no_report e = print_gen (print_anomaly false) !handle_stack e +let iprint_no_report (e, info) = + print_gen (print_anomaly false) !handle_stack e ++ print_backtrace info (** Predefined handlers **) diff --git a/lib/errors.mli b/lib/errors.mli index 03caa6a9f..5bd572474 100644 --- a/lib/errors.mli +++ b/lib/errors.mli @@ -80,6 +80,7 @@ val iprint : Exninfo.iexn -> Pp.std_ppcmds (** Same as [print], except that the "Please report" part of an anomaly isn't printed (used in Ltac debugging). *) val print_no_report : exn -> Pp.std_ppcmds +val iprint_no_report : Exninfo.iexn -> Pp.std_ppcmds (** Critical exceptions should not be caught and ignored by mistake by inner functions during a [vernacinterp]. They should be handled @@ -8,13 +8,9 @@ module Glue : sig - (* A left associative glue implements efficient glue operator - when used as left associative. If glue is denoted ++ then + (** The [Glue] module implements a container data structure with + efficient concatenation. *) - a ++ b ++ c ++ d = ((a ++ b) ++ c) ++ d = [d] @ ([c] @ ([b] @ [a])) - - I.e. if the short list is the second argument - *) type 'a t val atom : 'a -> 'a t @@ -22,19 +18,28 @@ module Glue : sig val empty : 'a t val is_empty : 'a t -> bool val iter : ('a -> unit) -> 'a t -> unit - val map : ('a -> 'b) -> 'a t -> 'b t end = struct - type 'a t = 'a list + type 'a t = GEmpty | GLeaf of 'a | GNode of 'a t * 'a t + + let atom x = GLeaf x + + let glue x y = + match x, y with + | GEmpty, _ -> y + | _, GEmpty -> x + | _, _ -> GNode (x,y) + + let empty = GEmpty - let atom x = [x] - let glue x y = y @ x - let empty = [] - let is_empty x = x = [] + let is_empty x = x = GEmpty + + let rec iter f = function + | GEmpty -> () + | GLeaf x -> f x + | GNode (x,y) -> iter f x; iter f y - let iter f g = List.iter f (List.rev g) - let map = List.map end module Tag : @@ -145,21 +150,6 @@ let app = Glue.glue let is_empty g = Glue.is_empty g -let rewrite f p = - let strtoken = function - | Str_len (s, n) -> - let s' = f s in - Str_len (s', String.length s') - | Str_def s -> - Str_def (f s) - in - let rec ppcmd_token = function - | Ppcmd_print x -> Ppcmd_print (strtoken x) - | Ppcmd_box (bt, g) -> Ppcmd_box (bt, Glue.map ppcmd_token g) - | p -> p - in - Glue.map ppcmd_token p - (* Compute length of an UTF-8 encoded string Rem 1 : utf8_length <= String.length (equal if pure ascii) Rem 2 : if used for an iso8859_1 encoded string, the result is @@ -259,7 +249,7 @@ let escape_string s = else escape_at s (i-1) in escape_at s (String.length s - 1) -let qstring s = str ("\""^escape_string s^"\"") +let qstring s = str "\"" ++ str (escape_string s) ++ str "\"" let qs = qstring let quote s = h 0 (str "\"" ++ s ++ str "\"") @@ -458,6 +448,27 @@ let logger = ref std_logger let make_pp_emacs() = print_emacs:=true; logger:=emacs_logger let make_pp_nonemacs() = print_emacs:=false; logger := std_logger +let ft_logger old_logger ft ~id level mesg = match level with + | Debug _ -> msgnl_with ft (debugbody mesg) + | Info -> msgnl_with ft (infobody mesg) + | Notice -> msgnl_with ft mesg + | Warning -> old_logger ~id:id level mesg + | Error -> old_logger ~id:id level mesg + +let with_output_to_file fname func input = + let old_logger = !logger in + let channel = open_out (String.concat "." [fname; "out"]) in + logger := ft_logger old_logger (Format.formatter_of_out_channel channel); + try + let output = func input in + logger := old_logger; + close_out channel; + output + with reraise -> + let reraise = Backtrace.add_backtrace reraise in + logger := old_logger; + close_out channel; + Exninfo.iraise reraise let feedback_id = ref (Feedback.Edit 0) let feedback_route = ref Feedback.default_route diff --git a/lib/pp.mli b/lib/pp.mli index 5dd2686d1..3b1123a9d 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -12,6 +12,8 @@ val make_pp_emacs:unit -> unit val make_pp_nonemacs:unit -> unit +val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b + (** Pretty-printers. *) type std_ppcmds @@ -46,9 +48,6 @@ val eval_ppcmds : std_ppcmds -> std_ppcmds val is_empty : std_ppcmds -> bool (** Test emptyness. *) -val rewrite : (string -> string) -> std_ppcmds -> std_ppcmds -(** [rewrite f pps] applies [f] to all strings that appear in [pps]. *) - (** {6 Derived commands} *) val spc : unit -> std_ppcmds diff --git a/lib/system.ml b/lib/system.ml index 70f590462..e4a60eccb 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -159,7 +159,8 @@ let is_in_system_path filename = let open_trapping_failure name = try open_out_bin name - with e when Errors.noncritical e -> error ("Can't open " ^ name) + with e when Errors.noncritical e -> + errorlabstrm "System.open" (str "Can't open " ++ str name) let try_remove filename = try Sys.remove filename @@ -167,7 +168,8 @@ let try_remove filename = msg_warning (str"Could not remove file " ++ str filename ++ str" which is corrupted!") -let error_corrupted file s = error (file ^": " ^ s ^ ". Try to rebuild it.") +let error_corrupted file s = + errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.") let input_binary_int f ch = try input_binary_int ch @@ -242,7 +244,8 @@ let extern_intern ?(warn=true) magic = let reraise = Errors.push reraise in let () = try_remove filename in iraise reraise - with Sys_error s -> error ("System error: " ^ s) + with Sys_error s -> + errorlabstrm "System.extern_state" (str "System error: " ++ str s) and intern_state paths name = try let _,filename = find_file_in_path ~warn paths name in @@ -251,7 +254,7 @@ let extern_intern ?(warn=true) magic = close_in channel; v with Sys_error s -> - error("System error: " ^ s) + errorlabstrm "System.intern_state" (str "System error: " ++ str s) in (extern_state,intern_state) diff --git a/library/declaremods.ml b/library/declaremods.ml index cc7c4d7f1..a82f5260b 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -950,7 +950,7 @@ type 'modast module_params = let debug_print_modtab _ = let pr_seg = function | [] -> str "[]" - | l -> str ("[." ^ string_of_int (List.length l) ^ ".]") + | l -> str "[." ++ int (List.length l) ++ str ".]" in let pr_modinfo mp (prefix,substobjs,keepobjs) s = s ++ str (string_of_mp mp) ++ (spc ()) diff --git a/library/goptions.ml b/library/goptions.ml index ef25fa590..4f50fbfbd 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -35,7 +35,7 @@ type option_state = { let nickname table = String.concat " " table let error_undeclared_key key = - error ((nickname key)^": no table or option of this type") + errorlabstrm "Goptions" (str (nickname key) ++ str ": no table or option of this type") (****************************************************************************) (* 1- Tables *) @@ -301,7 +301,9 @@ let declare_string_option = let set_option_value locality check_and_cast key v = let (name, depr, (_,read,write,lwrite,gwrite)) = try get_option key - with Not_found -> error ("There is no option "^(nickname key)^".") + with Not_found -> + errorlabstrm "Goptions.set_option_value" + (str "There is no option " ++ str (nickname key) ++ str ".") in let write = match locality with | None -> write @@ -364,9 +366,9 @@ let print_option_value key = let s = read () in match s with | BoolValue b -> - msg_info (str ("The "^name^" mode is "^(if b then "on" else "off"))) + msg_info (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off")) | _ -> - msg_info (str ("Current value of "^name^" is ") ++ msg_option_value (name, s)) + msg_info (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s)) let get_tables () = let tables = !value_tab in @@ -383,7 +385,7 @@ let get_tables () = let print_tables () = let print_option key name value depr = - let msg = str (" "^(nickname key)^": ") ++ msg_option_value (name, value) in + let msg = str " " ++ str (nickname key) ++ str ": " ++ msg_option_value (name, value) in if depr then msg ++ str " [DEPRECATED]" ++ fnl () else msg ++ fnl () in @@ -401,10 +403,10 @@ let print_tables () = !value_tab (mt ()) ++ str "Tables:" ++ fnl () ++ List.fold_right - (fun (nickkey,_) p -> p ++ str (" "^nickkey) ++ fnl ()) + (fun (nickkey,_) p -> p ++ str " " ++ str nickkey ++ fnl ()) !string_table (mt ()) ++ List.fold_right - (fun (nickkey,_) p -> p ++ str (" "^nickkey) ++ fnl ()) + (fun (nickkey,_) p -> p ++ str " " ++ str nickkey ++ fnl ()) !ref_table (mt ()) ++ fnl () diff --git a/library/impargs.ml b/library/impargs.ml index 4b0e2e3d1..94f53219e 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -10,6 +10,7 @@ open Errors open Util open Names open Globnames +open Nameops open Term open Reduction open Declarations @@ -337,10 +338,12 @@ let check_correct_manual_implicits autoimps l = List.iter (function | ExplByName id,(b,fi,forced) -> if not forced then - error ("Wrong or non-dependent implicit argument name: "^(Id.to_string id)^".") + errorlabstrm "" + (str "Wrong or non-dependent implicit argument name: " ++ pr_id id ++ str ".") | ExplByPos (i,_id),_t -> if i<1 || i>List.length autoimps then - error ("Bad implicit argument number: "^(string_of_int i)^".") + errorlabstrm "" + (str "Bad implicit argument number: " ++ int i ++ str ".") else errorlabstrm "" (str "Cannot set implicit argument number " ++ int i ++ diff --git a/library/lib.ml b/library/lib.ml index 9977b6665..81db547ef 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -75,7 +75,8 @@ let classify_segment seg = | (_,ClosedModule _) :: stk -> clean acc stk | (_,OpenedSection _) :: _ -> error "there are still opened sections" | (_,OpenedModule (ty,_,_,_)) :: _ -> - error ("there are still opened " ^ module_kind ty ^"s") + errorlabstrm "Lib.classify_segment" + (str "there are still opened " ++ str (module_kind ty) ++ str "s") | (_,FrozenState _) :: stk -> clean acc stk in clean ([],[],[]) (List.rev seg) @@ -274,7 +275,7 @@ let start_modtype = start_mod true None let error_still_opened string oname = let id = basename (fst oname) in errorlabstrm "" - (str ("The "^string^" ") ++ pr_id id ++ str " is still opened.") + (str "The " ++ str string ++ str " " ++ pr_id id ++ str " is still opened.") let end_mod is_type = let oname,fs = @@ -318,7 +319,8 @@ let end_compilation_checks dir = try match snd (find_entry_p is_opening_node) with | OpenedSection _ -> error "There are some open sections." | OpenedModule (ty,_,_,_) -> - error ("There are some open "^module_kind ty^"s.") + errorlabstrm "Lib.end_compilation_checks" + (str "There are some open " ++ str (module_kind ty) ++ str "s.") | _ -> assert false with Not_found -> () in @@ -369,7 +371,8 @@ let find_opening_node id = let oname,entry = find_entry_p is_opening_node in let id' = basename (fst oname) in if not (Names.Id.equal id id') then - error ("Last block to end has name "^(Names.Id.to_string id')^"."); + errorlabstrm "Lib.find_opening_node" + (str "Last block to end has name " ++ pr_id id' ++ str "."); entry with Not_found -> error "There is nothing to end." diff --git a/library/libobject.ml b/library/libobject.ml index 5f2a2127d..74930d76e 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -7,6 +7,7 @@ (************************************************************************) open Libnames +open Pp (* The relax flag is used to make it possible to load files while ignoring failures to incorporate some objects. This can be useful when one @@ -33,15 +34,13 @@ type 'a object_declaration = { discharge_function : object_name * 'a -> 'a option; rebuild_function : 'a -> 'a } -let yell s = Errors.anomaly (Pp.str s) - let default_object s = { object_name = s; cache_function = (fun _ -> ()); load_function = (fun _ _ -> ()); open_function = (fun _ _ -> ()); subst_function = (fun _ -> - yell ("The object "^s^" does not know how to substitute!")); + Errors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!")); classify_function = (fun obj -> Keep obj); discharge_function = (fun _ -> None); rebuild_function = (fun x -> x)} diff --git a/library/library.ml b/library/library.ml index 9d0ccb972..1ffa1a305 100644 --- a/library/library.ml +++ b/library/library.ml @@ -126,7 +126,8 @@ let find_library dir = let try_find_library dir = try find_library dir with Not_found -> - error ("Unknown library " ^ (DirPath.to_string dir)) + errorlabstrm "Library.find_library" + (str "Unknown library " ++ str (DirPath.to_string dir)) let register_library_filename dir f = (* Not synchronized: overwrite the previous binding if one existed *) @@ -378,10 +379,10 @@ let access_table what tables dp i = let t = try fetch_delayed f with Faulty f -> - error - ("The file "^f^" (bound to " ^ dir_path ^ - ") is inaccessible or corrupted,\n" ^ - "cannot load some "^what^" in it.\n") + errorlabstrm "Library.access_table" + (str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++ + str ") is inaccessible or corrupted,\ncannot load some " ++ + str what ++ str " in it.\n") in tables := LibraryMap.add dp (Fetched t) !tables; t @@ -462,7 +463,7 @@ let rec intern_library (needed, contents) (dir, f) from = let m = intern_from_file f in if not (DirPath.equal dir m.library_name) then errorlabstrm "load_physical_library" - (str ("The file " ^ f ^ " contains library") ++ spc () ++ + (str "The file " ++ str f ++ str " contains library" ++ spc () ++ pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir); Pp.feedback(Feedback.FileLoaded(DirPath.to_string dir, f)); @@ -475,9 +476,7 @@ and intern_library_deps libs dir m from = and intern_mandatory_library caller from libs (dir,d) = let digest, libs = intern_library libs (try_locate_absolute_library dir) from in if not (Safe_typing.digest_match ~actual:digest ~required:d) then - errorlabstrm "" (strbrk ("Compiled library "^ DirPath.to_string caller ^ - ".vo makes inconsistent assumptions over library " ^ - DirPath.to_string dir)); + errorlabstrm "" (str "Compiled library " ++ str (DirPath.to_string caller) ++ str ".vo makes inconsistent assumptions over library " ++ str (DirPath.to_string dir)); libs let rec_intern_library libs mref = @@ -487,7 +486,7 @@ let rec_intern_library libs mref = let check_library_short_name f dir = function | Some id when not (Id.equal id (snd (split_dirpath dir))) -> errorlabstrm "check_library_short_name" - (str ("The file " ^ f ^ " contains library") ++ spc () ++ + (str "The file " ++ str f ++ str " contains library" ++ spc () ++ pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++ pr_id id) | _ -> () @@ -613,7 +612,7 @@ let safe_locate_module (loc,qid) = try Nametab.locate_module qid with Not_found -> user_err_loc - (loc,"import_library", str (string_of_qualid qid ^ " is not a module")) + (loc,"import_library", str (string_of_qualid qid) ++ str " is not a module") let import_module export modl = (* Optimization: libraries in a raw in the list are imported @@ -633,7 +632,12 @@ let import_module export modl = with Not_found-> flush acc; safe_locate_module m, [] in (match m with | MPfile dir -> aux (dir::acc) l - | mp -> flush acc; Declaremods.import_module export mp; aux [] l) + | mp -> + flush acc; + try Declaremods.import_module export mp; aux [] l + with Not_found -> + user_err_loc (loc,"import_library", + str (string_of_qualid dir) ++ str " is not a module")) | [] -> flush acc in aux [] modl @@ -645,8 +649,8 @@ let check_coq_overwriting p id = let is_empty = match l with [] -> true | _ -> false in if not !Flags.boot && not is_empty && String.equal (Id.to_string (List.last l)) "Coq" then errorlabstrm "" - (strbrk ("Cannot build module "^DirPath.to_string p^"."^Id.to_string id^ - ": it starts with prefix \"Coq\" which is reserved for the Coq library.")) + (str "Cannot build module " ++ str (DirPath.to_string p) ++ str "." ++ pr_id id ++ str "." ++ spc () ++ + str "it starts with prefix \"Coq\" which is reserved for the Coq library.") (* Verifies that a string starts by a letter and do not contain others caracters than letters, digits, or `_` *) @@ -790,7 +794,7 @@ let save_library_to ?todo dir f otab = msg_error (str"Could not compile the library to native code. Skipping.") with reraise -> let reraise = Errors.push reraise in - let () = msg_warning (str ("Removed file "^f')) in + let () = msg_warning (str "Removed file " ++ str f') in let () = close_out ch in let () = Sys.remove f' in iraise reraise diff --git a/library/universes.ml b/library/universes.ml index 9fddc7067..3a8ee2625 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -139,6 +139,32 @@ let eq_constr_univs_infer univs m n = let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in res, !cstrs +(** Variant of [eq_constr_univs_infer] taking kind-of-term functions, + to expose subterms of [m] and [n], arguments. *) +let eq_constr_univs_infer_with kind1 kind2 univs m n = + (* spiwack: duplicates the code of [eq_constr_univs_infer] because I + haven't find a way to factor the code without destroying + pointer-equality optimisations in [eq_constr_univs_infer]. + Pointer equality is not sufficient to ensure equality up to + [kind1,kind2], because [kind1] and [kind2] may be different, + typically evaluating [m] and [n] in different evar maps. *) + let cstrs = ref Constraints.empty in + let eq_universes strict = Univ.Instance.check_eq univs in + let eq_sorts s1 s2 = + if Sorts.equal s1 s2 then true + else + let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in + if Univ.check_eq univs u1 u2 then true + else + (cstrs := Constraints.add (u1, UEq, u2) !cstrs; + true) + in + let rec eq_constr' m n = + Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n + in + let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in + res, !cstrs + let leq_constr_univs_infer univs m n = if m == n then true, Constraints.empty else @@ -148,18 +174,18 @@ let leq_constr_univs_infer univs m n = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_eq univs u1 u2 then true - else (cstrs := Constraints.add (u1, UEq, u2) !cstrs; - true) + if Univ.check_eq univs u1 u2 then true + else (cstrs := Constraints.add (u1, UEq, u2) !cstrs; + true) in let leq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_leq univs u1 u2 then true - else - (cstrs := Constraints.add (u1, ULe, u2) !cstrs; - true) + if Univ.check_leq univs u1 u2 then true + else + (cstrs := Constraints.add (u1, ULe, u2) !cstrs; + true) in let rec eq_constr' m n = m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n @@ -169,7 +195,7 @@ let leq_constr_univs_infer univs m n = eq_constr' leq_constr' m n and leq_constr' m n = m == n || compare_leq m n in let res = compare_leq m n in - res, !cstrs + res, !cstrs let eq_constr_universes m n = if m == n then true, Constraints.empty @@ -188,7 +214,7 @@ let eq_constr_universes m n = m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in - res, !cstrs + res, !cstrs let leq_constr_universes m n = if m == n then true, Constraints.empty @@ -216,22 +242,22 @@ let leq_constr_universes m n = Constr.compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n and leq_constr' m n = m == n || compare_leq m n in let res = compare_leq m n in - res, !cstrs + res, !cstrs let compare_head_gen_proj env equ eqs eqc' m n = match kind_of_term m, kind_of_term n with | Proj (p, c), App (f, args) | App (f, args), Proj (p, c) -> - (match kind_of_term f with - | Const (p', u) when eq_constant (Projection.constant p) p' -> - let pb = Environ.lookup_projection p env in - let npars = pb.Declarations.proj_npars in - if Array.length args == npars + 1 then - eqc' c args.(npars) - else false - | _ -> false) + (match kind_of_term f with + | Const (p', u) when eq_constant (Projection.constant p) p' -> + let pb = Environ.lookup_projection p env in + let npars = pb.Declarations.proj_npars in + if Array.length args == npars + 1 then + eqc' c args.(npars) + else false + | _ -> false) | _ -> Constr.compare_head_gen equ eqs eqc' m n - + let eq_constr_universes_proj env m n = if m == n then true, Constraints.empty else @@ -249,7 +275,7 @@ let eq_constr_universes_proj env m n = m == n || compare_head_gen_proj env eq_universes eq_sorts eq_constr' m n in let res = eq_constr' m n in - res, !cstrs + res, !cstrs (* Generator of levels *) let new_univ_level, set_remote_new_univ_level = diff --git a/library/universes.mli b/library/universes.mli index 252648d7d..5527da090 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -66,6 +66,14 @@ val to_constraints : universes -> universe_constraints -> constraints application grouping, the universe constraints in [u] and additional constraints [c]. *) val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained +(** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of + {!eq_constr_univs_infer} taking kind-of-term functions, to expose + subterms of [m] and [n], arguments. *) +val eq_constr_univs_infer_with : + (constr -> (constr,types) kind_of_term) -> + (constr -> (constr,types) kind_of_term) -> + Univ.universes -> constr -> constr -> bool universe_constrained + (** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b] modulo alpha, casts, application grouping, the universe constraints in [u] and additional constraints [c]. *) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 3bb029a88..74f17f9fb 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -223,12 +223,6 @@ GEXTEND Gram CHole (!@loc, None, IntroAnonymous, Some arg) ] ] ; - forall: - [ [ "forall" -> () ] ] - ; - lambda: - [ [ "fun" -> () ] ] - ; record_declaration: [ [ fs = LIST0 record_field_declaration SEP ";" -> CRecord (!@loc, None, fs) (* | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *) @@ -240,9 +234,9 @@ GEXTEND Gram (id, abstract_constr_expr c (binders_of_lidents params)) ] ] ; binder_constr: - [ [ forall; bl = open_binders; ","; c = operconstr LEVEL "200" -> + [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" -> mkCProdN (!@loc) bl c - | lambda; bl = open_binders; "=>"; c = operconstr LEVEL "200" -> + | "fun"; bl = open_binders; "=>"; c = operconstr LEVEL "200" -> mkCLambdaN (!@loc) bl c | "let"; id=name; bl = binders; ty = type_cstr; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index cf7f6af28..09059b410 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -79,6 +79,7 @@ GEXTEND Gram GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command; vernac: FIRST [ [ IDENT "Time"; l = vernac_list -> VernacTime l + | IDENT "Redirect"; s = ne_string; l = vernac_list -> VernacRedirect (s, l) | IDENT "Timeout"; n = natural; v = vernac -> VernacTimeout(n,v) | IDENT "Fail"; v = vernac -> VernacFail v diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 84e4a5732..992f9c59a 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -58,7 +58,7 @@ END let error_bad_arity loc n = let s = match n with 0 -> "none" | 1 -> "one" | 2 -> "two" | _ -> "many" in - user_err_loc (loc,"",str ("wrong number of arguments (expect "^s^").")) + user_err_loc (loc,"",str "wrong number of arguments (expect " ++ str s ++ str ").") (* Interpreting attributes *) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 8884aef1c..05f4c4903 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -302,9 +302,9 @@ let rec proof_tac p : unit Proofview.tactic = Tacticals.New.tclFIRST [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2); reflexivity; - Proofview.tclZERO (UserError ("Congruence" , + Tacticals.New.tclZEROMSG (Pp.str - "I don't know how to handle dependent equality")))]] + "I don't know how to handle dependent equality")]] | Inject (prf,cstr,nargs,argind) -> let ti=constr_of_term prf.p_lhs in let tj=constr_of_term prf.p_rhs in diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 9d0b7f346..36273faae 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -125,10 +125,34 @@ let go_to_proof_mode () = (* closing gaps *) +(* spiwack: should use [Proofview.give_up] but that would require + moving the whole declarative mode into the new proof engine. It + will eventually have to be done. + + As far as I can tell, [daimon_tac] is used after a [thus thesis], + it will leave uninstantiated variables instead of giving a relevant + message at [Qed]. *) let daimon_tac gls = set_daimon_flag (); {it=[];sigma=sig_sig gls;} +let daimon_instr env p = + let (p,(status,_)) = + Proof.run_tactic env begin + Proofview.tclINDEPENDENT Proofview.give_up + end p + in + p,status + +let do_daimon () = + let env = Global.env () in + let status = + Proof_global.with_current_proof begin fun _ p -> + daimon_instr env p + end + in + if not status then Pp.feedback Feedback.AddedAxiom else () + (* post-instruction focus management *) let goto_current_focus () = @@ -144,7 +168,7 @@ let goto_current_focus_or_top () = (* return *) let close_tactic_mode () = - try goto_current_focus () + try do_daimon ();goto_current_focus () with Not_found -> error "\"return\" cannot be used outside of Declarative Proof Mode." @@ -165,7 +189,7 @@ let close_block bt pts = in match bt,stack with B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] -> - (goto_current_focus ()) + do_daimon ();goto_current_focus () | _, Claim::_ -> error "\"end claim\" expected." | _, Focus_claim::_ -> @@ -196,7 +220,7 @@ let close_previous_case pts = match get_stack pts with Per (et,_,_,_) :: _ -> () | Suppose_case :: Per (et,_,_,_) :: _ -> - goto_current_focus () + do_daimon ();goto_current_focus () | _ -> error "Not inside a proof per cases or induction." (* Proof instructions *) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 45e5aaf54..a2bbf97ae 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -604,7 +604,8 @@ let build_scheme fas = try Smartlocate.global_with_alias f with Not_found -> - Errors.error ("Cannot find "^ Libnames.string_of_reference f) + errorlabstrm "FunInd.build_scheme" + (str "Cannot find " ++ Libnames.pr_reference f) in let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' f in @@ -636,10 +637,12 @@ let build_case_scheme fa = (* let id_to_constr id = *) (* Constrintern.global_reference id *) (* in *) - let funs = (fun (_,f,_) -> - try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f)) - with Not_found -> - Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in + let funs = + let (_,f,_) = fa in + try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f)) + with Not_found -> + errorlabstrm "FunInd.build_case_scheme" + (str "Cannot find " ++ Libnames.pr_reference f) in let first_fun,u = destConst funs in let funs_mp,funs_dp,_ = Names.repr_con first_fun in let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 738ade8ca..1c409500e 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -109,7 +109,9 @@ let const_of_id id = qualid_of_reference (Libnames.Ident (Loc.ghost,id)) in try Constrintern.locate_reference princ_ref - with Not_found -> Errors.error ("cannot find "^ Id.to_string id) + with Not_found -> + Errors.errorlabstrm "IndFun.const_of_id" + (str "cannot find " ++ Nameops.pr_id id) let def_of_const t = match (Term.kind_of_term t) with diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d9ae87ecc..d10924f88 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -378,7 +378,6 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres))); (* Conclusion *) observe_tac "exact" (fun g -> - Pp.msgnl (str "TITI " ++ pf_apply Printer.pr_lconstr_env g (app_constructor g)); Proofview.V82.of_tactic (exact_check (app_constructor g)) g) ] ) @@ -427,7 +426,6 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes in (params_bindings@lemmas_bindings) in - Pp.msgnl (str "princ_type := " ++ pf_apply Printer.pr_lconstr_env g princ_type); tclTHENSEQ [ observe_tac "principle" (Proofview.V82.of_tactic (assert_by diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index c6fab43d1..77a7f006b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -305,7 +305,8 @@ let check_not_nested forbidden e = | Rel _ -> () | Var x -> if Id.List.mem x forbidden - then error ("check_not_nested : failure "^Id.to_string x) + then errorlabstrm "Recdef.check_not_nested" + (str "check_not_nested: failure " ++ pr_id x) | Meta _ | Evar _ | Sort _ -> () | Cast(e,_,t) -> check_not_nested e;check_not_nested t | Prod(_,t,b) -> check_not_nested t;check_not_nested b diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 37428c39d..4e2696dfd 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1462,7 +1462,7 @@ let coq_omega = let path = simplify_strong (new_id,new_var_num,display_var) system in if !display_action_flag then display_action display_var path; Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path) - with NO_CONTRADICTION -> Proofview.tclZERO (UserError ("" , Pp.str"Omega can't solve this system")) + with NO_CONTRADICTION -> Tacticals.New.tclZEROMSG (Pp.str"Omega can't solve this system") end end diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 161cffa86..e28180713 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -428,7 +428,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = | [] -> assert false | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) in - let sub = (env, c1) :: subargs env lc in + let sub = (env, hd) :: (env, c1) :: subargs env lc in let next () = try_aux sub next_mk_ctx next in authorized_occ env sigma partial_app closed pat c mk_ctx next | Fix (indx,(names,types,bodies)) -> diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f388f9005..97b1b1645 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -201,13 +201,6 @@ let ise_and evd l = | UnifFailure _ as x -> x in ise_and evd l -(* This function requires to get the outermost arguments first. It is - a fold_right for backward compatibility. - - It tries to unify the suffix of 2 lists element by element and if - it reaches the end of a list, it returns the remaining elements in - the other list if there are some. -*) let ise_exact ise x1 x2 = match ise x1 x2 with | None, out -> out diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 201a16ebe..2508f4ef3 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -844,6 +844,25 @@ let subterm_source evk (loc,k) = (loc,Evar_kinds.SubEvar evk) -(** Term exploration up to isntantiation. *) +(** Term exploration up to instantiation. *) let kind_of_term_upto sigma t = Constr.kind (Reductionops.whd_evar sigma t) + +(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and + [u] up to existential variable instantiation and equalisable + universes. The term [t] is interpreted in [sigma1] while [u] is + interpreted in [sigma2]. The universe constraints in [sigma2] are + assumed to be an extention of those in [sigma1]. *) +let eq_constr_univs_test sigma1 sigma2 t u = + (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *) + let open Evd in + let b, c = + Universes.eq_constr_univs_infer_with + (fun t -> kind_of_term_upto sigma1 t) + (fun u -> kind_of_term_upto sigma2 u) + (universes sigma2) t u + in + if b then + try let _ = add_universe_constraints sigma2 c in true + with Univ.UniverseInconsistency _ | UniversesDiffer -> false + else false diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 49036798e..f1d94b0a4 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -206,6 +206,13 @@ val flush_and_check_evars : evar_map -> constr -> constr value of [e] in [sigma] is (recursively) used. *) val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term +(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and + [u] up to existential variable instantiation and equalisable + universes. The term [t] is interpreted in [sigma1] while [u] is + interpreted in [sigma2]. The universe constraints in [sigma2] are + assumed to be an extention of those in [sigma1]. *) +val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool + (** {6 debug pretty-printer:} *) val pr_tycon : env -> type_constraint -> Pp.std_ppcmds diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 705e594af..fb629d049 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -395,7 +395,9 @@ let rec pat_of_raw metas vars = function | Some p, Some (_,_,nal) -> let nvars = na :: List.rev nal @ vars in rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p)) - | _ -> PMeta None + | (None | Some (GHole _)), _ -> PMeta None + | Some p, None -> + user_err_loc (loc,"",strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.") in let info = { cip_style = sty; diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 01e1154e5..c2281e13a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1528,7 +1528,8 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let ids = ids_of_named_context (named_context env) in if name == Anonymous then next_ident_away_in_goal x ids else if mem_named_context x (named_context env) then - error ("The variable "^(Id.to_string x)^" is already declared.") + errorlabstrm "Unification.make_abstraction_core" + (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.") else x in diff --git a/printing/pptactic.ml b/printing/pptactic.ml index a76d73006..b8ad996aa 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1265,13 +1265,12 @@ module Make and pr_tacarg = function | TacDynamic (loc,t) -> - pr_with_comments loc ( - str "<" ++ keyword "dynamic" ++ str (" [" ^ (Dyn.tag t)^"]>") - ) + pr_with_comments loc + (str "<" ++ keyword "dynamic" ++ str " [" ++ str (Dyn.tag t) ++ str "]>") | MetaIdArg (loc,true,s) -> - pr_with_comments loc (str ("$" ^ s)) + pr_with_comments loc (str "$" ++ str s) | MetaIdArg (loc,false,s) -> - pr_with_comments loc (keyword "constr:" ++ str(" $" ^ s)) + pr_with_comments loc (keyword "constr:" ++ str " $" ++ str s) | Reference r -> pr.pr_reference r | ConstrMayEval c -> diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 89ffae4b3..832c08fe0 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -627,6 +627,8 @@ module Make ) | VernacTime v -> return (keyword "Time" ++ spc() ++ pr_vernac_list v) + | VernacRedirect (s, v) -> + return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_list v) | VernacTimeout(n,v) -> return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac v) | VernacFail v -> @@ -1253,7 +1255,7 @@ module Make and pr_extend s cl = let pr_arg a = try pr_gen a - with Failure _ -> str ("<error in "^fst s^">") in + with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in try let rl = Egramml.get_extend_vernac_rule s in let start,rl,cl = @@ -1271,7 +1273,7 @@ module Make (start,cl) rl in hov 1 pp with Not_found -> - hov 1 (str ("TODO("^fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")") + hov 1 (str "TODO(" ++ str (fst s) ++ prlist_with_sep sep pr_arg cl ++ str ")") in pr_vernac diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 4a66c33df..e50435cda 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -180,16 +180,16 @@ let print_opacity ref = | None -> [] | Some s -> [pr_global ref ++ str " is " ++ - str (match s with - | FullyOpaque -> "opaque" + match s with + | FullyOpaque -> str "opaque" | TransparentMaybeOpacified Conv_oracle.Opaque -> - "basically transparent but considered opaque for reduction" + str "basically transparent but considered opaque for reduction" | TransparentMaybeOpacified lev when Conv_oracle.is_transparent lev -> - "transparent" + str "transparent" | TransparentMaybeOpacified (Conv_oracle.Level n) -> - "transparent (with expansion weight "^string_of_int n^")" + str "transparent (with expansion weight " ++ int n ++ str ")" | TransparentMaybeOpacified Conv_oracle.Expand -> - "transparent (with minimal expansion weight)")] + str "transparent (with minimal expansion weight)"] (*******************) (* *) @@ -386,9 +386,9 @@ let print_located_qualid name flags ref = | [] -> let (dir,id) = repr_qualid qid in if DirPath.is_empty dir then - str ("No " ^ name ^ " of basename") ++ spc () ++ pr_id id + str "No " ++ str name ++ str " of basename" ++ spc () ++ pr_id id else - str ("No " ^ name ^ " of suffix") ++ spc () ++ pr_qualid qid + str "No " ++ str name ++ str " of suffix" ++ spc () ++ pr_qualid qid | l -> prlist_with_sep fnl (fun (o,oqid) -> diff --git a/printing/printer.ml b/printing/printer.ml index 0d3a1c17e..141ae145d 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -654,7 +654,7 @@ let pr_goal_by_id id = let p = Proof_global.give_me_the_proof () in let g = Goal.get_by_uid id in let pr gs = - v 0 (str ("goal / evar " ^ id ^ " is:") ++ cut () + v 0 (str "goal / evar " ++ str id ++ str " is:" ++ cut () ++ pr_goal gs) in try @@ -723,7 +723,7 @@ let pr_assumptionset env s = try pr_constant env kn with Not_found -> let mp,_,lab = repr_con kn in - str (string_of_mp mp ^ "." ^ Label.to_string lab) + str (string_of_mp mp) ++ str "." ++ pr_label lab in let safe_pr_ltype typ = try str " : " ++ pr_ltype typ diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index c8cb1d1cc..9b358210a 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -12,6 +12,7 @@ open Names open Evd open Evarutil open Evarsolve +open Pp (******************************************) (* Instantiation of existential variables *) @@ -54,8 +55,8 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = with e when Errors.noncritical e -> let loc = Glob_ops.loc_of_glob_constr rawc in user_err_loc - (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^ - string_of_existential evk)) + (loc,"", str "Instance is not well-typed in the environment of " ++ + str (string_of_existential evk)) in define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma) diff --git a/proofs/logic.ml b/proofs/logic.ml index b8206ca1b..898588d9e 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -179,7 +179,8 @@ let check_decl_position env sign (x,_,_ as d) = let needed = global_vars_set_of_decl env d in let deps = dependency_closure env (named_context_of_val sign) needed in if Id.List.mem x deps then - error ("Cannot create self-referring hypothesis "^Id.to_string x); + errorlabstrm "Logic.check_decl_position" + (str "Cannot create self-referring hypothesis " ++ pr_id x); x::deps (* Auxiliary functions for primitive MOVE tactic @@ -488,9 +489,11 @@ let convert_hyp check sign sigma (id,b,bt as d) = (fun _ (_,c,ct) _ -> let env = Global.env_of_context sign in if check && not (is_conv env sigma bt ct) then - error ("Incorrect change of the type of "^(Id.to_string id)^"."); + errorlabstrm "Logic.convert_hyp" + (str "Incorrect change of the type of " ++ pr_id id ++ str "."); if check && not (Option.equal (is_conv env sigma) b c) then - error ("Incorrect change of the body of "^(Id.to_string id)^"."); + errorlabstrm "Logic.convert_hyp" + (str "Incorrect change of the body of "++ pr_id id ++ str "."); if check then reorder := check_decl_position env sign d; d) in reorder_val_context env sign' !reorder @@ -522,7 +525,8 @@ let prim_refiner r sigma goal = t,cl,sigma else (if !check && mem_named_context id (named_context_of_val sign) then - error ("Variable " ^ Id.to_string id ^ " is already declared."); + errorlabstrm "Logic.prim_refiner" + (str "Variable " ++ pr_id id ++ str " is already declared."); push_named_context_val (id,None,t) sign,t,cl,sigma) in let (sg2,ev2,sigma) = Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in @@ -550,11 +554,10 @@ let prim_refiner r sigma goal = | (f,n,ar)::oth -> let ((sp',_),u') = check_ind env n ar in if not (eq_mind sp sp') then - error ("Fixpoints should be on the same " ^ - "mutual inductive declaration."); + error "Fixpoints should be on the same mutual inductive declaration."; if !check && mem_named_context f (named_context_of_val sign) then - error - ("Name "^Id.to_string f^" already used in the environment"); + errorlabstrm "Logic.prim_refiner" + (str "Name " ++ pr_id f ++ str " already used in the environment"); mk_sign (push_named_context_val (f,None,ar) sign) oth | [] -> Evd.Monad.List.map (fun (_,_,c) sigma -> @@ -584,8 +587,7 @@ let prim_refiner r sigma goal = try let _ = find_coinductive env sigma b in () with Not_found -> - error ("All methods must construct elements " ^ - "in coinductive types.") + error "All methods must construct elements in coinductive types." in let firsts,lasts = List.chop j others in let all = firsts@(f,cl)::lasts in diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 6f6263413..6e653806b 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -722,19 +722,7 @@ let give_up = module Progress = struct - (** equality function up to evar instantiation in heterogeneous - contexts. *) - (* spiwack (2015-02-19): In the previous version of progress an - equality which considers two universes equal when it is consistent - tu unify them ([Evd.eq_constr_univs_test]) was used. Maybe this - behaviour has to be restored as well. This has to be established by - practice. *) - - let rec eq_constr sigma1 sigma2 t1 t2 = - Constr.equal_with - (fun t -> Evarutil.kind_of_term_upto sigma1 t) - (fun t -> Evarutil.kind_of_term_upto sigma2 t) - t1 t2 + let eq_constr = Evarutil.eq_constr_univs_test (** equality function on hypothesis contexts *) let eq_named_context_val sigma1 sigma2 ctx1 ctx2 = diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 1383d7556..d25f7e915 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -167,18 +167,20 @@ let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction" let declare_reduction s f = if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab - then error ("There is already a reduction expression of name "^s) + then errorlabstrm "Redexpr.declare_reduction" + (str "There is already a reduction expression of name " ++ str s) else reduction_tab := String.Map.add s f !reduction_tab let check_custom = function | ExtraRedExpr s -> if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab) - then error ("Reference to undefined reduction expression "^s) + then errorlabstrm "Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s) |_ -> () let decl_red_expr s e = if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab - then error ("There is already a reduction expression of name "^s) + then errorlabstrm "Redexpr.decl_red_expr" + (str "There is already a reduction expression of name " ++ str s) else begin check_custom e; red_expr_tab := String.Map.add s e !red_expr_tab @@ -232,7 +234,8 @@ let reduction_of_red_expr env = with Not_found -> (try reduction_of_red_expr (String.Map.find s !red_expr_tab) with Not_found -> - error("unknown user-defined reduction \""^s^"\""))) + errorlabstrm "Redexpr.reduction_of_red_expr" + (str "unknown user-defined reduction \"" ++ str s ++ str "\""))) | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast) | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast) in diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 3cc81daf5..d7f4b5ead 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -11,6 +11,7 @@ open Names open Pp open Tacexpr open Termops +open Nameops let (prtac, tactic_printer) = Hook.make () let (prmatchpatt, match_pattern_printer) = Hook.make () @@ -231,17 +232,16 @@ let db_pattern_rule debug num r = (* Prints the hypothesis pattern identifier if it exists *) let hyp_bound = function - | Anonymous -> " (unbound)" - | Name id -> " (bound to "^(Names.Id.to_string id)^")" + | Anonymous -> str " (unbound)" + | Name id -> str " (bound to " ++ pr_id id ++ str ")" (* Prints a matched hypothesis *) let db_matched_hyp debug env (id,_,c) ido = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str "Hypothesis " ++ - str ((Names.Id.to_string id)^(hyp_bound ido)^ - " has been matched: ") ++ print_constr_env env c) + msg_tac_debug (str "Hypothesis " ++ pr_id id ++ hyp_bound ido ++ + str " has been matched: " ++ print_constr_env env c) else return () (* Prints the matched conclusion *) @@ -266,8 +266,8 @@ let db_hyp_pattern_failure debug env sigma (na,hyp) = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str ("The pattern hypothesis"^(hyp_bound na)^ - " cannot match: ") ++ + msg_tac_debug (str "The pattern hypothesis" ++ hyp_bound na ++ + str " cannot match: " ++ Hook.get prmatchpatt env sigma hyp) else return () diff --git a/stm/stm.ml b/stm/stm.ml index 38745e227..977156475 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -86,7 +86,7 @@ let vernac_interp ?proof id ?route { verbose; loc; expr } = | VernacResetName _ | VernacResetInitial | VernacBack _ | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true - | VernacTime el -> List.for_all (fun (_,e) -> internal_command e) el + | VernacTime el | VernacRedirect (_,el) -> List.for_all (fun (_,e) -> internal_command e) el | _ -> false in if internal_command expr then begin prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr)) @@ -1472,7 +1472,7 @@ end = struct (* {{{ *) let e, etac, time, fail = let rec find time fail = function | VernacSolve(_,_,re,b) -> re, b, time, fail - | VernacTime [_,e] -> find true fail e + | VernacTime [_,e] | VernacRedirect (_,[_,e]) -> find true fail e | VernacFail e -> find time true e | _ -> errorlabstrm "Stm" (str"unsupported") in find false false e in Hooks.call Hooks.with_fail fail (fun () -> @@ -2018,7 +2018,7 @@ let handle_failure (e, info) vcs tty = end; VCS.print (); anomaly(str"error with no safe_id attached:" ++ spc() ++ - Errors.print_no_report e) + Errors.iprint_no_report (e, info)) | Some (safe_id, id) -> prerr_endline ("Failed at state " ^ Stateid.to_string id); VCS.restore vcs; diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 180f20ae8..9edc1f1c7 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -490,6 +490,9 @@ let rec tmpp v loc = | VernacTime l -> xmlApply loc (Element("time",[],[]) :: List.map (fun(loc,e) ->tmpp e loc) l) + | VernacRedirect (s, l) -> + xmlApply loc (Element("redirect",["path", s],[]) :: + List.map (fun(loc,e) ->tmpp e loc) l) | VernacTimeout (s,e) -> xmlApply loc (Element("timeout",["val",string_of_int s],[]) :: [tmpp e loc]) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 783ff2e11..2b5eb8683 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -86,7 +86,7 @@ let rec classify_vernac e = make_polymorphic (classify_vernac e) else classify_vernac e | VernacTimeout (_,e) -> classify_vernac e - | VernacTime e -> classify_vernac_list e + | VernacTime e | VernacRedirect (_, e) -> classify_vernac_list e | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match classify_vernac e with | ( VtQuery _ | VtProofStep _ | VtSideff _ diff --git a/tactics/auto.ml b/tactics/auto.ml index 46274f832..7da841571 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -131,7 +131,7 @@ let conclPattern concl pat tac = try Proofview.tclUNIT (Constr_matching.matches env sigma pat concl) with Constr_matching.PatternMatchingFailure -> - Proofview.tclZERO (UserError ("conclPattern",str"conclPattern")) + Tacticals.New.tclZEROMSG (str "conclPattern") in Proofview.Goal.enter (fun gl -> let env = Proofview.Goal.env gl in @@ -458,7 +458,7 @@ let search d n mod_delta db_list local_db = (* spiwack: the test of [n] to 0 must be done independently in each goal. Hence the [tclEXTEND] *) Proofview.tclEXTEND [] begin - if Int.equal n 0 then Proofview.tclZERO (Errors.UserError ("",str"BOUND 2")) else + if Int.equal n 0 then Tacticals.New.tclZEROMSG (str"BOUND 2") else Tacticals.New.tclORELSE0 (dbg_assumption d) (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db) ( Proofview.Goal.enter begin fun gl -> diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 4eb8a7925..ad8164fa6 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -66,7 +66,7 @@ let find_base bas = try raw_find_base bas with Not_found -> errorlabstrm "AutoRewrite" - (str ("Rewriting base "^(bas)^" does not exist.")) + (str "Rewriting base " ++ str bas ++ str " does not exist.") let find_rewrites bas = List.rev_map snd (HintDN.find_all (find_base bas)) @@ -174,7 +174,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl = if cl.concl_occs != AllOccurrences && cl.concl_occs != NoOccurrences then - Proofview.tclZERO (UserError("" , str"The \"at\" syntax isn't available yet for the autorewrite tactic.")) + Tacticals.New.tclZEROMSG (str"The \"at\" syntax isn't available yet for the autorewrite tactic.") else let compose_tac t1 t2 = match cl.onhyps with @@ -204,7 +204,7 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl = *) gen_auto_multi_rewrite conds tac_main lbas cl | _ -> - Proofview.tclZERO (UserError ("autorewrite",strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.")) + Tacticals.New.tclZEROMSG (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.") (* Functions necessary to the library object declaration *) let cache_hintrewrite (_,(rbase,lrl)) = diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index 1f5177c3d..b87d65753 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -144,7 +144,7 @@ struct type t = Dn.t - let create = Dn.create + let empty = Dn.empty let add = function | None -> diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index 6c396b4c8..f29d18615 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -28,7 +28,7 @@ module Make : sig type t - val create : unit -> t + val empty : t val add : transparent_state option -> t -> (constr_pattern * Z.t) -> t val rmv : transparent_state option -> t -> (constr_pattern * Z.t) -> t diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 9b69481da..c03710e91 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -55,7 +55,7 @@ let contradiction_context = let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let rec seek_neg l = match l with - | [] -> Proofview.tclZERO (UserError ("" , Pp.str"No such contradiction")) + | [] -> Tacticals.New.tclZEROMSG (Pp.str"No such contradiction") | (id,_,typ)::rest -> let typ = nf_evar sigma typ in let typ = whd_betadeltaiota env sigma typ in @@ -107,7 +107,7 @@ let contradiction_term (c,lbind as cl) = Proofview.tclZERO Not_found end begin function (e, info) -> match e with - | Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction.")) + | Not_found -> Tacticals.New.tclZEROMSG (Pp.str"Not a contradiction.") | e -> Proofview.tclZERO ~info e end end diff --git a/tactics/dn.ml b/tactics/dn.ml index 3b1614d6c..aed2c2832 100644 --- a/tactics/dn.ml +++ b/tactics/dn.ml @@ -38,7 +38,7 @@ struct type t = Trie.t - let create () = Trie.empty + let empty = Trie.empty (* [path_of dna pat] returns the list of nodes of the pattern [pat] read in prefix ordering, [dna] is the function returning the main node of a pattern *) diff --git a/tactics/dn.mli b/tactics/dn.mli index 20407e9d9..2a60c3eb8 100644 --- a/tactics/dn.mli +++ b/tactics/dn.mli @@ -10,7 +10,7 @@ sig type t - val create : unit -> t + val empty : t (** [add t f (tree,inf)] adds a structured object [tree] together with the associated information [inf] to the table [t]; the function diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 607664486..bd55e6fb1 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -619,7 +619,7 @@ TACTIC EXTEND unify match table with | None -> let msg = str "Hint table " ++ str base ++ str " not found" in - Proofview.tclZERO (UserError ("", msg)) + Tacticals.New.tclZEROMSG msg | Some t -> let state = Hint_db.transparent_state t in unify ~state x y diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index c2cd9e47f..2ee4bf8e1 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -158,7 +158,7 @@ let solveEqBranch rectype = end end begin function (e, info) -> match e with - | PatternMatchingFailure -> Proofview.tclZERO (UserError ("",Pp.str"Unexpected conclusion!")) + | PatternMatchingFailure -> Tacticals.New.tclZEROMSG (Pp.str"Unexpected conclusion!") | e -> Proofview.tclZERO ~info e end @@ -186,7 +186,7 @@ let decideGralEquality = end begin function (e, info) -> match e with | PatternMatchingFailure -> - Proofview.tclZERO (UserError ("", Pp.str"The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}.")) + Tacticals.New.tclZEROMSG (Pp.str"The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}.") | e -> Proofview.tclZERO ~info e end diff --git a/tactics/equality.ml b/tactics/equality.ml index 7ab8d0c3b..f2860a230 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -306,8 +306,8 @@ let find_elim hdcncl lft2rgt dep cls ot gl = let _ = Global.lookup_constant c1' in c1' with Not_found -> - let rwr_thm = Label.to_string l' in - error ("Cannot find rewrite principle "^rwr_thm^".") + errorlabstrm "Equality.find_elim" + (str "Cannot find rewrite principle " ++ pr_label l' ++ str ".") end | _ -> destConstRef pr1 end @@ -454,7 +454,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl = (* Otherwise, if we are told to rewrite in all hypothesis via the syntax "* |-", we fail iff all the different rewrites fail *) let rec do_hyps_atleastonce = function - | [] -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Nothing to rewrite.")) + | [] -> tclZEROMSG (Pp.str"Nothing to rewrite.") | id :: l -> tclIFTHENTRYELSEMUST (general_rewrite_ebindings_in l2r AllOccurrences false true ?tac id c with_evars) @@ -874,7 +874,7 @@ let gen_absurdity id = then simplest_elim (mkVar id) else - Proofview.tclZERO (Errors.UserError ("Equality.gen_absurdity" , str "Not the negation of an equality.")) + tclZEROMSG (str "Not the negation of an equality.") end (* Precondition: eq is leibniz equality @@ -936,7 +936,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let concl = Proofview.Goal.concl gl in match find_positions env sigma t1 t2 with | Inr _ -> - Proofview.tclZERO (Errors.UserError ("discr" , str"Not a discriminable equality.")) + tclZEROMSG (str"Not a discriminable equality.") | Inl (cpath, (_,dirn), _) -> let sort = pf_apply get_type_of gl concl in discr_positions env sigma u eq_clause cpath dirn sort @@ -968,7 +968,7 @@ let onNegatedEquality with_evars tac = (onLastHypId (fun id -> onEquality with_evars tac (mkVar id,NoBindings))) | _ -> - Proofview.tclZERO (Errors.UserError ("" , str "Not a negated primitive equality.")) + tclZEROMSG (str "Not a negated primitive equality.") end let discrSimpleClause with_evars = function @@ -1303,7 +1303,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = in let injectors = List.map_filter filter posns in if List.is_empty injectors then - Proofview.tclZERO (Errors.UserError ("Equality.inj" , str "Failed to decompose the equality.")) + tclZEROMSG (str "Failed to decompose the equality.") else Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Proofview.tclBIND @@ -1319,12 +1319,12 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause = let env = eq_clause.env in match find_positions env sigma t1 t2 with | Inl _ -> - Proofview.tclZERO (Errors.UserError ("Inj",strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal.")) + tclZEROMSG (strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal.") | Inr [] -> let suggestion = if !injection_on_proofs then "" else " You can try to use option Set Injection On Proofs." in - Proofview.tclZERO (Errors.UserError ("Equality.inj",strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion))) + tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion)) | Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 -> - Proofview.tclZERO (Errors.UserError ("Equality.inj" , str"Nothing to inject.")) + tclZEROMSG (str"Nothing to inject.") | Inr posns -> inject_at_positions env sigma l2r u eq_clause posns (tac (clenv_value eq_clause)) @@ -1589,10 +1589,10 @@ let is_eq_x gl x (id,_,c) = erase hyp and x; proceed by generalizing all dep hyps *) let subst_one dep_proof_ok x (hyp,rhs,dir) = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let hyps = Proofview.Goal.hyps gl in - let concl = Proofview.Goal.concl gl in + let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in (* The set of hypotheses using x *) let dephyps = List.rev (snd (List.fold_right (fun (id,b,_ as dcl) (deps,allhyps) -> @@ -1663,24 +1663,45 @@ let default_subst_tactic_flags () = { only_leibniz = true; rewrite_dependent_proof = false } let subst_all ?(flags=default_subst_tactic_flags ()) () = - Proofview.Goal.nf_enter begin fun gl -> - let find_eq_data_decompose = find_eq_data_decompose gl in - let test (_,c) = - try - let lbeq,u,(_,x,y) = find_eq_data_decompose c in - let eq = Universes.constr_of_global_univ (lbeq.eq,u) in - if flags.only_leibniz then restrict_to_eq_and_identity eq; - (* J.F.: added to prevent failure on goal containing x=x as an hyp *) - if Term.eq_constr x y then failwith "caught"; - match kind_of_term x with Var x -> x | _ -> - match kind_of_term y with Var y -> y | _ -> failwith "caught" - with Constr_matching.PatternMatchingFailure -> failwith "caught" + + (* First step: find hypotheses to treat in linear time *) + let find_equations gl = + let gl = Proofview.Goal.assume gl in + let find_eq_data_decompose = find_eq_data_decompose gl in + let test (hyp,_,c) = + try + let lbeq,u,(_,x,y) = find_eq_data_decompose c in + let eq = Universes.constr_of_global_univ (lbeq.eq,u) in + if flags.only_leibniz then restrict_to_eq_and_identity eq; + (* J.F.: added to prevent failure on goal containing x=x as an hyp *) + if Term.eq_constr x y then None else + match kind_of_term x, kind_of_term y with + | Var _, _ | _, Var _ -> Some hyp + | _ -> None + with Constr_matching.PatternMatchingFailure -> None + in + let hyps = Proofview.Goal.hyps gl in + List.map_filter test hyps + in + + (* Second step: treat equations *) + let process hyp = + Proofview.Goal.enter begin fun gl -> + let gl = Proofview.Goal.assume gl in + let find_eq_data_decompose = find_eq_data_decompose gl in + let (_,_,c) = pf_get_hyp hyp gl in + let _,_,(_,x,y) = find_eq_data_decompose c in + (* J.F.: added to prevent failure on goal containing x=x as an hyp *) + if Term.eq_constr x y then Proofview.tclUNIT () else + match kind_of_term x, kind_of_term y with + | Var x, _ -> subst_one flags.rewrite_dependent_proof x (hyp,y,true) + | _, Var y -> subst_one flags.rewrite_dependent_proof y (hyp,x,false) + | _ -> Proofview.tclUNIT () + end in - let test p = try Some (test p) with Failure _ -> None in - let hyps = pf_hyps_types gl in - let ids = List.map_filter test hyps in - let ids = List.uniquize ids in - subst_gen flags.rewrite_dependent_proof ids + Proofview.Goal.nf_enter begin fun gl -> + let ids = find_equations gl in + tclMAP process ids end (* Rewrite the first assumption for which a condition holds diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 891e2dba5..f217cda89 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -750,7 +750,7 @@ let rec find_a_destructable_match t = let destauto t = try find_a_destructable_match t; - Proofview.tclZERO (UserError ("", str"No destructable match found")) + Tacticals.New.tclZEROMSG (str "No destructable match found") with Found tac -> tac let destauto_in id = @@ -772,7 +772,7 @@ END let eq_constr x y = Proofview.Goal.enter (fun gl -> let evd = Proofview.Goal.sigma gl in - if Evd.eq_constr_univs_test evd x y then Proofview.tclUNIT () + if Evarutil.eq_constr_univs_test evd evd x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal")) TACTIC EXTEND constr_eq @@ -966,7 +966,7 @@ let guard tst = Proofview.tclUNIT () else let msg = Pp.(str"Condition not satisfied:"++ws 1++(pr_itest tst)) in - Proofview.tclZERO (Errors.UserError("guard",msg)) + Tacticals.New.tclZEROMSG msg TACTIC EXTEND guard diff --git a/tactics/hints.ml b/tactics/hints.ml index dea47794e..f83aa5601 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -171,7 +171,7 @@ type search_entry = { let empty_se = { sentry_nopat = []; sentry_pat = []; - sentry_bnet = Bounded_net.create (); + sentry_bnet = Bounded_net.empty; sentry_mode = []; } @@ -206,7 +206,7 @@ let rebuild_dn st se = let dn' = List.fold_left (fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t))) - (Bounded_net.create ()) se.sentry_pat + Bounded_net.empty se.sentry_pat in { se with sentry_bnet = dn' } @@ -394,7 +394,7 @@ module Hint_db = struct hintdb_state : Names.transparent_state; hintdb_cut : hints_path; hintdb_unfolds : Id.Set.t * Cset.t; - mutable hintdb_max_id : int; + hintdb_max_id : int; use_dn : bool; hintdb_map : search_entry Constr_map.t; (* A list of unindexed entries starting with an unfoldable constant @@ -402,8 +402,9 @@ module Hint_db = struct hintdb_nopat : (global_reference option * stored_data) list } - let next_hint_id t = - let h = t.hintdb_max_id in t.hintdb_max_id <- succ t.hintdb_max_id; h + let next_hint_id db = + let h = db.hintdb_max_id in + { db with hintdb_max_id = succ db.hintdb_max_id }, h let empty st use_dn = { hintdb_state = st; hintdb_cut = PathEmpty; @@ -510,8 +511,9 @@ module Hint_db = struct state, { db with hintdb_unfolds = unfs }, true | _ -> db.hintdb_state, db, false in - let db = if db.use_dn && rebuild then rebuild_db st' db else db - in addkv k (next_hint_id db) v db + let db = if db.use_dn && rebuild then rebuild_db st' db else db in + let db, id = next_hint_id db in + addkv k id v db let add_list l db = List.fold_left (fun db k -> add_one k db) db l @@ -596,7 +598,7 @@ let current_pure_db () = List.map snd (Hintdbmap.bindings (Hintdbmap.remove "v62" !searchtable)) let error_no_such_hint_database x = - error ("No such Hint database: "^x^".") + errorlabstrm "Hints" (str "No such Hint database: " ++ str x ++ str ".") (**************************************************************************) (* Definition of the summary *) diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index ac8b4923e..60ce0e0dc 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -52,7 +52,7 @@ let try_find_global_reference dir s = let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in try Nametab.global_of_path sp with Not_found -> - anomaly (str ("Global reference " ^ s ^ " not found in generalized rewriting")) + anomaly (str "Global reference " ++ str s ++ str " not found in generalized rewriting") let find_reference dir s = let gr = lazy (try_find_global_reference dir s) in diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index 53f3f5652..e8cb8c63b 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -43,7 +43,7 @@ end module MLTacMap = Map.Make(MLName) let pr_tacname t = - t.mltac_plugin ^ "::" ^ t.mltac_tactic + str t.mltac_plugin ++ str "::" ++ str t.mltac_tactic let tac_tab = ref MLTacMap.empty @@ -52,9 +52,9 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic array) = if MLTacMap.mem s !tac_tab then if overwrite then let () = tac_tab := MLTacMap.remove s !tac_tab in - msg_warning (str ("Overwriting definition of tactic " ^ pr_tacname s)) + msg_warning (str "Overwriting definition of tactic " ++ pr_tacname s) else - Errors.anomaly (str ("Cannot redeclare tactic " ^ pr_tacname s ^ ".")) + Errors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s ++ str ".") in tac_tab := MLTacMap.add s t !tac_tab @@ -65,7 +65,7 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } = tacs.(i) with Not_found -> Errors.errorlabstrm "" - (str "The tactic " ++ str (pr_tacname s) ++ str " is not installed.") + (str "The tactic " ++ pr_tacname s ++ str " is not installed.") (***************************************************************************) (* Tactic registration *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index f29680e18..7ce158fd1 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1040,8 +1040,8 @@ let read_pattern lfun ist env sigma = function let cons_and_check_name id l = if Id.List.mem id l then user_err_loc (dloc,"read_match_goal_hyps", - strbrk ("Hypothesis pattern-matching variable "^(Id.to_string id)^ - " used twice in the same pattern.")) + str "Hypothesis pattern-matching variable " ++ pr_id id ++ + str " used twice in the same pattern.") else id::l let rec read_match_goal_hyps lfun ist env sigma lidh = function @@ -1492,11 +1492,11 @@ and tactic_of_value ist vle = extra = TacStore.set ist.extra f_trace []; } in let tac = name_if_glob appl (eval_tactic ist t) in catch_error_tac trace tac - | (VFun _|VRec _) -> Proofview.tclZERO (UserError ("" , str "A fully applied tactic is expected.")) + | (VFun _|VRec _) -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.") else if has_type vle (topwit wit_tactic) then let tac = out_gen (topwit wit_tactic) vle in eval_tactic ist tac - else Proofview.tclZERO (UserError ("" , str"Expression does not evaluate to a tactic.")) + else Tacticals.New.tclZEROMSG (str "Expression does not evaluate to a tactic.") (* Interprets the clauses of a recursive LetIn *) and interp_letrec ist llc u = @@ -1752,10 +1752,8 @@ and interp_ltac_constr ist e : constr Ftactic.t = Ftactic.return cresult with CannotCoerceTo _ -> let env = Proofview.Goal.env gl in - Proofview.tclZERO (UserError ( "", - errorlabstrm "" - (str "Must evaluate to a closed term" ++ fnl() ++ - str "offending expression: " ++ fnl() ++ pr_inspect env e result))) + Tacticals.New.tclZEROMSG (str "Must evaluate to a closed term" ++ fnl() ++ + str "offending expression: " ++ fnl() ++ pr_inspect env e result) end diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 9b16fe3f7..5ba53a764 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -420,7 +420,7 @@ module New = struct (* Try the first tactic that does not fail in a list of tactics *) let rec tclFIRST = function - | [] -> tclZERO (Errors.UserError ("Tacticals.New.tclFIRST",str"No applicable tactic.")) + | [] -> tclZEROMSG (str"No applicable tactic.") | t::rest -> tclORELSE0 t (tclFIRST rest) let rec tclFIRST_PROGRESS_ON tac = function @@ -430,10 +430,7 @@ module New = struct let rec tclDO n t = if n < 0 then - tclZERO (Errors.UserError ( - "Refiner.tclDO", - str"Wrong argument : Do needs a positive integer.") - ) + tclZEROMSG (str"Wrong argument : Do needs a positive integer.") else if n = 0 then tclUNIT () else if n = 1 then t else tclTHEN t (tclDO (n-1) t) @@ -456,7 +453,7 @@ module New = struct let tclCOMPLETE t = t >>= fun res -> (tclINDEPENDENT - (tclZERO (Errors.UserError ("",str"Proof is not complete."))) + (tclZEROMSG (str"Proof is not complete.")) ) <*> tclUNIT res @@ -618,7 +615,8 @@ module New = struct | Var id -> string_of_id id | _ -> "\b" in - error ("The elimination combinator " ^ name_elim ^ " is unknown.") + errorlabstrm "Tacticals.general_elim_then_using" + (str "The elimination combinator " ++ str name_elim ++ str " is unknown.") in let elimclause' = clenv_fchain indmv elimclause indclause in let branchsigns = compute_construtor_signatures isrec ind in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 7484139c6..3038a9506 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -139,7 +139,8 @@ let introduction ?(check=true) id = let store = Proofview.Goal.extra gl in let env = Proofview.Goal.env gl in let () = if check && mem_named_context id hyps then - error ("Variable " ^ Id.to_string id ^ " is already declared.") + errorlabstrm "Tactics.introduction" + (str "Variable " ++ pr_id id ++ str " is already declared.") in match kind_of_term (whd_evar sigma concl) with | Prod (_, t, b) -> unsafe_intro env store (id, None, t) b @@ -751,8 +752,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = (intro_then_gen name_flag move_flag false dep_flag tac)) begin function (e, info) -> match e with | RefinerError IntroNeedsProduct -> - Proofview.tclZERO - (Errors.UserError("Intro",str "No product even after head-reduction.")) + Tacticals.New.tclZEROMSG (str "No product even after head-reduction.") | e -> Proofview.tclZERO ~info e end end @@ -1358,7 +1358,7 @@ let make_projection env sigma params cstr sign elim i n c u = | None -> None in elim -let descend_in_conjunctions avoid tac exit c = +let descend_in_conjunctions avoid tac (err, info) c = Proofview.Goal.nf_enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in @@ -1392,9 +1392,8 @@ let descend_in_conjunctions avoid tac exit c = (* Might be ill-typed due to forbidden elimination. *) Tacticals.New.onLastHypId (tac (not isrec))] end)) - | None -> - raise Exit - with RefinerError _|UserError _|Exit -> exit () + | None -> Proofview.tclZERO ~info err + with RefinerError _|UserError _ -> Proofview.tclZERO ~info err end (****************************************************) @@ -1417,7 +1416,15 @@ let solve_remaining_apply_goals = with Not_found -> Proofview.tclUNIT () else Proofview.tclUNIT () end - + +let tclORELSEOPT t k = + Proofview.tclORELSE t + (fun e -> match k e with + | None -> + let (e, info) = e in + Proofview.tclZERO ~info e + | Some tac -> tac) + let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) = Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in @@ -1442,50 +1449,46 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) with UserError _ as exn -> Proofview.tclZERO exn in - Proofview.tclORELSE + let rec try_red_apply thm_ty (exn0, info) = + try + (* Try to head-reduce the conclusion of the theorem *) + let red_thm = try_red_product env sigma thm_ty in + tclORELSEOPT + (try_apply red_thm concl_nprod) + (function (e, info) -> match e with + | PretypeError _|RefinerError _|UserError _|Failure _ -> + Some (try_red_apply red_thm (exn0, info)) + | _ -> None) + with Redelimination -> + (* Last chance: if the head is a variable, apply may try + second order unification *) + let info = Loc.add_loc info loc in + let tac = + if with_destruct then + descend_in_conjunctions [] + (fun b id -> + Tacticals.New.tclTHEN + (try_main_apply b (mkVar id)) + (Proofview.V82.tactic (thin [id]))) + (exn0, info) c + else + Proofview.tclZERO ~info exn0 in + if not (Int.equal concl_nprod 0) then + tclORELSEOPT + (try_apply thm_ty 0) + (function (e, info) -> match e with + | PretypeError _|RefinerError _|UserError _|Failure _-> + Some tac + | _ -> None) + else + tac + in + tclORELSEOPT (try_apply thm_ty0 concl_nprod) (function (e, info) -> match e with - | PretypeError _|RefinerError _|UserError _|Failure _ as exn0 -> - let rec try_red_apply thm_ty = - try - (* Try to head-reduce the conclusion of the theorem *) - let red_thm = try_red_product env sigma thm_ty in - Proofview.tclORELSE - (try_apply red_thm concl_nprod) - (function (e, info) -> match e with - | PretypeError _|RefinerError _|UserError _|Failure _ -> - try_red_apply red_thm - | exn -> iraise (exn, info)) - with Redelimination -> - (* Last chance: if the head is a variable, apply may try - second order unification *) - let tac = - if with_destruct then - descend_in_conjunctions [] - (fun b id -> - Tacticals.New.tclTHEN - (try_main_apply b (mkVar id)) - (Proofview.V82.tactic (thin [id]))) - (fun _ -> - let info = Loc.add_loc info loc in - Proofview.tclZERO ~info exn0) c - else - let info = Loc.add_loc info loc in - Proofview.tclZERO ~info exn0 in - if not (Int.equal concl_nprod 0) then - try - Proofview.tclORELSE - (try_apply thm_ty 0) - (function (e, info) -> match e with - | PretypeError _|RefinerError _|UserError _|Failure _-> - tac - | exn -> iraise (exn, info)) - with UserError _ | Exit -> - tac - else - tac - in try_red_apply thm_ty0 - | exn -> iraise (exn, info)) + | PretypeError _|RefinerError _|UserError _|Failure _ -> + Some (try_red_apply thm_ty0 (e, info)) + | _ -> None) end in Tacticals.New.tclTHENLIST [ @@ -1596,10 +1599,10 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming tac id ]) with e when with_destruct && Errors.noncritical e -> - let e = Errors.push e in + let (e, info) = Errors.push e in (descend_in_conjunctions [targetid] (fun b id -> aux (id::idstoclear) b (mkVar id)) - (fun _ -> iraise e) c) + (e, info) c) end in aux [] with_destruct d @@ -1871,8 +1874,8 @@ let check_number_of_constructors expctdnumopt i nconstr = if Int.equal i 0 then error "The constructors are numbered starting from 1."; begin match expctdnumopt with | Some n when not (Int.equal n nconstr) -> - error ("Not an inductive goal with "^ - string_of_int n ^ String.plural n " constructor"^".") + errorlabstrm "Tactics.check_number_of_constructors" + (str "Not an inductive goal with " ++ int n ++ str (String.plural n " constructor") ++ str ".") | _ -> () end; if i > nconstr then error "Not enough constructors." @@ -3043,7 +3046,7 @@ let make_up_names n ind_opt cname = let error_ind_scheme s = let s = if not (String.is_empty s) then s^" " else s in - error ("Cannot recognize "^s^"an induction scheme.") + errorlabstrm "Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.") let glob = Universes.constr_of_global diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index e6f33a47b..59c579237 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -318,7 +318,7 @@ let tauto_intuitionistic flags = (intuition_gen (default_ist ()) flags <:tactic<fail>>) begin function (e, info) -> match e with | Refiner.FailError _ | UserError _ -> - Proofview.tclZERO (UserError ("tauto" , str "tauto failed.")) + Tacticals.New.tclZEROMSG (str "tauto failed.") | e -> Proofview.tclZERO ~info e end @@ -330,7 +330,7 @@ let tauto_classical flags nnpp = Proofview.tclORELSE (Tacticals.New.tclTHEN (apply nnpp) (tauto_intuitionistic flags)) begin function (e, info) -> match e with - | UserError _ -> Proofview.tclZERO (UserError ("tauto" , str "Classical tauto failed.")) + | UserError _ -> Tacticals.New.tclZEROMSG (str "Classical tauto failed.") | e -> Proofview.tclZERO ~info e end diff --git a/test-suite/bugs/opened/3593.v b/test-suite/bugs/closed/3593.v index d83b90060..378db6857 100644 --- a/test-suite/bugs/opened/3593.v +++ b/test-suite/bugs/closed/3593.v @@ -5,6 +5,6 @@ Record prod A B := pair { fst : A ; snd : B }. Goal forall x : prod Set Set, let f := @fst _ in f _ x = @fst _ _ x. simpl; intros. constr_eq (@fst Set Set x) (fst (A := Set) (B := Set) x). - Fail Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x). + Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x). reflexivity. Qed. diff --git a/test-suite/bugs/closed/4190.v b/test-suite/bugs/closed/4190.v new file mode 100644 index 000000000..2843488ba --- /dev/null +++ b/test-suite/bugs/closed/4190.v @@ -0,0 +1,15 @@ +Module Type A . + Tactic Notation "bar" := idtac "ITSME". +End A. + +Module Type B. + Tactic Notation "foo" := fail "NOTME". +End B. + +Module Type C := A <+ B. + +Module Type F (Import M : C). + +Lemma foo : True. +Proof. +bar. diff --git a/test-suite/bugs/closed/4191.v b/test-suite/bugs/closed/4191.v new file mode 100644 index 000000000..290bb384d --- /dev/null +++ b/test-suite/bugs/closed/4191.v @@ -0,0 +1,5 @@ +(* Test maximal implicit arguments in the presence of let-ins *) +Definition foo (x := 1) {y : nat} (H : y = y) : True := I. +Definition bar {y : nat} (x := 1) (H : y = y) : True := I. +Check bar (eq_refl 1). +Check foo (eq_refl 1). diff --git a/test-suite/bugs/closed/4193.v b/test-suite/bugs/closed/4193.v new file mode 100644 index 000000000..885d04a92 --- /dev/null +++ b/test-suite/bugs/closed/4193.v @@ -0,0 +1,7 @@ +Module Type E. +End E. + +Module Type A (M : E). +End A. + +Fail Module Type F (Import X : A). diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v new file mode 100644 index 000000000..ef991365d --- /dev/null +++ b/test-suite/bugs/closed/4198.v @@ -0,0 +1,13 @@ +Require Import List. +Open Scope list_scope. +Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'), + let k := + (match H in (_ = y) return x = hd x y with + | eq_refl => eq_refl + end : x = x') + in k = k. + simpl. + intros. + match goal with + | [ |- appcontext G[@hd] ] => idtac + end. diff --git a/test-suite/bugs/closed/4214.v b/test-suite/bugs/closed/4214.v new file mode 100644 index 000000000..cd53c898e --- /dev/null +++ b/test-suite/bugs/closed/4214.v @@ -0,0 +1,5 @@ +(* Check that subst uses all equations around *) +Goal forall A (a b c : A), b = a -> b = c -> a = c. +intros. +subst. +reflexivity. diff --git a/test-suite/bugs/closed/4217.v b/test-suite/bugs/closed/4217.v new file mode 100644 index 000000000..19973f30a --- /dev/null +++ b/test-suite/bugs/closed/4217.v @@ -0,0 +1,6 @@ +(* Checking correct index of implicit by pos in fixpoints *) + +Fixpoint ith_default + {default_A : nat} + {As : list nat} + {struct As} : Set. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 1783085fc..c34bbd56e 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -2276,7 +2276,7 @@ Section ForallPairs. Proof. induction 1. inversion 1. - simpl; destruct 1; destruct 1; repeat subst; auto. + simpl; destruct 1; destruct 1; subst; auto. right; left. apply -> Forall_forall; eauto. right; right. apply -> Forall_forall; eauto. Qed. diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index b5d0d2281..11b4b3732 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -299,7 +299,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in printf "find %s/%s -maxdepth 0 -and -empty -exec rmdir -p \\{\\} \\;\\n' >> \"$@\"\n" dir kind in printf "uninstall_me.sh: %s\n" !makefile_name; - print "\techo '#!/bin/sh' > $@ \n"; + print "\techo '#!/bin/sh' > $@\n"; if (not_empty cmxsfiles) then uninstall_by_root where_what_cmxs; uninstall_by_root where_what_oth; if not_empty vfiles then uninstall_one_kind "html" doc_dir; @@ -496,7 +496,7 @@ endif\n"; print "\n" let parameters () = - print ".DEFAULT_GOAL := all\n\n# \n"; + print ".DEFAULT_GOAL := all\n\n"; print "# This Makefile may take arguments passed as environment variables:\n"; print "# COQBIN to specify the directory where Coq binaries resides;\n"; print "# TIMECMD set a command to log .v compilation time;\n"; diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 7d8199ab3..9b7845b09 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -122,10 +122,8 @@ let error_cannot_parse s (i,j) = exit 1 let warning_module_notfound f s = - eprintf "*** Warning: in file %s, library " f; - eprintf "%s.v is required and has not been found in the loadpath!\n" - (String.concat "." s); - flush stderr + eprintf "*** Warning: in file %s, library %s is required and has not been found in the loadpath!\n%!" + f (String.concat "." s) let warning_notfound f s = eprintf "*** Warning: in file %s, the file " f; diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 26b54a73e..96bb89e2a 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -19,6 +19,7 @@ open Termops open Declarations open Names open Globnames +open Nameops open Inductiveops open Tactics open Ind_tables @@ -338,7 +339,8 @@ let do_replace_lb lb_scheme_key aavoid narg p q = let rec find i = if Id.equal avoid.(n-i) s then avoid.(n-i-x) else (if i<n then find (i+1) - else error ("Var "^(Id.to_string s)^" seems unknown.") + else errorlabstrm "AutoIndDecl.do_replace_lb" + (str "Var " ++ pr_id s ++ str " seems unknown.") ) in mkVar (find 1) with e when Errors.noncritical e -> @@ -369,7 +371,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q = Printer.pr_constr type_of_pq ++ str " first.") in - Proofview.tclZERO (Errors.UserError("",err_msg)) + Tacticals.New.tclZEROMSG err_msg in lb_type_of_p >>= fun (lb_type_of_p,eff) -> let lb_args = Array.append (Array.append @@ -395,7 +397,8 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = let rec find i = if Id.equal avoid.(n-i) s then avoid.(n-i-x) else (if i<n then find (i+1) - else error ("Var "^(Id.to_string s)^" seems unknown.") + else errorlabstrm "AutoIndDecl.do_replace_bl" + (str "Var " ++ pr_id s ++ str " seems unknown.") ) in mkVar (find 1) with e when Errors.noncritical e -> @@ -456,28 +459,28 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = ) end | ([],[]) -> Proofview.tclUNIT () - | _ -> Proofview.tclZERO (UserError ("" , str"Both side of the equality must have the same arity.")) + | _ -> Tacticals.New.tclZEROMSG (str "Both side of the equality must have the same arity.") in begin try Proofview.tclUNIT (destApp lft) - with DestKO -> Proofview.tclZERO (UserError ("" , str"replace failed.")) + with DestKO -> Tacticals.New.tclZEROMSG (str "replace failed.") end >>= fun (ind1,ca1) -> begin try Proofview.tclUNIT (destApp rgt) - with DestKO -> Proofview.tclZERO (UserError ("" , str"replace failed.")) + with DestKO -> Tacticals.New.tclZEROMSG (str "replace failed.") end >>= fun (ind2,ca2) -> begin try Proofview.tclUNIT (out_punivs (destInd ind1)) with DestKO -> begin try Proofview.tclUNIT (fst (fst (destConstruct ind1))) - with DestKO -> Proofview.tclZERO (UserError ("" , str"The expected type is an inductive one.")) + with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.") end end >>= fun (sp1,i1) -> begin try Proofview.tclUNIT (out_punivs (destInd ind2)) with DestKO -> begin try Proofview.tclUNIT (fst (fst (destConstruct ind2))) - with DestKO -> Proofview.tclZERO (UserError ("" , str"The expected type is an inductive one.")) + with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.") end end >>= fun (sp2,i2) -> if not (eq_mind sp1 sp2) || not (Int.equal i1 i2) - then Proofview.tclZERO (UserError ("" , str"Eq should be on the same type")) + then Tacticals.New.tclZEROMSG (str "Eq should be on the same type") else aux (Array.to_list ca1) (Array.to_list ca2) (* @@ -502,8 +505,8 @@ let eqI ind l = (List.map (fun (_,seq,_,_)-> mkVar seq) list_id )) and e, eff = try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff - with Not_found -> error - ("The boolean equality on "^(string_of_mind (fst ind))^" is needed."); + with Not_found -> errorlabstrm "AutoIndDecl.eqI" + (str "The boolean equality on " ++ pr_mind (fst ind) ++ str " is needed."); in (if Array.equal eq_constr eA [||] then e else mkApp(e,eA)), eff (**********************************************************************) @@ -610,10 +613,10 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). (ca.(1))) Auto.default_auto else - Proofview.tclZERO (UserError ("",str"Failure while solving Boolean->Leibniz.")) - | _ -> Proofview.tclZERO (UserError ("", str"Failure while solving Boolean->Leibniz.")) + Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.") + | _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.") ) - | _ -> Proofview.tclZERO (UserError ("", str"Failure while solving Boolean->Leibniz.")) + | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.") end ] @@ -733,10 +736,10 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec = nparrec ca'.(n-2) ca'.(n-1) | _ -> - Proofview.tclZERO (UserError ("",str"Failure while solving Leibniz->Boolean.")) + Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.") ) | _ -> - Proofview.tclZERO (UserError ("",str"Failure while solving Leibniz->Boolean.")) + Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.") end ] end @@ -856,15 +859,13 @@ let compute_dec_tact ind lnamesparrec nparrec = let c, eff = find_scheme bl_scheme_kind ind in Proofview.tclUNIT (mkConst c,eff) with Not_found -> - Proofview.tclZERO (UserError ("",str"Error during the decidability part, boolean to leibniz"++ - str" equality is required.")) + Tacticals.New.tclZEROMSG (str "Error during the decidability part, boolean to leibniz equality is required.") end >>= fun (blI,eff') -> begin try let c, eff = find_scheme lb_scheme_kind ind in Proofview.tclUNIT (mkConst c,eff) with Not_found -> - Proofview.tclZERO (UserError ("",str"Error during the decidability part, leibniz to boolean"++ - str" equality is required.")) + Tacticals.New.tclZEROMSG (str "Error during the decidability part, leibniz to boolean equality is required.") end >>= fun (lbI,eff'') -> let eff = (Declareops.union_side_effects eff'' (Declareops.union_side_effects eff' eff)) in Tacticals.New.tclTHENLIST [ diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index b29ba1efc..a0892bed9 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -20,7 +20,7 @@ let print_loc loc = let loc = Loc.unloc loc in (int (fst loc) ++ str"-" ++ int (snd loc)) -let guill s = "\""^s^"\"" +let guill s = str "\"" ++ str s ++ str "\"" (** Invariant : exceptions embedded in EvaluatedError satisfy Errors.noncritical *) @@ -33,10 +33,10 @@ exception EvaluatedError of std_ppcmds * exn option let explain_exn_default = function (* Basic interaction exceptions *) - | Stream.Error txt -> hov 0 (str ("Syntax error: " ^ txt ^ ".")) - | Compat.Token.Error txt -> hov 0 (str ("Syntax error: " ^ txt ^ ".")) + | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") + | Compat.Token.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".") | Lexer.Error.E err -> hov 0 (str (Lexer.Error.to_string err)) - | Sys_error msg -> hov 0 (str ("System error: " ^ guill msg)) + | Sys_error msg -> hov 0 (str "System error: " ++ guill msg) | Out_of_memory -> hov 0 (str "Out of memory.") | Stack_overflow -> hov 0 (str "Stack overflow.") | Timeout -> hov 0 (str "Timeout!") diff --git a/toplevel/command.ml b/toplevel/command.ml index 754ad8526..1249581ee 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -609,8 +609,7 @@ let declare_mutual_inductive_with_eliminations mie impls = begin match mie.mind_entry_finite with | BiFinite when is_recursive mie -> if Option.has_some mie.mind_entry_record then - error ("Records declared with the keywords Record or Structure cannot be recursive." ^ - "You can, however, define recursive records using the Inductive or CoInductive command.") + error "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command." else error ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.") | _ -> () @@ -697,19 +696,19 @@ let rec partial_order cmp = function let non_full_mutual_message x xge y yge isfix rest = let reason = if Id.List.mem x yge then - Id.to_string y^" depends on "^Id.to_string x^" but not conversely" + pr_id y ++ str " depends on " ++ pr_id x ++ str " but not conversely" else if Id.List.mem y xge then - Id.to_string x^" depends on "^Id.to_string y^" but not conversely" + pr_id x ++ str " depends on " ++ pr_id y ++ str " but not conversely" else - Id.to_string y^" and "^Id.to_string x^" are not mutually dependent" in - let e = if List.is_empty rest then reason else "e.g.: "^reason in + pr_id y ++ str " and " ++ pr_id x ++ str " are not mutually dependent" in + let e = if List.is_empty rest then reason else str "e.g., " ++ reason in let k = if isfix then "fixpoint" else "cofixpoint" in let w = if isfix - then strbrk "Well-foundedness check may fail unexpectedly." ++ fnl() + then str "Well-foundedness check may fail unexpectedly." ++ fnl() else mt () in - strbrk ("Not a fully mutually defined "^k) ++ fnl () ++ - strbrk ("("^e^").") ++ fnl () ++ w + str "Not a fully mutually defined " ++ str k ++ fnl () ++ + str "(" ++ e ++ str ")." ++ fnl () ++ w let check_mutuality env isfix fixl = let names = List.map fst fixl in @@ -734,7 +733,7 @@ type structured_fixpoint_expr = { let interp_fix_context env evdref isfix fix = let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in let impl_env, ((env', ctx), imps) = interp_context_evars env evdref before in - let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env env' evdref after in + let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env ~shift:(List.length before) env' evdref after in let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot) diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 3385d67e3..f0cac72d0 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -57,11 +57,6 @@ let load_rcfile() = else Flags.if_verbose msg_info (str"Skipping rcfile loading.") -(* Puts dir in the path of ML and in the LoadPath *) -let coq_add_path unix_path s = - Mltop.add_rec_path ~unix_path ~coq_root:(Names.DirPath.make [Nameops.coq_root;Names.Id.of_string s]) ~implicit:true; - Mltop.add_ml_dir unix_path - (* Recursively puts dir in the LoadPath if -nois was not passed *) let add_stdlib_path ~unix_path ~coq_root ~with_ml = Mltop.add_rec_path ~unix_path ~coq_root ~implicit:(!Flags.load_init); @@ -88,10 +83,11 @@ let init_load_path () = let coq_root = Names.DirPath.make [Nameops.coq_root] in (* NOTE: These directories are searched from last to first *) (* first, developer specific directory to open *) - if Coq_config.local then coq_add_path (coqlib/"dev") "dev"; + if Coq_config.local then + Mltop.add_ml_dir (coqlib/"dev"); (* main loops *) if Coq_config.local || !Flags.boot then begin - let () = Mltop.add_ml_dir (coqlib/"stm") in + Mltop.add_ml_dir (coqlib/"stm"); Mltop.add_ml_dir (coqlib/"ide") end; Mltop.add_ml_dir (coqlib/"toploop"); @@ -138,6 +134,6 @@ let get_compat_version = function | "8.3" -> Flags.V8_3 | "8.2" -> Flags.V8_2 | ("8.1" | "8.0") as s -> - msg_warning (strbrk ("Compatibility with version "^s^" not supported.")); + msg_warning (str "Compatibility with version " ++ str s ++ str " not supported."); Flags.V8_2 - | s -> Errors.error ("Unknown compatibility version \""^s^"\".") + | s -> Errors.errorlabstrm "get_compat_version" (str "Unknown compatibility version \"" ++ str s ++ str "\".") diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 52fa9e01e..caaf8054b 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -176,7 +176,7 @@ let print_location_in_file {outer=s;inner=fname} loc = try let (line, bol) = line_of_pos 1 0 0 in hov 0 (* No line break so as to follow emacs error message format *) - (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ + (errstrm ++ str"File " ++ str "\"" ++ str fname ++ str "\"" ++ str", line " ++ int line ++ str", characters " ++ Cerrors.print_loc (Loc.make_loc (bp-bol,ep-bol))) ++ str":" ++ fnl () diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 1544fd869..ca379cb7e 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -38,7 +38,7 @@ let get_version_date () = let print_header () = let (ver,rev) = get_version_date () in - ppnl (str ("Welcome to Coq "^ver^" ("^rev^")")); + ppnl (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); pp_flush () let warning s = msg_warning (strbrk s) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 5429e6608..ac8ca3a11 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -872,11 +872,11 @@ let explain_not_match_error = function quote (Univ.pr_constraints (Evd.pr_evd_level Evd.empty) cst) let explain_signature_mismatch l spec why = - str "Signature components for label " ++ str (Label.to_string l) ++ + str "Signature components for label " ++ pr_label l ++ str " do not match:" ++ spc () ++ explain_not_match_error why ++ str "." let explain_label_already_declared l = - str ("The label "^Label.to_string l^" is already declared.") + str "The label " ++ pr_label l ++ str " is already declared." let explain_application_to_not_path _ = strbrk "A module cannot be applied to another module application or " ++ @@ -1170,18 +1170,18 @@ let explain_bad_constructor env cstr ind = str "is expected." let decline_string n s = - if Int.equal n 0 then "no "^s^"s" - else if Int.equal n 1 then "1 "^s - else (string_of_int n^" "^s^"s") + if Int.equal n 0 then str "no " ++ str s ++ str "s" + else if Int.equal n 1 then str "1 " ++ str s + else (int n ++ str " " ++ str s ++ str "s") let explain_wrong_numarg_constructor env cstr n = str "The constructor " ++ pr_constructor env cstr ++ str " (in type " ++ pr_inductive env (inductive_of_constructor cstr) ++ - str ") expects " ++ str (decline_string n "argument") ++ str "." + str ") expects " ++ decline_string n "argument" ++ str "." let explain_wrong_numarg_inductive env ind n = str "The inductive type " ++ pr_inductive env ind ++ - str " expects " ++ str (decline_string n "argument") ++ str "." + str " expects " ++ decline_string n "argument" ++ str "." let explain_unused_clause env pats = (* Without localisation diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 138e5189a..0d39466ed 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -23,6 +23,7 @@ open Util open Declare open Entries open Decl_kinds +open Pp (**********************************************************************) (* Registering schemes in the environment *) @@ -87,7 +88,8 @@ let declare_scheme_object s aux f = try let _ = Hashtbl.find scheme_object_table key in (* let aux_msg = if aux="" then "" else " (with key "^aux^")" in*) - error ("Scheme object "^key^" already declared.") + errorlabstrm "IndTables.declare_scheme_object" + (str "Scheme object " ++ str key ++ str " already declared.") with Not_found -> Hashtbl.add scheme_object_table key (s,f); key diff --git a/toplevel/locality.ml b/toplevel/locality.ml index f711dad94..1145a20bb 100644 --- a/toplevel/locality.ml +++ b/toplevel/locality.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Pp + (** * Managing locality *) let local_of_bool = function @@ -16,7 +18,8 @@ let check_locality locality_flag = match locality_flag with | Some b -> let s = if b then "Local" else "Global" in - Errors.error ("This command does not support the \""^s^"\" prefix.") + Errors.errorlabstrm "Locality.check_locality" + (str "This command does not support the \"" ++ str s ++ str "\" prefix.") | None -> () (** Extracting the locality flag *) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 75e836922..deffb4fe5 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -62,11 +62,19 @@ let rec make_tags = function | [] -> [] let make_fresh_key = - let id = Summary.ref ~name:"Tactic Notation counter" 0 in - fun () -> KerName.make - (Safe_typing.current_modpath (Global.safe_env ())) - (Global.current_dirpath ()) - (incr id; Label.make ("_" ^ string_of_int !id)) + let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in + fun () -> + let cur = incr id; !id in + let lbl = Id.of_string ("_" ^ string_of_int cur) in + let kn = Lib.make_kn lbl in + let (mp, dir, _) = KerName.repr kn in + (** We embed the full path of the kernel name in the label so that the + identifier should be unique. This ensures that including two modules + together won't confuse the corresponding labels. *) + let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i" + (ModPath.to_string mp) (DirPath.to_string dir) cur) + in + KerName.make mp dir (Label.of_id lbl) type tactic_grammar_obj = { tacobj_key : KerName.t; @@ -381,7 +389,8 @@ let rec find_pattern nt xl = function | _, Break s :: _ | Break s :: _, _ -> error ("A break occurs on one side of \"..\" but not on the other side.") | _, Terminal s :: _ | Terminal s :: _, _ -> - error ("The token \""^s^"\" occurs on one side of \"..\" but not on the other side.") + errorlabstrm "Metasyntax.find_pattern" + (str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.") | _, [] -> error msg_expected_form_of_recursive_notation | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) -> @@ -442,7 +451,8 @@ let rec get_notation_vars = function let vars = get_notation_vars sl in if Id.equal id ldots_var then vars else if Id.List.mem id vars then - error ("Variable "^Id.to_string id^" occurs more than once.") + errorlabstrm "Metasyntax.get_notation_vars" + (str "Variable " ++ pr_id id ++ str " occurs more than once.") else id::vars | (Terminal _ | Break _) :: sl -> get_notation_vars sl @@ -455,8 +465,8 @@ let analyze_notation_tokens l = recvars, List.subtract Id.equal vars (List.map snd recvars), l let error_not_same_scope x y = - error ("Variables "^Id.to_string x^" and "^Id.to_string y^ - " must be in the same scope.") + errorlabstrm "Metasyntax.error_not_name_scope" + (str "Variables " ++ pr_id x ++ str " and " ++ pr_id y ++ str " must be in the same scope.") (**********************************************************************) (* Build pretty-printing rules *) @@ -704,7 +714,7 @@ let is_not_small_constr = function let rec define_keywords_aux = function | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l when is_not_small_constr e -> - Flags.if_verbose msg_info (strbrk ("Identifier '"^k^"' now a keyword")); + Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); Lexer.add_keyword k; n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l | n :: l -> n :: define_keywords_aux l @@ -713,7 +723,7 @@ let rec define_keywords_aux = function (* Ensure that IDENT articulation terminal symbols are keywords *) let define_keywords = function | GramConstrTerminal(IDENT k)::l -> - Flags.if_verbose msg_info (strbrk ("Identifier '"^k^"' now a keyword")); + Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); Lexer.add_keyword k; GramConstrTerminal(KEYWORD k) :: define_keywords_aux l | l -> define_keywords_aux l @@ -798,7 +808,7 @@ let pr_level ntn (from,args) = let error_incompatible_level ntn oldprec prec = errorlabstrm "" - (str ("Notation "^ntn^" is already defined") ++ spc() ++ + (str "Notation " ++ str ntn ++ str " is already defined" ++ spc() ++ pr_level ntn oldprec ++ spc() ++ str "while it is now required to be" ++ spc() ++ pr_level ntn prec ++ str ".") @@ -865,14 +875,16 @@ let interp_modifiers modl = | SetEntryType (s,typ) :: l -> let id = Id.of_string s in if Id.List.mem_assoc id etyps then - error (s^" is already assigned to an entry or constr level."); + errorlabstrm "Metasyntax.interp_modifiers" + (str s ++ str " is already assigned to an entry or constr level."); interp assoc level ((id,typ)::etyps) format extra l | SetItemLevel ([],n) :: l -> interp assoc level etyps format extra l | SetItemLevel (s::idl,n) :: l -> let id = Id.of_string s in if Id.List.mem_assoc id etyps then - error (s^" is already assigned to an entry or constr level."); + errorlabstrm "Metasyntax.interp_modifiers" + (str s ++ str " is already assigned to an entry or constr level."); let typ = ETConstr (n,()) in interp assoc level ((id,typ)::etyps) format extra (SetItemLevel (idl,n)::l) | SetLevel n :: l -> @@ -899,7 +911,8 @@ let check_infix_modifiers modifiers = let check_useless_entry_types recvars mainvars etyps = let vars = let (l1,l2) = List.split recvars in l1@l2@mainvars in match List.filter (fun (x,etyp) -> not (List.mem x vars)) etyps with - | (x,_)::_ -> error (Id.to_string x ^ " is unbound in the notation.") + | (x,_)::_ -> errorlabstrm "Metasyntax.check_useless_entry_types" + (pr_id x ++ str " is unbound in the notation.") | _ -> () let no_syntax_modifiers = function diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 2362d250e..fa5ed7bbd 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -164,7 +164,7 @@ let add_rec_ml_dir unix_path = let convert_string d = try Names.Id.of_string d with UserError _ -> - msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); + msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); raise Exit let add_rec_path ~unix_path ~coq_root ~implicit = @@ -184,7 +184,7 @@ let add_rec_path ~unix_path ~coq_root ~implicit = let () = List.iter add dirs in Loadpath.add_load_path unix_path ~implicit coq_root else - msg_warning (str ("Cannot open " ^ unix_path)) + msg_warning (str "Cannot open " ++ str unix_path) (* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = @@ -321,13 +321,13 @@ let reset_loaded_modules () = loaded_modules := [] let if_verbose_load verb f name ?path fname = if not verb then f name ?path fname else - let info = "[Loading ML file "^fname^" ..." in + let info = str "[Loading ML file " ++ str fname ++ str " ..." in try let path = f name ?path fname in - msg_info (str (info^" done]")); + msg_info (info ++ str " done]"); path with reraise -> - msg_info (str (info^" failed]")); + msg_info (info ++ str " failed]"); raise reraise (** Load a module for the first time (i.e. dynlink it) @@ -340,7 +340,8 @@ let trigger_ml_object verb cache reinit ?path name = add_loaded_module name (known_module_path name); if cache then perform_cache_obj name end else if not has_dynlink then - error ("Dynamic link not supported (module "^name^")") + errorlabstrm "Mltop.trigger_ml_object" + (str "Dynamic link not supported (module " ++ str name ++ str ")") else begin let file = file_of_name (Option.default name path) in let path = diff --git a/toplevel/search.ml b/toplevel/search.ml index 59283edf9..9e67eef00 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -32,7 +32,7 @@ module SearchBlacklist = let key = ["Search";"Blacklist"] let title = "Current search blacklist : " let member_message s b = - str ("Search blacklist does "^(if b then "" else "not ")^"include "^s) + str "Search blacklist does " ++ (if b then mt () else str "not ") ++ str "include " ++ str s let synchronous = true end) @@ -253,7 +253,8 @@ let interface_search flags = let regexp = try Str.regexp s with e when Errors.noncritical e -> - Errors.error ("Invalid regexp: " ^ s) + Errors.errorlabstrm "Search.interface_search" + (str "Invalid regexp: " ++ str s) in extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l | (Type_Pattern s, b) :: l -> @@ -271,7 +272,8 @@ let interface_search flags = let id = try Nametab.full_name_module qid with Not_found -> - Errors.error ("Module " ^ path ^ " not found.") + Errors.errorlabstrm "Search.interface_search" + (str "Module " ++ str path ++ str " not found.") in extract_flags name tpe subtpe ((id, b) :: mods) blacklist l | (Include_Blacklist, b) :: l -> diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 176a6c333..11cb047e0 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -27,7 +27,7 @@ let rec is_navigation_vernac = function | VernacBacktrack _ | VernacBackTo _ | VernacBack _ -> true - | VernacTime l -> + | VernacRedirect (_, l) | VernacTime l -> List.exists (fun (_,c) -> is_navigation_vernac c) l (* Time Back* is harmless *) | c -> is_deep_navigation_vernac c @@ -208,7 +208,7 @@ let display_cmd_header loc com = let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com))) in Pp.pp (str "Chars " ++ int start ++ str " - " ++ int stop ++ - str (" ["^cmd^"] ")); + str " [" ++ str cmd ++ str "] "); Pp.flush_all () let rec vernac_com verbosely checknav (loc,com) = diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index cfa9bddc6..4300d5e24 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -351,7 +351,7 @@ let dump_universes_gen g s = try Univ.dump_universes output_constraint g; close (); - msg_info (str ("Universes written to file \""^s^"\".")) + msg_info (str "Universes written to file \"" ++ str s ++ str "\".") with reraise -> let reraise = Errors.push reraise in close (); @@ -610,16 +610,14 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast = let binders_ast = List.map (fun (export,idl,ty) -> if not (Option.is_empty export) then - error ("Arguments of a functor declaration cannot be exported. " ^ - "Remove the \"Export\" and \"Import\" keywords from every functor " ^ - "argument.") + error "Arguments of a functor declaration cannot be exported. Remove the \"Export\" and \"Import\" keywords from every functor argument." else (idl,ty)) binders_ast in let mp = Declaremods.declare_module Modintern.interp_module_ast id binders_ast (Enforce mty_ast) [] in Dumpglob.dump_moddef loc mp "mod"; - if_verbose msg_info (str ("Module "^ Id.to_string id ^" is declared")); + if_verbose msg_info (str "Module " ++ pr_id id ++ str " is declared"); Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = @@ -641,7 +639,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = in Dumpglob.dump_moddef loc mp "mod"; if_verbose msg_info - (str ("Interactive Module "^ Id.to_string id ^" started")); + (str "Interactive Module " ++ pr_id id ++ str " started"); List.iter (fun (export,id) -> Option.iter @@ -651,9 +649,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = let binders_ast = List.map (fun (export,idl,ty) -> if not (Option.is_empty export) then - error ("Arguments of a functor definition can be imported only if" ^ - " the definition is interactive. Remove the \"Export\" and " ^ - "\"Import\" keywords from every functor argument.") + error "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument." else (idl,ty)) binders_ast in let mp = Declaremods.declare_module Modintern.interp_module_ast @@ -661,14 +657,14 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = in Dumpglob.dump_moddef loc mp "mod"; if_verbose msg_info - (str ("Module "^ Id.to_string id ^" is defined")); + (str "Module " ++ pr_id id ++ str " is defined"); Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export let vernac_end_module export (loc,id as lid) = let mp = Declaremods.end_module () in Dumpglob.dump_modref loc mp "mod"; - if_verbose msg_info (str ("Module "^ Id.to_string id ^" is defined")); + if_verbose msg_info (str "Module " ++ pr_id id ++ str " is defined"); Option.iter (fun export -> vernac_import export [Ident lid]) export let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = @@ -690,7 +686,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = in Dumpglob.dump_moddef loc mp "modtype"; if_verbose msg_info - (str ("Interactive Module Type "^ Id.to_string id ^" started")); + (str "Interactive Module Type " ++ pr_id id ++ str " started"); List.iter (fun (export,id) -> Option.iter @@ -701,9 +697,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = let binders_ast = List.map (fun (export,idl,ty) -> if not (Option.is_empty export) then - error ("Arguments of a functor definition can be imported only if" ^ - " the definition is interactive. Remove the \"Export\" " ^ - "and \"Import\" keywords from every functor argument.") + error "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument." else (idl,ty)) binders_ast in let mp = Declaremods.declare_modtype Modintern.interp_module_ast @@ -711,12 +705,12 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = in Dumpglob.dump_moddef loc mp "modtype"; if_verbose msg_info - (str ("Module Type "^ Id.to_string id ^" is defined")) + (str "Module Type " ++ pr_id id ++ str " is defined") let vernac_end_modtype (loc,id) = let mp = Declaremods.end_modtype () in Dumpglob.dump_modref loc mp "modtype"; - if_verbose msg_info (str ("Module Type "^ Id.to_string id ^" is defined")) + if_verbose msg_info (str "Module Type " ++ pr_id id ++ str " is defined") let vernac_include l = Declaremods.declare_include Modintern.interp_module_ast l @@ -868,7 +862,8 @@ let vernac_set_used_variables e = let vars = Environ.named_context env in List.iter (fun id -> if not (List.exists (fun (id',_,_) -> Id.equal id id') vars) then - error ("Unknown variable: " ^ Id.to_string id)) + errorlabstrm "vernac_set_used_variables" + (str "Unknown variable: " ++ pr_id id)) l; let closure_l = List.map pi1 (set_used_variables l) in let closure_l = List.fold_right Id.Set.add closure_l Id.Set.empty in @@ -914,7 +909,7 @@ let vernac_chdir = function | Some path -> begin try Sys.chdir (expand path) - with Sys_error err -> msg_warning (str ("Cd failed: " ^ err)) + with Sys_error err -> msg_warning (str "Cd failed: " ++ str err) end; if_verbose msg_info (str (Sys.getcwd())) @@ -1051,15 +1046,16 @@ let vernac_declare_arguments locality r l nargs flags = let inf_names = let ty = Global.type_of_global_unsafe sr in Impargs.compute_implicits_names (Global.env ()) ty in - let string_of_name = function Anonymous -> "_" | Name id -> Id.to_string id in let rec check li ld ls = match li, ld, ls with | [], [], [] -> () | [], Anonymous::ld, (Some _)::ls when extra_scope_flag -> check li ld ls | [], _::_, (Some _)::ls when extra_scope_flag -> error "Extra notation scopes can be set on anonymous arguments only" - | [], x::_, _ -> error ("Extra argument " ^ string_of_name x ^ ".") - | l, [], _ -> error ("The following arguments are not declared: " ^ - (String.concat ", " (List.map string_of_name l)) ^ ".") + | [], x::_, _ -> errorlabstrm "vernac_declare_arguments" + (str "Extra argument " ++ pr_name x ++ str ".") + | l, [], _ -> errorlabstrm "vernac_declare_arguments" + (str "The following arguments are not declared: " ++ + prlist_with_sep pr_comma pr_name l ++ str ".") | _::li, _::ld, _::ls -> check li ld ls | _ -> assert false in let () = match l with @@ -1087,9 +1083,6 @@ let vernac_declare_arguments locality r l nargs flags = let renamed_arg = ref None in let set_renamed a b = if Option.is_empty !renamed_arg && not (Id.equal a b) then renamed_arg := Some(b,a) in - let pr_renamed_arg () = match !renamed_arg with None -> "" - | Some (o,n) -> - "\nArgument "^string_of_id o ^" renamed to "^string_of_id n^"." in let some_renaming_specified = try let names = Arguments_renaming.arguments_names sr in @@ -1103,7 +1096,8 @@ let vernac_declare_arguments locality r l nargs flags = let sr', impl = List.fold_map (fun b -> function | (Anonymous, _,_, true, max), Name id -> assert false | (Name x, _,_, true, _), Anonymous -> - error ("Argument "^Id.to_string x^" cannot be declared implicit.") + errorlabstrm "vernac_declare_arguments" + (str "Argument " ++ pr_id x ++ str " cannot be declared implicit.") | (Name iid, _,_, true, max), Name id -> set_renamed iid id; b || not (Id.equal iid id), Some (ExplByName id, max, false) @@ -1116,8 +1110,12 @@ let vernac_declare_arguments locality r l nargs flags = some_renaming_specified l in if some_renaming_specified then if not (List.mem `Rename flags) then - error ("To rename arguments the \"rename\" flag must be specified." - ^ pr_renamed_arg ()) + errorlabstrm "vernac_declare_arguments" + (str "To rename arguments the \"rename\" flag must be specified." ++ + match !renamed_arg with + | None -> mt () + | Some (o,n) -> + str "\nArgument " ++ pr_id o ++ str " renamed to " ++ pr_id n ++ str ".") else Arguments_renaming.rename_arguments (make_section_locality locality) sr names_decl; @@ -1581,7 +1579,8 @@ let print_about_hyp_globs ref_or_by_not glnumopt = | Some n,AN (Ident (_loc,id)) -> (* goal number given, catch if wong *) (try get_nth_goal n,id with - Failure _ -> Errors.error ("No such goal: "^string_of_int n^".")) + Failure _ -> errorlabstrm "print_about_hyp_globs" + (str "No such goal: " ++ int n ++ str ".")) | _ , _ -> raise NoHyp in let hyps = pf_hyps gl in let (id,bdyopt,typ) = Context.lookup_named id hyps in @@ -1674,8 +1673,8 @@ let interp_search_about_item env = (fun _ -> true) s sc in GlobSearchSubPattern (Pattern.PRef ref) with UserError _ -> - error ("Unable to interp \""^s^"\" either as a reference or \ - as an identifier component") + errorlabstrm "interp_search_about_item" + (str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component") let vernac_search s gopt r = let r = interp_search_restriction r in @@ -1850,6 +1849,7 @@ let interp ?proof locality poly c = | VernacLoad _ -> assert false | VernacFail _ -> assert false | VernacTime _ -> assert false + | VernacRedirect _ -> assert false | VernacTimeout _ -> assert false | VernacStm _ -> assert false @@ -2128,6 +2128,8 @@ let interp ?(verbosely=true) ?proof (loc,c) = | VernacTimeout (n,v) -> current_timeout := Some n; aux ?locality ?polymorphism isprogcmd v + | VernacRedirect (s, v) -> + Pp.with_output_to_file s (aux_list ?locality ?polymorphism isprogcmd) v; | VernacTime v -> System.with_time !Flags.time (aux_list ?locality ?polymorphism isprogcmd) v; |