diff options
| -rw-r--r-- | .travis.yml | 6 | ||||
| -rw-r--r-- | TODO | 53 | ||||
| -rw-r--r-- | dev/doc/econstr.md | 129 | ||||
| -rw-r--r-- | ide/coqOps.ml | 49 | ||||
| -rw-r--r-- | ide/ide_slave.ml | 11 | ||||
| -rw-r--r-- | ide/session.ml | 2 | ||||
| -rw-r--r-- | ide/texmacspp.ml | 1 | ||||
| -rw-r--r-- | ide/wg_Command.ml | 13 | ||||
| -rw-r--r-- | ide/wg_Command.mli | 2 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 7 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 35 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 13 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_proofs.mli | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 5 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.mli | 5 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 14 | ||||
| -rw-r--r-- | plugins/funind/recdef.mli | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_ltac.ml4 | 2 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 9 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 27 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 1 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4306.v | 32 | ||||
| -rw-r--r-- | test-suite/output/Search.out | 8 | ||||
| -rw-r--r-- | test-suite/output/Search.v | 10 | ||||
| -rw-r--r-- | vernac/topfmt.ml | 27 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 32 |
27 files changed, 319 insertions, 181 deletions
diff --git a/.travis.yml b/.travis.yml index d35b7a842..72ce17a09 100644 --- a/.travis.yml +++ b/.travis.yml @@ -22,6 +22,7 @@ env: - NJOBS=2 # system is == 4.02.3 - COMPILER="system" + - CAMLP5_VER="6.14" # Main test suites matrix: - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" @@ -81,6 +82,7 @@ matrix: - env: - TEST_TARGET="test-suite" - COMPILER="4.04.0" + - CAMLP5_VER="6.17" - EXTRA_CONF="-coqide opt -with-doc yes" - EXTRA_OPAM="lablgtk-extras hevea" addons: @@ -106,8 +108,8 @@ matrix: install: - opam init -j ${NJOBS} --compiler=${COMPILER} -n -y - eval $(opam config env) -- opam config var root -- opam install -j ${NJOBS} -y camlp5 ocamlfind ${EXTRA_OPAM} +- opam config list +- opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${EXTRA_OPAM} - opam list script: @@ -1,53 +0,0 @@ -Langage: - -Distribution: - -Environnement: - -- Porter SearchIsos - -Noyau: - -Tactic: - -- Que contradiction raisonne a isomorphisme pres de False - -Vernac: - -- Print / Print Proof en fait identiques ; Print ne devrait pas afficher - les constantes opaques (devrait afficher qqchose comme <opaque>) - -Theories: - -- Rendre transparent tous les theoremes prouvant {A}+{B} -- Faire demarrer PolyList.nth a` l'indice 0 - Renommer l'actuel nth en nth1 ?? - -Doc: - -- Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection -- Documenter le filtrage sur les types inductifs avec let-ins (dont la - compatibilite V6) - -- Ajouter let dans les règles du CIC - -> FAIT, mais reste a documenter le let dans les inductifs - et les champs manifestes dans les Record -- revoir le chapitre sur les tactiques utilisateur -- faut-il mieux spécifier la sémantique de Simpl (??) - -- Préciser la clarification syntaxique de IntroPattern -- preciser que Goal vient en dernier dans une clause pattern list et - qu'il doit apparaitre si il y a un "in" - -- Omega Time debranche mais Omega System et Omega Action remarchent ? -- Ajout "Replace in" (mais TODO) -- Syntaxe Conditional tac Rewrite marche, à documenter -- Documenter Dependent Rewrite et CutRewrite ? -- Ajouter les motifs sous-termes de ltac - -- ajouter doc de GenFixpoint (mais avant: changer syntaxe) (J. Forest ou Pierre C.) -- mettre à jour la doc de induction (arguments multiples) (Pierre C.) -- mettre à jour la doc de functional induction/scheme (J. Forest ou Pierre C.) ---> mettre à jour le CHANGES (vers la ligne 72) - - diff --git a/dev/doc/econstr.md b/dev/doc/econstr.md new file mode 100644 index 000000000..bb17e8fb6 --- /dev/null +++ b/dev/doc/econstr.md @@ -0,0 +1,129 @@ +# Evar-insensitive terms (EConstr) + +Evar-insensitive terms were introduced in 8.7, following +[CEP #10](https://github.com/coq/ceps/blob/master/text/010-econstr.md). We will +not recap the motivations in this document and rather summarize the code changes +to perform. + +## Overview + +The essential datastructures are defined in +[the `EConstr` module](/engine/eConstr.mli) module. It defines +the tactic counterparts of kernel data structures such as terms +(`EConstr.constr`), universes (`EConstr.ESorts.t`) and contexts +(`EConstr.*_context`). + +The main difference with kernel-side types is that observing them requires +an evar-map at hand in order to normalize evars on the fly. The basic primitive +to observe an `EConstr.t` is the following function: +``` +val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term +(** Same as {!Constr.kind} except that it expands evars and normalizes + universes on the fly. *) +``` + +Essentially, each time it sees an evar which happens to be defined in the +provided evar-map, it replaces it with the corresponding body and carries on. + +Due to universe unification occuring at the tactic level, the same goes for +universe instances and sorts. See the `ESort` and `EInstance` modules in +`EConstr`. + +This normalization is critical for the soundness of tactics. Before EConstr, a +lot of bugs were lurking in the code base, a few still are (most notably in +meta-based unification) and failure to respect the guidelines thereafter may +result in nasal demons. + +## Transition path + +### Types + +As a rule of thumb, all functions living at the tactic level should manipulate +`EConstr.t` instead of `Constr.t`, and similarly for the other data structures. + +To ease the transition, the `EConstr` module defines a handful of aliases to +shadow the type names from the kernel. + +It is recommended to perform the following replacement in headers. +```ocaml +(** Kernel types. You may remove the two following opens if you want. Beware + that [kind_of_term] needs to be in scope if you use [EConstr.kind] so that + you may still need to open one of the two. *) +open Term +open Constr +(** Tactic types. Open this after to shadow kernel types. *) +open EConstr +``` + +Note that the `EConstr` module also redefines a `Vars` submodule. + +### Evar-map-passing + +All functions deconstructing an econstr need to take an evar-map as a parameter. +Therefore, you need to pass one as an argument virtually everywhere. + +In the Coq source code, it is recommended to take the evar-map as a first +argument called `sigma`, except if the function also takes an environment in +which case it is passed second. Namely, the two typical instances are: +```ocaml +let foo sigma c = mycode +val foo : Evd.evar_map -> EConstr.t -> Foo.t + +let bar env sigma c = mycode +val bar : Environ.env -> Evd.evar_map -> EConstr.t -> Bar.t +``` + +The EConstr API makes the code much more sensitive to evar-maps, because a +lot of now useless normalizations were removed. Thus one should be cautious of +**not** dropping the evar-map when it has been updated, and should rather stick +to a strict state-passing discipline. Unsound primitives like +`Typing.unsafe_type_of` are also a known source of problems, so you should +replace them with the corresponding evar-map-returning function and thread it +properly. + +### Functions + +Many functions from `Constr` and `Term` are redefined to work on econstr in +the `EConstr` module, so that it is often enough to perform the `open` as +described above to replace them. Their type may differ though, because they now +need access to an evar-map. A lot of econstr-manipulating functions are also +defined in [`Termops`](/engine/termops.mli). + +Functions manipulating tactic terms and kernel terms share the same name if they +are the equivalent one of the other. Do not hesitate to grep Coq mli files to +find the equivalent of a function you want to port if it is neither in `EConstr` +nor in `Termops` (this should be very rare). + +### Conversion + +Sometimes you do not have any other choice than calling kernel-side functions +on terms, and conversely to turn a kernel term into a tactic term. + +There are two functions to do so. +* `EConstr.of_constr` turns kernel terms into tactic terms. It is currently +the physical identity, and thus O(1), but this may change in the future. +* `EConstr.to_constr` turns tactic terms into kernel terms. It performs a +full-blown normalization of the given term, which is O(n) and potentially +costly. + +For performance reasons, avoiding to jump back and forth between kernel and +tactic terms is recommended. + +There are also a few unsafe conversion functions that take advantage of the +fact that `EConstr.t` is internally the same as `Constr.t`. Namely, +`EConstr.Unsafe.to_constr` is the physical identity. It should **not** be used +in typical code and is instead provided for efficiency **when you know what you +are doing**. Either use it to reimplement low-level functions that happen to +be insensitive externally, or use it to provide backward compatibility with +broken code that relies on evar-sensitivity. **Do not use it because it is +easier than stuffing evar-maps everywhere.** You've been warned. + +## Notes + +The EConstr branch fixed a lot of eisenbugs linked to lack of normalization +everywhere, most notably in unification. It may also have introduced a few, so +if you see a change in behaviour *that looks like a bug*, please report it. +Obviously, unification is not specified, so it's hard to tell apart, but still. + +Efficiency has been affected as well. We now pay an overhead when observing a +term, but at the same time a lot of costly upfront normalizations were removed. diff --git a/ide/coqOps.ml b/ide/coqOps.ml index eb97755fa..222b9eed9 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -366,6 +366,9 @@ object(self) (* This method is intended to perform stateless commands *) method raw_coq_query phrase = + let sid = try Document.tip document + with Document.Empty -> Stateid.initial + in let action = log "raw_coq_query starting now" in let display_error s = if not (validate s) then @@ -373,11 +376,10 @@ object(self) else messages#add s; in let query = - Coq.query (phrase,Stateid.dummy) in + Coq.query (phrase,sid) in let next = function | Fail (_, _, err) -> display_error err; Coq.return () - | Good msg -> - messages#add_string msg; Coq.return () + | Good msg -> Coq.return () in Coq.bind (Coq.seq action query) next @@ -414,12 +416,9 @@ object(self) buffer#apply_tag Tags.Script.tooltip ~start ~stop; add_tooltip sentence pre post markup - method private is_dummy_id id = Stateid.equal id Stateid.dummy - method private enqueue_feedback msg = - (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt (Xmlprotocol.of_feedback msg)); *) - let id = msg.id in - if self#is_dummy_id id then () else Queue.add msg feedbacks + (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt Xmlprotocol.(of_feedback Ppcmds msg)); *) + Queue.add msg feedbacks method private process_feedback () = let rec eat_feedback n = @@ -433,41 +432,41 @@ object(self) | _ -> None in try Some (Doc.find_map document finder) with Not_found -> None in - let log_pp s state_id = + let log_pp ?id s= Minilib.log_pp Pp.(seq - [str "Feedback "; s; str " on "; - str (Stateid.to_string (Option.default Stateid.dummy state_id))]) in - let log s state_id = log_pp (Pp.str s) state_id in + [str "Feedback "; s; pr_opt (fun id -> str " on " ++ str (Stateid.to_string id)) id]) + in + let log ?id s = log_pp ?id (Pp.str s) in begin match msg.contents, sentence with | AddedAxiom, Some (id,sentence) -> - log "AddedAxiom" id; + log ?id "AddedAxiom"; remove_flag sentence `PROCESSING; remove_flag sentence `ERROR; add_flag sentence `UNSAFE; self#mark_as_needed sentence | Processed, Some (id,sentence) -> - log "Processed" id; + log ?id "Processed" ; remove_flag sentence `PROCESSING; self#mark_as_needed sentence | ProcessingIn _, Some (id,sentence) -> - log "ProcessingIn" id; + log ?id "ProcessingIn"; add_flag sentence `PROCESSING; self#mark_as_needed sentence | Incomplete, Some (id, sentence) -> - log "Incomplete" id; + log ?id "Incomplete"; add_flag sentence `INCOMPLETE; self#mark_as_needed sentence | Complete, Some (id, sentence) -> - log "Complete" id; + log ?id "Complete"; remove_flag sentence `INCOMPLETE; self#mark_as_needed sentence | GlobRef(loc, filepath, modpath, ident, ty), Some (id,sentence) -> - log "GlobRef" id; + log ?id "GlobRef"; self#attach_tooltip ~loc sentence (Printf.sprintf "%s %s %s" filepath ident ty) | Message(Error, loc, msg), Some (id,sentence) -> let uloc = Option.default Loc.ghost loc in - log_pp Pp.(str "ErrorMsg" ++ msg) id; + log_pp ?id Pp.(str "ErrorMsg" ++ msg); remove_flag sentence `PROCESSING; let rmsg = Pp.string_of_ppcmds msg in add_flag sentence (`ERROR (uloc, rmsg)); @@ -476,22 +475,24 @@ object(self) self#position_tag_at_sentence ?loc Tags.Script.error sentence | Message(Warning, loc, msg), Some (id,sentence) -> let uloc = Option.default Loc.ghost loc in - log_pp Pp.(str "WarningMsg" ++ msg) id; + log_pp ?id Pp.(str "WarningMsg" ++ msg); let rmsg = Pp.string_of_ppcmds msg in add_flag sentence (`WARNING (uloc, rmsg)); self#attach_tooltip sentence ?loc rmsg; self#position_tag_at_sentence ?loc Tags.Script.warning sentence; messages#push Warning msg | Message(lvl, loc, msg), Some (id,sentence) -> - log_pp Pp.(str "Msg" ++ msg) id; + log_pp ?id Pp.(str "Msg" ++ msg); + messages#push lvl msg + | Message(lvl, loc, msg), None -> + log_pp Pp.(str "Msg" ++ msg); messages#push lvl msg | InProgress n, _ -> if n < 0 then processed <- processed + abs n else to_process <- to_process + n | WorkerStatus(id,status), _ -> - log "WorkerStatus" None; + log "WorkerStatus"; slaves_status <- CString.Map.add id status slaves_status - | _ -> if sentence <> None then Minilib.log "Unsupported feedback message" else if Doc.is_empty document then () @@ -500,7 +501,7 @@ object(self) match id, Doc.tip document with | id1, id2 when Stateid.newer_than id2 id1 -> () | _ -> Queue.add msg feedbacks - with Doc.Empty | Invalid_argument _ -> Queue.add msg feedbacks + with Doc.Empty | Invalid_argument _ -> Queue.add msg feedbacks end; eat_feedback (n-1) in diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 4b95e983d..bf86db08f 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -63,25 +63,26 @@ let is_known_option cmd = match cmd with (** Check whether a command is forbidden in the IDE *) -let ide_cmd_checks (loc,ast) = +let ide_cmd_checks ~id (loc,ast) = let user_error s = CErrors.user_err ~loc ~hdr:"CoqIde" (str s) in + let warn msg = Feedback.(feedback ~id (Message (Warning, Some loc, strbrk msg))) in if is_debug ast then user_error "Debug mode not available in the IDE"; if is_known_option ast then - Feedback.msg_warning ~loc (strbrk "Set this option from the IDE menu instead"); + warn "Set this option from the IDE menu instead"; if is_navigation_vernac ast || is_undo ast then - Feedback.msg_warning ~loc (strbrk "Use IDE navigation instead"); + warn "Use IDE navigation instead"; if is_query ast then - Feedback.msg_warning ~loc (strbrk "Query commands should not be inserted in scripts") + warn "Query commands should not be inserted in scripts" (** Interpretation (cf. [Ide_intf.interp]) *) let add ((s,eid),(sid,verbose)) = let pa = Pcoq.Gram.parsable (Stream.of_string s) in let loc_ast = Stm.parse_sentence sid pa in - ide_cmd_checks loc_ast; let newid, rc = Stm.add ~ontop:sid verbose loc_ast in let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in + ide_cmd_checks newid loc_ast; (* TODO: the "" parameter is a leftover of the times the protocol * used to include stderr/stdout output. * diff --git a/ide/session.ml b/ide/session.ml index fc6340d28..6262820e7 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -386,12 +386,12 @@ let create file coqtop_args = let proof = create_proof () in let messages = create_messages () in let segment = new Wg_Segment.segment () in - let command = new Wg_Command.command_window basename coqtop in let finder = new Wg_Find.finder basename (script :> GText.view) in let fops = new FileOps.fileops (buffer :> GText.buffer) file reset in let _ = fops#update_stats in let cops = new CoqOps.coqops script proof messages segment coqtop (fun () -> fops#filename) in + let command = new Wg_Command.command_window basename coqtop cops in let errpage = create_errpage script in let jobpage = create_jobpage coqtop cops in let _ = set_buffer_handlers (buffer :> GText.buffer) script cops coqtop in diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index e787e48bf..e20704b7f 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -504,7 +504,6 @@ let rec tmpp v loc = xmlApply loc (Element("timeout",["val",string_of_int s],[]) :: [tmpp e loc]) | VernacFail e -> xmlApply loc (Element("fail",[],[]) :: [tmpp e loc]) - | VernacError _ -> xmlWithLoc loc "error" [] [] (* Syntax *) | VernacSyntaxExtension (_, ((_, name), sml)) -> diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 47dad8f19..3fcb7ce49 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -8,7 +8,7 @@ open Preferences -class command_window name coqtop = +class command_window name coqtop coqops = let frame = Wg_Detachable.detachable ~title:(Printf.sprintf "Query pane (%s)" name) () in let _ = frame#hide in @@ -26,6 +26,11 @@ object(self) val notebook = notebook + (* We need access to coqops in order to place queries in the proper + document stint. This should remove access from this module to the + low-level Coq one. *) + val coqops = coqops + method pack_in (f : GObj.widget -> unit) = f frame#coerce val mutable new_page : GObj.widget = (GMisc.label ())#coerce @@ -101,7 +106,10 @@ object(self) else com ^ " " ^ arg ^" . " in let process = - Coq.bind (Coq.query (phrase,Stateid.dummy)) (function + (* We need to adapt this to route_id and redirect to the result buffer below *) + coqops#raw_coq_query phrase + (* + Coq.bind (Coq.query (phrase,sid)) (function | Interface.Fail (_,l,str) -> let width = Ideutils.textview_width result in Ideutils.insert_xml result#buffer (Richpp.richpp_of_pp width str); @@ -111,6 +119,7 @@ object(self) result#buffer#insert res; notebook#set_page ~tab_label:(new_tab_lbl arg) frame#coerce; Coq.return ()) + *) in result#buffer#set_text ("Result for command " ^ phrase ^ ":\n"); Coq.try_grab coqtop process ignore diff --git a/ide/wg_Command.mli b/ide/wg_Command.mli index fa50ba5fd..341322be1 100644 --- a/ide/wg_Command.mli +++ b/ide/wg_Command.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -class command_window : string -> Coq.coqtop -> +class command_window : string -> Coq.coqtop -> CoqOps.coqops -> object method new_query : ?command:string -> ?term:string -> unit -> unit method pack_in : (GObj.widget -> unit) -> unit diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 25d3c705f..f018d59e6 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -71,7 +71,7 @@ type printable = | PrintScopes | PrintScope of string | PrintVisibility of string option - | PrintAbout of reference or_by_notation*int option + | PrintAbout of reference or_by_notation * goal_selector option | PrintImplicit of reference or_by_notation | PrintAssumptions of bool * bool * reference or_by_notation | PrintStrategy of reference or_by_notation option @@ -316,7 +316,6 @@ type vernac_expr = | VernacRedirect of string * vernac_expr located | VernacTimeout of int * vernac_expr | VernacFail of vernac_expr - | VernacError of exn (* always fails *) (* Syntax *) | VernacSyntaxExtension of @@ -436,11 +435,11 @@ type vernac_expr = | VernacRemoveOption of Goptions.option_name * option_ref_value list | VernacMemOption of Goptions.option_name * option_ref_value list | VernacPrintOption of Goptions.option_name - | VernacCheckMayEval of Genredexpr.raw_red_expr option * int option * constr_expr + | VernacCheckMayEval of Genredexpr.raw_red_expr option * goal_selector option * constr_expr | VernacGlobalCheck of constr_expr | VernacDeclareReduction of string * Genredexpr.raw_red_expr | VernacPrint of printable - | VernacSearch of searchable * int option * search_restriction + | VernacSearch of searchable * goal_selector option * search_restriction | VernacLocate of locatable | VernacRegister of lident * register_kind | VernacComments of comment list diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 4fd316119..011565d86 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -40,7 +40,6 @@ let def_body = Gram.entry_create "vernac:def_body" let decl_notation = Gram.entry_create "vernac:decl_notation" let record_field = Gram.entry_create "vernac:record_field" let of_type_with_opt_coercion = Gram.entry_create "vernac:of_type_with_opt_coercion" -let subgoal_command = Gram.entry_create "proof_mode:subgoal_command" let instance_name = Gram.entry_create "vernac:instance_name" let section_subset_expr = Gram.entry_create "vernac:section_subset_expr" @@ -53,7 +52,7 @@ let make_bullet s = | _ -> assert false GEXTEND Gram - GLOBAL: vernac gallina_ext noedit_mode subprf subgoal_command; + GLOBAL: vernac gallina_ext noedit_mode subprf; vernac: FIRST [ [ IDENT "Time"; c = located_vernac -> VernacTime c | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c) @@ -92,7 +91,7 @@ GEXTEND Gram [ [ prfcom = command_entry -> prfcom ] ] ; noedit_mode: - [ [ c = subgoal_command -> c None] ] + [ [ c = query_command -> c None] ] ; subprf: @@ -102,15 +101,6 @@ GEXTEND Gram ] ] ; - subgoal_command: - [ [ c = query_command; "." -> - begin function - | Some (SelectNth g) -> c (Some g) - | None -> c None - | _ -> - VernacError (UserError (None,str"Typing and evaluation commands, cannot be used with the \"all:\" selector.")) - end ] ] - ; located_vernac: [ [ v = vernac -> !@loc, v ] ] ; @@ -918,29 +908,30 @@ GEXTEND Gram VernacRemoveOption ([table], v) ]] ; query_command: (* TODO: rapprocher Eval et Check *) - [ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr -> + [ [ IDENT "Eval"; r = red_expr; "in"; c = lconstr; "." -> fun g -> VernacCheckMayEval (Some r, g, c) - | IDENT "Compute"; c = lconstr -> + | IDENT "Compute"; c = lconstr; "." -> fun g -> VernacCheckMayEval (Some (Genredexpr.CbvVm None), g, c) - | IDENT "Check"; c = lconstr -> + | IDENT "Check"; c = lconstr; "." -> fun g -> VernacCheckMayEval (None, g, c) (* Searching the environment *) - | IDENT "About"; qid = smart_global -> + | IDENT "About"; qid = smart_global; "." -> fun g -> VernacPrint (PrintAbout (qid,g)) - | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules -> + | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules; "." -> fun g -> VernacSearch (SearchHead c,g, l) - | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules -> + | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules; "." -> fun g -> VernacSearch (SearchPattern c,g, l) - | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules -> + | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." -> fun g -> VernacSearch (SearchRewrite c,g, l) - | IDENT "Search"; s = searchabout_query; l = searchabout_queries -> + | IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." -> let (sl,m) = l in fun g -> VernacSearch (SearchAbout (s::sl),g, m) (* compatibility: SearchAbout *) - | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries -> + | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries; "." -> fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m) (* compatibility: SearchAbout with "[ ... ]" *) | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]"; - l = in_or_out_modules -> fun g -> VernacSearch (SearchAbout sl,g, l) + l = in_or_out_modules; "." -> + fun g -> VernacSearch (SearchAbout sl,g, l) ] ] ; printable: diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 48c0f5f04..8dae17d69 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -299,7 +299,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = Can be safely replaced by the next comment for Ocaml >= 3.08.4 *) let sub = Int.Map.bindings sub in - List.fold_left (fun end_of_type (i,t) -> lift 1 (substnl [t] (i-1) end_of_type)) + List.fold_left (fun end_of_type (i,t) -> liftn 1 i (substnl [t] (i-1) end_of_type)) end_of_type_with_pop sub in @@ -1401,8 +1401,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let prove_with_tcc tcc_lemma_constr eqs : tactic = match !tcc_lemma_constr with - | None -> anomaly (Pp.str "No tcc proof !!") - | Some lemma -> + | Undefined -> anomaly (Pp.str "No tcc proof !!") + | Value lemma -> fun gls -> (* let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *) (* let ids = hid::pf_ids_of_hyps gls in *) @@ -1420,7 +1420,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic = Proofview.V82.of_tactic (Eauto.gen_eauto (false,5) [] (Some [])) ] gls - + | Not_needed -> tclIDTAC let backtrack_eqs_until_hrec hrec eqs : tactic = fun gls -> @@ -1599,8 +1599,9 @@ let prove_principle_for_gen let args_ids = List.map (get_name %> Nameops.out_name) princ_info.args in let lemma = match !tcc_lemma_ref with - | None -> error "No tcc proof !!" - | Some lemma -> EConstr.of_constr lemma + | Undefined -> error "No tcc proof !!" + | Value lemma -> EConstr.of_constr lemma + | Not_needed -> EConstr.of_constr (Coqlib.build_coq_I ()) in (* let rec list_diff del_list check_list = *) (* match del_list with *) diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli index 769d726d7..7ddc84d01 100644 --- a/plugins/funind/functional_principles_proofs.mli +++ b/plugins/funind/functional_principles_proofs.mli @@ -9,7 +9,7 @@ val prove_princ_for_struct : val prove_principle_for_gen : constant*constant*constant -> (* name of the function, the functional and the fixpoint equation *) - constr option ref -> (* a pointer to the obligation proofs lemma *) + Indfun_common.tcc_lemma_value ref -> (* a pointer to the obligation proofs lemma *) bool -> (* is that function uses measure *) int -> (* the number of recursive argument *) EConstr.types -> (* the type of the recursive argument *) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 20da12f39..7b0d7d27d 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -543,3 +543,8 @@ let prodn n env b = (* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *) let compose_prod l b = prodn (List.length l) l b + +type tcc_lemma_value = + | Undefined + | Value of Constr.constr + | Not_needed diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 5c3e73e9d..5ef8f05bb 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -119,3 +119,8 @@ val decompose_lam_n : Evd.evar_map -> int -> EConstr.t -> (Names.Name.t * EConstr.t) list * EConstr.t val compose_lam : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t + +type tcc_lemma_value = + | Undefined + | Value of Constr.constr + | Not_needed diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5460d6fb7..26ba5ef40 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -45,12 +45,6 @@ open Indfun_common open Sigma.Notations open Context.Rel.Declaration -let local_assum (na, t) = - LocalAssum (na, EConstr.Unsafe.to_constr t) - -let local_def (na, b, t) = - LocalDef (na, EConstr.Unsafe.to_constr b, EConstr.Unsafe.to_constr t) - (* Ugly things which should not be here *) let coq_constant m s = @@ -1323,7 +1317,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant") in let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in - ref_ := Some (EConstr.Unsafe.to_constr lemma); + ref_ := Value (EConstr.Unsafe.to_constr lemma); let lid = ref [] in let h_num = ref (-1) in let env = Global.env () in @@ -1411,7 +1405,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp let com_terminate tcc_lemma_name - (tcc_lemma_ref : Constr.t option ref) + tcc_lemma_ref is_mes fonctional_ref input_type @@ -1440,6 +1434,7 @@ let com_terminate (new_goal_type); with Failure "empty list of subgoals!" -> (* a non recursive function declared with measure ! *) + tcc_lemma_ref := Not_needed; defined () @@ -1515,7 +1510,6 @@ let (com_eqn : int -> Id.t -> (* Pp.msgnl (str "eqn finished"); *) );; - let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq generate_induction_principle using_lemmas : unit = let open Term in @@ -1561,7 +1555,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num in let evm = Evd.from_ctx evuctx in let tcc_lemma_name = add_suffix function_name "_tcc" in - let tcc_lemma_constr = ref None in + let tcc_lemma_constr = ref Undefined in (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) let hook _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index 9c1081b9d..80f02e01c 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -13,7 +13,7 @@ bool -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> int -> Constrexpr.constr_expr -> (Term.pconstant -> - Term.constr option ref -> + Indfun_common.tcc_lemma_value ref -> Term.pconstant -> Term.pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index ece0adb07..ca5d198c2 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -335,7 +335,7 @@ GEXTEND Gram | IDENT "all"; ":" -> SelectAll ] ] ; tactic_mode: - [ [ g = OPT toplevel_selector; tac = G_vernac.subgoal_command -> tac g ] ] + [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g ] ] ; command: [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 547cb1de9..e4a87739b 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -107,7 +107,7 @@ open Decl_kinds | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc let pr_search a gopt b pr_p = - pr_opt (fun g -> int g ++ str ":"++ spc()) gopt + pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt ++ match a with | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b @@ -497,7 +497,7 @@ open Decl_kinds | PrintVisibility s -> keyword "Print Visibility" ++ pr_opt str s | PrintAbout (qid,gopt) -> - pr_opt (fun g -> int g ++ str ":"++ spc()) gopt + pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt ++ keyword "About" ++ spc() ++ pr_smart_global qid | PrintImplicit qid -> keyword "Print Implicit" ++ spc() ++ pr_smart_global qid @@ -619,8 +619,6 @@ open Decl_kinds return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_body v) | VernacFail v -> return (keyword "Fail" ++ spc() ++ pr_vernac_body v) - | VernacError _ -> - return (keyword "No-parsing-rule for VernacError") (* Syntax *) | VernacOpenCloseScope (_,(opening,sc)) -> @@ -1140,7 +1138,8 @@ open Decl_kinds spc() ++ keyword "in" ++ spc () ++ pr_lconstr c) | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) in - let pr_i = match io with None -> mt () | Some i -> int i ++ str ": " in + let pr_i = match io with None -> mt () + | Some i -> Proof_global.pr_goal_selector i ++ str ": " in return (pr_i ++ pr_mayeval r c) | VernacGlobalCheck c -> return (hov 2 (keyword "Type" ++ pr_constrarg c)) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 3ee6fd40f..5f4a7766f 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -671,16 +671,18 @@ let _ = let default_goal_selector = ref (Vernacexpr.SelectNth 1) let get_default_goal_selector () = !default_goal_selector -let print_range_selector (i, j) = - if i = j then string_of_int i - else string_of_int i ^ "-" ^ string_of_int j - -let print_goal_selector = function - | Vernacexpr.SelectAll -> "all" - | Vernacexpr.SelectNth i -> string_of_int i - | Vernacexpr.SelectList l -> "[" ^ - String.concat ", " (List.map print_range_selector l) ^ "]" - | Vernacexpr.SelectId id -> Id.to_string id +let pr_range_selector (i, j) = + if i = j then int i + else int i ++ str "-" ++ int j + +let pr_goal_selector = function + | Vernacexpr.SelectAll -> str "all" + | Vernacexpr.SelectNth i -> int i + | Vernacexpr.SelectList l -> + str "[" + ++ prlist_with_sep pr_comma pr_range_selector l + ++ str "]" + | Vernacexpr.SelectId id -> Id.print id let parse_goal_selector = function | "all" -> Vernacexpr.SelectAll @@ -699,7 +701,10 @@ let _ = optdepr = false; optname = "default goal selector" ; optkey = ["Default";"Goal";"Selector"] ; - optread = begin fun () -> print_goal_selector !default_goal_selector end; + optread = begin fun () -> + string_of_ppcmds + (pr_goal_selector !default_goal_selector) + end; optwrite = begin fun n -> default_goal_selector := parse_goal_selector n end diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 3b2cc6b23..6bb6f5e2c 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -198,6 +198,7 @@ end (* *) (**********************************************************) +val pr_goal_selector : Vernacexpr.goal_selector -> Pp.std_ppcmds val get_default_goal_selector : unit -> Vernacexpr.goal_selector module V82 : sig diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index fb6adaec5..c4f392f20 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -202,8 +202,7 @@ let rec classify_vernac e = (* What are these? *) | VernacToplevelControl _ | VernacRestoreState _ - | VernacWriteState _ - | VernacError _ -> VtUnknown, VtNow + | VernacWriteState _ -> VtUnknown, VtNow (* Plugins should classify their commands *) | VernacExtend (s,l) -> try List.assoc s !classifiers l () diff --git a/test-suite/bugs/closed/4306.v b/test-suite/bugs/closed/4306.v new file mode 100644 index 000000000..4aef5bb95 --- /dev/null +++ b/test-suite/bugs/closed/4306.v @@ -0,0 +1,32 @@ +Require Import List. +Require Import Arith. +Require Import Recdef. +Require Import Omega. + +Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat := + match xys with + | (nil, _) => snd xys + | (_, nil) => fst xys + | (x :: xs', y :: ys') => match Compare_dec.nat_compare x y with + | Lt => x :: foo (xs', y :: ys') + | Eq => x :: foo (xs', ys') + | Gt => y :: foo (x :: xs', ys') + end + end. +Proof. + intros; simpl; omega. + intros; simpl; omega. + intros; simpl; omega. +Qed. + +Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat := + let (xs, ys) := xys in + match (xs, ys) with + | (nil, _) => ys + | (_, nil) => xs + | (x :: xs', y :: ys') => match Compare_dec.nat_compare x y with + | Lt => x :: foo (xs', ys) + | Eq => x :: foo (xs', ys') + | Gt => y :: foo (xs, ys') + end + end.
\ No newline at end of file diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 81fda176e..7446c17d9 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -98,6 +98,14 @@ h: n <> newdef n h': newdef n <> n h: n <> newdef n h: n <> newdef n +h: n <> newdef n +h': newdef n <> n +The command has indeed failed with message: +No such goal. +The command has indeed failed with message: +Query commands only support the single numbered goal selector. +The command has indeed failed with message: +Query commands only support the single numbered goal selector. h: P n h': ~ P n h: P n diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v index 2a0f0b407..82096f29b 100644 --- a/test-suite/output/Search.v +++ b/test-suite/output/Search.v @@ -10,11 +10,19 @@ Search (@eq _ _ _) true -false "prop" -"intro". (* andb_prop *) Definition newdef := fun x:nat => x. Goal forall n:nat, n <> newdef n -> newdef n <> n -> False. - intros n h h'. + cut False. + intros _ n h h'. Search n. (* search hypothesis *) Search newdef. (* search hypothesis *) Search ( _ <> newdef _). (* search hypothesis, pattern *) Search ( _ <> newdef _) -"h'". (* search hypothesis, pattern *) + + 1:Search newdef. + 2:Search newdef. + + Fail 3:Search newdef. + Fail 1-2:Search newdef. + Fail all:Search newdef. Abort. Goal forall n (P:nat -> Prop), P n -> ~P n -> False. diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index a4acd3f24..c25dd55fb 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -112,26 +112,23 @@ let msgnl_with ?pre_hdr fmt strm = pp_with fmt (strm ++ fnl ()); Format.pp_print_flush fmt () -(* XXX: This is really painful! *) module Emacs = struct (* Special chars for emacs, to detect warnings inside goal output *) - let emacs_quote_start = String.make 1 (Char.chr 254) - let emacs_quote_end = String.make 1 (Char.chr 255) + let quote_warning_start = "<warning>" + let quote_warning_end = "</warning>" - let emacs_quote_err g = - hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end) + let quote_info_start = "<infomsg>" + let quote_info_end = "</infomsg>" - let emacs_quote_info_start = "<infomsg>" - let emacs_quote_info_end = "</infomsg>" + let quote_emacs q_start q_end msg = + hov 0 (seq [str q_start; brk(0,0); msg; brk(0,0); str q_end]) - let emacs_quote_info g = - hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end) + let quote_warning = quote_emacs quote_warning_start quote_warning_end + let quote_info = quote_emacs quote_info_start quote_info_end end -open Emacs - let dbg_hdr = tag Tag.debug (str "Debug:") ++ spc () let info_hdr = mt () let warn_hdr = tag Tag.warning (str "Warning:") ++ spc () @@ -144,13 +141,13 @@ let make_body quoter info ?pre_hdr s = (* The empty quoter *) let noq x = x (* Generic logger *) -let gen_logger dbg err ?pre_hdr level msg = match level with +let gen_logger dbg warn ?pre_hdr level msg = match level with | Debug -> msgnl_with !std_ft (make_body dbg dbg_hdr ?pre_hdr msg) | Info -> msgnl_with !std_ft (make_body dbg info_hdr ?pre_hdr msg) | Notice -> msgnl_with !std_ft (make_body noq info_hdr ?pre_hdr msg) | Warning -> Flags.if_warn (fun () -> - msgnl_with !err_ft (make_body err warn_hdr ?pre_hdr msg)) () - | Error -> msgnl_with !err_ft (make_body err err_hdr ?pre_hdr msg) + msgnl_with !err_ft (make_body warn warn_hdr ?pre_hdr msg)) () + | Error -> msgnl_with !err_ft (make_body noq err_hdr ?pre_hdr msg) (** Standard loggers *) @@ -261,7 +258,7 @@ let init_color_output () = - Warning/Error: emacs_quote_err - Notice: unquoted *) -let emacs_logger = gen_logger emacs_quote_info emacs_quote_err +let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning (* Output to file, used only in extraction so a candidate for removal *) let ft_logger old_logger ft ?loc level mesg = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 92b1a5956..52136a70e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1533,7 +1533,14 @@ let get_current_context_of_args = function | Some n -> get_goal_context n | None -> get_current_context () -let vernac_check_may_eval redexp glopt rc = +let query_command_selector ~loc = function + | None -> None + | Some (SelectNth n) -> Some n + | _ -> user_err ~loc ~hdr:"query_command_selector" + (str "Query commands only support the single numbered goal selector.") + +let vernac_check_may_eval ~loc redexp glopt rc = + let glopt = query_command_selector ~loc glopt in let (sigma, env) = get_current_context_of_args glopt in let sigma', c = interp_open_constr env sigma rc in let c = EConstr.Unsafe.to_constr c in @@ -1595,9 +1602,10 @@ exception NoHyp (* Printing "About" information of a hypothesis of the current goal. We only print the type and a small statement to this comes from the goal. Precondition: there must be at least one current goal. *) -let print_about_hyp_globs ref_or_by_not glnumopt = +let print_about_hyp_globs ~loc ref_or_by_not glopt = let open Context.Named.Declaration in try + let glnumopt = query_command_selector ~loc glopt in let gl,id = match glnumopt,ref_or_by_not with | None,AN (Ident (_loc,id)) -> (* goal number not given, catch any failure *) @@ -1605,8 +1613,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 _ -> user_err ~hdr:"print_about_hyp_globs" - (str "No such goal: " ++ int n ++ str ".")) + Failure _ -> user_err ~loc ~hdr:"print_about_hyp_globs" + (str "No such goal: " ++ int n ++ str ".")) | _ , _ -> raise NoHyp in let hyps = pf_hyps gl in let decl = Context.Named.lookup id hyps in @@ -1619,7 +1627,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt = | NoHyp | Not_found -> print_about ref_or_by_not -let vernac_print = let open Feedback in function +let vernac_print ~loc = let open Feedback in function | PrintTables -> msg_notice (print_tables ()) | PrintFullContext-> msg_notice (print_full_context_typ ()) | PrintSectionContext qid -> msg_notice (print_sec_context_typ qid) @@ -1664,7 +1672,7 @@ let vernac_print = let open Feedback in function | PrintVisibility s -> msg_notice (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s) | PrintAbout (ref_or_by_not,glnumopt) -> - msg_notice (print_about_hyp_globs ref_or_by_not glnumopt) + msg_notice (print_about_hyp_globs ~loc ref_or_by_not glnumopt) | PrintImplicit qid -> dump_global qid; msg_notice (print_impargs qid) | PrintAssumptions (o,t,r) -> @@ -1729,7 +1737,8 @@ let _ = optread = (fun () -> !search_output_name_only); optwrite = (:=) search_output_name_only } -let vernac_search s gopt r = +let vernac_search ~loc s gopt r = + let gopt = query_command_selector ~loc gopt in let r = interp_search_restriction r in let env,gopt = match gopt with | None -> @@ -1935,9 +1944,6 @@ let interp ?proof ~loc locality poly c = | VernacBack _ -> anomaly (str "VernacBack not handled by Stm") | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm") - (* Horrible Hack that should die. *) - | VernacError e -> raise e - (* This one is possible to handle here *) | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") @@ -2039,11 +2045,11 @@ let interp ?proof ~loc locality poly c = | VernacAddOption (key,v) -> vernac_add_option key v | VernacMemOption (key,v) -> vernac_mem_option key v | VernacPrintOption key -> vernac_print_option key - | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval r g c + | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval ~loc r g c | VernacDeclareReduction (s,r) -> vernac_declare_reduction locality s r | VernacGlobalCheck c -> vernac_global_check c - | VernacPrint p -> vernac_print p - | VernacSearch (s,g,r) -> vernac_search s g r + | VernacPrint p -> vernac_print ~loc p + | VernacSearch (s,g,r) -> vernac_search ~loc s g r | VernacLocate l -> vernac_locate l | VernacRegister (id, r) -> vernac_register id r | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n") |