aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES7
-rw-r--r--dev/Coq_Bugzilla_autolink.user.js34
-rw-r--r--ide/coqOps.ml7
-rw-r--r--lib/coqProject_file.ml42
-rw-r--r--parsing/egramcoq.ml2
-rw-r--r--parsing/g_constr.ml41
-rw-r--r--plugins/ltac/g_ltac.ml411
-rw-r--r--plugins/ltac/pptactic.ml16
-rw-r--r--plugins/ltac/pptactic.mli2
-rw-r--r--plugins/ltac/tacinterp.ml8
-rw-r--r--plugins/ssrmatching/ssrmatching.ml414
-rw-r--r--pretyping/detyping.ml2
-rw-r--r--stm/stm.ml59
-rw-r--r--tactics/auto.ml35
-rw-r--r--test-suite/bugs/closed/5692.v38
-rw-r--r--test-suite/bugs/closed/5741.v4
-rw-r--r--test-suite/output/auto.out2
-rw-r--r--test-suite/output/auto.v4
-rw-r--r--test-suite/output/ltac_extra_args.out8
-rw-r--r--test-suite/output/ltac_extra_args.v10
-rw-r--r--tools/coqwc.mll2
-rw-r--r--toplevel/vernac.ml6
22 files changed, 202 insertions, 72 deletions
diff --git a/CHANGES b/CHANGES
index ca5172d7b7..fdf0c9d6be 100644
--- a/CHANGES
+++ b/CHANGES
@@ -133,6 +133,13 @@ Plugins
- The mathematical proof language (also known as declarative mode) was removed.
- A new command Extraction TestCompile has been introduced, not meant
for the general user but instead for Coq's test-suite.
+- The extraction plugin is no longer loaded by default. It must be
+ explicitly loaded with [Require Extraction], which is backwards
+ compatible.
+- The functional induction plugin (which provides the [Function]
+ vernacular) is no longer loaded by default. It must be explicitly
+ loaded with [Require FunInd], which is backwards compatible.
+
Dependencies
diff --git a/dev/Coq_Bugzilla_autolink.user.js b/dev/Coq_Bugzilla_autolink.user.js
new file mode 100644
index 0000000000..371c5adc00
--- /dev/null
+++ b/dev/Coq_Bugzilla_autolink.user.js
@@ -0,0 +1,34 @@
+// ==UserScript==
+// @name Coq Bugzilla autolink
+// @namespace SkySkimmer
+// @include https://github.com/coq/coq/*
+// @description Makes BZ#XXXX into links to bugzilla for GitHub
+// @version 1
+// @grant none
+// ==/UserScript==
+
+var regex = /BZ#(\d+)/g;
+var substr = '<a href="https://coq.inria.fr/bugs/show_bug.cgi?id=$1">$&</a>';
+
+function doNode(node)
+{
+ node.innerHTML = node.innerHTML.replace(regex,substr);
+}
+
+var comments = document.getElementsByClassName("comment-body");
+
+for(var i=0; i<comments.length; i++)
+{
+ var pars = comments[i].getElementsByTagName("p");
+ for(var j=0; j<pars.length; j++)
+ {
+ doNode(pars[j]);
+ }
+}
+
+// usually 1 or 0 titles...
+var titles = document.getElementsByClassName("js-issue-title");
+for(var i=0; i<titles.length; i++)
+{
+ doNode(titles[i]);
+}
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 9be70e6d38..0dd08293c8 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -480,8 +480,11 @@ object(self)
| Message(lvl, loc, msg), Some (id,sentence) ->
log_pp ?id Pp.(str "Msg " ++ msg);
messages#push lvl msg
+ (* We do nothing here as for BZ#5583 *)
+ | Message(Error, loc, msg), None ->
+ log_pp Pp.(str "Error Msg without a sentence" ++ msg)
| Message(lvl, loc, msg), None ->
- log_pp Pp.(str "Msg " ++ msg);
+ log_pp Pp.(str "Msg without a sentence " ++ msg);
messages#push lvl msg
| InProgress n, _ ->
if n < 0 then processed <- processed + abs n
@@ -655,7 +658,7 @@ object(self)
with Doc.Empty -> initial_state | Invalid_argument _ -> assert false in
loop tip [] in
Coq.bind fill_queue process_queue
-
+
method join_document =
let next = function
| Good _ ->
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index 13de731f54..970666638c 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml4
@@ -206,7 +206,7 @@ let rec find_project_file ~from ~projfile_name =
if Sys.file_exists fname then Some fname
else
let newdir = Filename.dirname from in
- if newdir = "" || newdir = "/" then None
+ if newdir = from then None
else find_project_file ~from:newdir ~projfile_name
;;
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 870137ca11..d51b8b54e5 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -34,6 +34,7 @@ let default_levels =
[200,Extend.RightA,false;
100,Extend.RightA,false;
99,Extend.RightA,true;
+ 90,Extend.RightA,true;
10,Extend.RightA,false;
9,Extend.RightA,false;
8,Extend.RightA,true;
@@ -44,6 +45,7 @@ let default_pattern_levels =
[200,Extend.RightA,true;
100,Extend.RightA,false;
99,Extend.RightA,true;
+ 90,Extend.RightA,true;
11,Extend.LeftA,false;
10,Extend.RightA,false;
1,Extend.LeftA,false;
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 4e8b98fcf2..844c040fdf 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -376,6 +376,7 @@ GEXTEND Gram
| "100" RIGHTA
[ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CAst.make ~loc:!@loc @@ CPatOr (p::pl) ]
| "99" RIGHTA [ ]
+ | "90" RIGHTA [ ]
| "11" LEFTA
[ p = pattern; "as"; id = ident ->
CAst.make ~loc:!@loc @@ CPatAlias (p, id) ]
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 2ea0f60ebc..86c983bdd9 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -388,16 +388,7 @@ let vernac_solve n info tcom b =
p,status) in
if not status then Feedback.feedback Feedback.AddedAxiom
-let pr_range_selector (i, j) =
- if Int.equal i j then int i
- else int i ++ str "-" ++ int j
-
-let pr_ltac_selector = function
-| SelectNth i -> int i ++ str ":"
-| SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++
- str "]" ++ str ":"
-| SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":"
-| SelectAll -> str "all" ++ str ":"
+let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s
VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector
| [ toplevel_selector(s) ] -> [ s ]
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 8a0764975d..d8bd166208 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -477,12 +477,14 @@ type 'a extra_genarg_printer =
if Int.equal i j then int i
else int i ++ str "-" ++ int j
- let pr_goal_selector = function
- | SelectNth i -> int i ++ str ":"
- | SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++
- str "]" ++ str ":"
- | SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":"
- | SelectAll -> str "all" ++ str ":"
+let pr_goal_selector toplevel = function
+ | SelectNth i -> int i ++ str ":"
+ | SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":"
+ | SelectId id -> str "[" ++ Id.print id ++ str "]:"
+ | SelectAll -> assert toplevel; str "all:"
+
+let pr_goal_selector ~toplevel s =
+ (if toplevel then mt () else str "only ") ++ pr_goal_selector toplevel s
let pr_lazy = function
| General -> keyword "multi"
@@ -988,7 +990,7 @@ type 'a extra_genarg_printer =
keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
| TacComplete t ->
pr_tac (lcomplete,E) t, lcomplete
- | TacSelect (s, tac) -> pr_goal_selector s ++ spc () ++ pr_tac ltop tac, latom
+ | TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, latom
| TacId l ->
keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom
| TacAtom (loc,t) ->
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 1f6ebaf448..c79d5b389f 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -53,6 +53,8 @@ type pp_tactic = {
pptac_prods : grammar_terminals;
}
+val pr_goal_selector : toplevel:bool -> goal_selector -> Pp.t
+
val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
val pr_with_occurrences :
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 18348bc113..20f117ff4f 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1394,7 +1394,13 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval
else
Ftactic.return (of_tacvalue (VFun(push_appl appl largs,trace,newlfun,lvar,body)))
- | _ -> fail
+ | (VFun(appl,trace,olfun,[],body)) ->
+ let extra_args = List.length largs in
+ Tacticals.New.tclZEROMSG (str "Illegal tactic application: got " ++
+ str (string_of_int extra_args) ++
+ str " extra " ++ str (String.plural extra_args "argument") ++
+ str ".")
+ | VRec(_,_) -> fail
else fail
(* Gives the tactic corresponding to the tactic value *)
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 2e5522b83f..e3e34616bf 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -502,16 +502,16 @@ let ungen_upat lhs (sigma, uc, t) u =
let nb_cs_proj_args pc f u =
let na k =
List.length (snd (lookup_canonical_conversion (ConstRef pc, k))).o_TCOMPS in
- try match kind_of_term f with
- | Prod _ -> na Prod_cs
- | Sort s -> na (Sort_cs (family_of_sort s))
- | Const (c',_) when Constant.equal c' pc ->
- begin match kind_of_term u.up_f with
+ let nargs_of_proj t = match kind_of_term t with
| App(_,args) -> Array.length args
| Proj _ -> 0 (* if splay_app calls expand_projection, this has to be
the number of arguments including the projected *)
- | _ -> assert false
- end
+ | _ -> assert false in
+ try match kind_of_term f with
+ | Prod _ -> na Prod_cs
+ | Sort s -> na (Sort_cs (family_of_sort s))
+ | Const (c',_) when Constant.equal c' pc -> nargs_of_proj u.up_f
+ | Proj (c',_) when Constant.equal (Projection.constant c') pc -> nargs_of_proj u.up_f
| Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (global_of_constr f))
| _ -> -1
with Not_found -> -1
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 69a49749cd..f3e8e72bb7 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -464,7 +464,7 @@ and detype_r d flags avoid env sigma t =
(* Using a dash to be unparsable *)
GEvar (Id.of_string_soft "CONTEXT-HOLE", [])
else
- GEvar (Id.of_string_soft ("INTERNAL#" ^ string_of_int n), [])
+ GEvar (Id.of_string_soft ("M" ^ string_of_int n), [])
| Var id ->
(try let _ = Global.lookup_named id in GRef (VarRef id, None)
with Not_found -> GVar id)
diff --git a/stm/stm.ml b/stm/stm.ml
index 75ec946f03..984a874296 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1044,8 +1044,18 @@ end = struct (* {{{ *)
match f acc (id, vcs, ids, tactic, undo) with
| `Stop x -> x
| `Cont acc -> next acc
-
+
+ let undo_costly_in_batch_mode =
+ CWarnings.create ~name:"undo-batch-mode" ~category:"non-interactive" Pp.(fun v ->
+ str "Command " ++ Ppvernac.pr_vernac v ++
+ str (" is not recommended in batch mode. In particular, going back in the document" ^
+ " is not efficient in batch mode due to Coq not caching previous states for memory optimization reasons." ^
+ " If your use is intentional, you may want to disable this warning and pass" ^
+ " the \"-async-proofs-cache force\" option to Coq."))
+
let undo_vernac_classifier v =
+ if !Flags.batch_mode && !Flags.async_proofs_cache <> Some Flags.Force
+ then undo_costly_in_batch_mode v;
try
match v with
| VernacResetInitial ->
@@ -2000,24 +2010,24 @@ let collect_proof keep cur hd brkind id =
| { expr = (VernacRequire _ | VernacImport _) } -> true
| ast -> may_pierce_opaque ast in
let parent = function Some (p, _) -> p | None -> assert false in
- let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> false in
+ let is_empty = function `Async(_,[],_,_) | `MaybeASync(_,[],_,_) -> true | _ -> false in
let rec collect last accn id =
let view = VCS.visit id in
match view.step with
| (`Sideff (ReplayCommand x,_) | `Cmd { cast = x })
- when too_complex_to_delegate x -> `Sync(no_name,None,`Print)
+ when too_complex_to_delegate x -> `Sync(no_name,`Print)
| `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next
| `Sideff (ReplayCommand x,_) -> collect (Some (id,x)) (id::accn) view.next
(* An Alias could jump everywhere... we hope we can ignore it*)
- | `Alias _ -> `Sync (no_name,None,`Alias)
+ | `Alias _ -> `Sync (no_name,`Alias)
| `Fork((_,_,_,_::_::_), _) ->
- `Sync (no_name,proof_using_ast last,`MutualProofs)
+ `Sync (no_name,`MutualProofs)
| `Fork((_,_,Doesn'tGuaranteeOpacity,_), _) ->
- `Sync (no_name,proof_using_ast last,`Doesn'tGuaranteeOpacity)
+ `Sync (no_name,`Doesn'tGuaranteeOpacity)
| `Fork((_,hd',GuaranteesOpacity,ids), _) when has_proof_using last ->
assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
let name = name ids in
- `ASync (parent last,proof_using_ast last,accn,name,delegate name)
+ `ASync (parent last,accn,name,delegate name)
| `Fork((_, hd', GuaranteesOpacity, ids), _) when
has_proof_no_using last && not (State.is_cached_and_valid (parent last)) &&
!Flags.compilation_mode = Flags.BuildVio ->
@@ -2026,31 +2036,32 @@ let collect_proof keep cur hd brkind id =
let name, hint = name ids, get_hint_ctx loc in
let t, v = proof_no_using last in
v.expr <- VernacProof(t, Some hint);
- `ASync (parent last,proof_using_ast last,accn,name,delegate name)
+ `ASync (parent last,accn,name,delegate name)
with Not_found ->
let name = name ids in
- `MaybeASync (parent last, None, accn, name, delegate name))
+ `MaybeASync (parent last, accn, name, delegate name))
| `Fork((_, hd', GuaranteesOpacity, ids), _) ->
assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
let name = name ids in
- `MaybeASync (parent last, None, accn, name, delegate name)
+ `MaybeASync (parent last, accn, name, delegate name)
| `Sideff _ ->
warn_deprecated_nested_proofs ();
- `Sync (no_name,None,`NestedProof)
- | _ -> `Sync (no_name,None,`Unknown) in
+ `Sync (no_name,`NestedProof)
+ | _ -> `Sync (no_name,`Unknown) in
let make_sync why = function
- | `Sync(name,pua,_) -> `Sync (name,pua,why)
- | `MaybeASync(_,pua,_,name,_) -> `Sync (name,pua,why)
- | `ASync(_,pua,_,name,_) -> `Sync (name,pua,why) in
+ | `Sync(name,_) -> `Sync (name,why)
+ | `MaybeASync(_,_,name,_) -> `Sync (name,why)
+ | `ASync(_,_,name,_) -> `Sync (name,why) in
+
let check_policy rc = if async_policy () then rc else make_sync `Policy rc in
match cur, (VCS.visit id).step, brkind with
| (parent, { expr = VernacExactProof _ }), `Fork _, _
| (parent, { expr = VernacTime (_, VernacExactProof _) }), `Fork _, _ ->
- `Sync (no_name,None,`Immediate)
+ `Sync (no_name,`Immediate)
| _, _, { VCS.kind = `Edit _ } -> check_policy (collect (Some cur) [] id)
| _ ->
- if is_defined cur then `Sync (no_name,None,`Transparent)
- else if keep == VtDrop then `Sync (no_name,None,`Aborted)
+ if is_defined cur then `Sync (no_name,`Transparent)
+ else if keep == VtDrop then `Sync (no_name,`Aborted)
else
let rc = collect (Some cur) [] id in
if is_empty rc then make_sync `AlreadyEvaluated rc
@@ -2222,7 +2233,7 @@ let known_state ?(redefine_qed=false) ~cache id =
), `Yes, true
| `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) ->
let rec aux = function
- | `ASync (block_start, pua, nodes, name, delegate) -> (fun () ->
+ | `ASync (block_start, nodes, name, delegate) -> (fun () ->
assert(keep == VtKeep || keep == VtKeepAsAxiom);
let drop_pt = keep == VtKeepAsAxiom in
let block_stop, exn_info, loc = eop, (id, eop), x.loc in
@@ -2269,10 +2280,10 @@ let known_state ?(redefine_qed=false) ~cache id =
end;
Proof_global.discard_all ()
), (if redefine_qed then `No else `Yes), true
- | `Sync (name, _, `Immediate) -> (fun () ->
+ | `Sync (name, `Immediate) -> (fun () ->
reach eop; stm_vernac_interp id x; Proof_global.discard_all ()
), `Yes, true
- | `Sync (name, pua, reason) -> (fun () ->
+ | `Sync (name, reason) -> (fun () ->
log_processing_sync id name reason;
reach eop;
let wall_clock = Unix.gettimeofday () in
@@ -2297,12 +2308,12 @@ let known_state ?(redefine_qed=false) ~cache id =
(Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2));
Proof_global.discard_all ()
), `Yes, true
- | `MaybeASync (start, pua, nodes, name, delegate) -> (fun () ->
+ | `MaybeASync (start, nodes, name, delegate) -> (fun () ->
reach ~cache:`Shallow start;
(* no sections *)
if CList.is_empty (Environ.named_context (Global.env ()))
- then Util.pi1 (aux (`ASync (start, pua, nodes, name, delegate))) ()
- else Util.pi1 (aux (`Sync (name, pua, `NoPU_NoHint_NoES))) ()
+ then Util.pi1 (aux (`ASync (start, nodes, name, delegate))) ()
+ else Util.pi1 (aux (`Sync (name, `NoPU_NoHint_NoES))) ()
), (if redefine_qed then `No else `Yes), true
in
aux (collect_proof keep (view.next, x) brname brinfo eop)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 7aa5114a4f..d0424eb892 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -187,35 +187,34 @@ let _ =
add_option ["Info";"Trivial"] global_info_trivial;
add_option ["Info";"Auto"] global_info_auto
-let no_dbg () = (Off,0,ref [])
+type debug_kind = ReportForTrivial | ReportForAuto
+
+let no_dbg (_,whatfor,_,_) = (Off,whatfor,0,ref [])
let mk_trivial_dbg debug =
let d =
if debug == Debug || !global_debug_trivial then Debug
else if debug == Info || !global_info_trivial then Info
else Off
- in (d,0,ref [])
-
-(** Note : we start the debug depth of auto at 1 to distinguish it
- for trivial (whose depth is 0). *)
+ in (d,ReportForTrivial,0,ref [])
let mk_auto_dbg debug =
let d =
if debug == Debug || !global_debug_auto then Debug
else if debug == Info || !global_info_auto then Info
else Off
- in (d,1,ref [])
+ in (d,ReportForAuto,0,ref [])
-let incr_dbg = function (dbg,depth,trace) -> (dbg,depth+1,trace)
+let incr_dbg = function (dbg,whatfor,depth,trace) -> (dbg,whatfor,depth+1,trace)
(** A tracing tactic for debug/info trivial/auto *)
-let tclLOG (dbg,depth,trace) pp tac =
+let tclLOG (dbg,_,depth,trace) pp tac =
match dbg with
| Off -> tac
| Debug ->
(* For "debug (trivial/auto)", we directly output messages *)
- let s = String.make depth '*' in
+ let s = String.make (depth+1) '*' in
Proofview.V82.tactic begin fun gl ->
try
let out = Proofview.V82.of_tactic tac gl in
@@ -256,23 +255,23 @@ and erase_subtree depth = function
| (d,_) :: l -> if Int.equal d depth then l else erase_subtree depth l
let pr_info_atom (d,pp) =
- str (String.make (d-1) ' ') ++ pp () ++ str "."
+ str (String.make d ' ') ++ pp () ++ str "."
let pr_info_trace = function
- | (Info,_,{contents=(d,Some pp)::l}) ->
+ | (Info,_,_,{contents=(d,Some pp)::l}) ->
Feedback.msg_info (prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l))
| _ -> ()
let pr_info_nop = function
- | (Info,_,_) -> Feedback.msg_info (str "idtac.")
+ | (Info,_,_,_) -> Feedback.msg_info (str "idtac.")
| _ -> ()
let pr_dbg_header = function
- | (Off,_,_) -> ()
- | (Debug,0,_) -> Feedback.msg_debug (str "(* debug trivial: *)")
- | (Debug,_,_) -> Feedback.msg_debug (str "(* debug auto: *)")
- | (Info,0,_) -> Feedback.msg_info (str "(* info trivial: *)")
- | (Info,_,_) -> Feedback.msg_info (str "(* info auto: *)")
+ | (Off,_,_,_) -> ()
+ | (Debug,ReportForTrivial,_,_) -> Feedback.msg_debug (str "(* debug trivial: *)")
+ | (Debug,ReportForAuto,_,_) -> Feedback.msg_debug (str "(* debug auto: *)")
+ | (Info,ReportForTrivial,_,_) -> Feedback.msg_info (str "(* info trivial: *)")
+ | (Info,ReportForAuto,_,_) -> Feedback.msg_info (str "(* info auto: *)")
let tclTRY_dbg d tac =
let delay f = Proofview.tclUNIT () >>= fun () -> f () in
@@ -382,7 +381,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
(unify_resolve_gen poly flags (c,cl))
(* With "(debug) trivial", we shouldn't end here, and
with "debug auto" we don't display the details of inner trivial *)
- (trivial_fail_db (no_dbg ()) (not (Option.is_empty flags)) db_list local_db)
+ (trivial_fail_db (no_dbg dbg) (not (Option.is_empty flags)) db_list local_db)
| Unfold_nth c ->
Proofview.Goal.enter begin fun gl ->
if exists_evaluable_reference (Tacmach.New.pf_env gl) c then
diff --git a/test-suite/bugs/closed/5692.v b/test-suite/bugs/closed/5692.v
new file mode 100644
index 0000000000..55ef7abe40
--- /dev/null
+++ b/test-suite/bugs/closed/5692.v
@@ -0,0 +1,38 @@
+Set Primitive Projections.
+Require Import ZArith ssreflect.
+
+Module Test3.
+
+Set Primitive Projections.
+
+Structure semigroup := SemiGroup {
+ sg_car :> Type;
+ sg_op : sg_car -> sg_car -> sg_car;
+}.
+
+Structure group := Something {
+ group_car :> Type;
+ group_op : group_car -> group_car -> group_car;
+ group_neg : group_car -> group_car;
+ group_neg_op' x y : group_neg (group_op x y) = group_op (group_neg x) (group_neg y)
+}.
+
+Coercion group_sg (X : group) : semigroup :=
+ SemiGroup (group_car X) (group_op X).
+Canonical Structure group_sg.
+
+Axiom group_neg_op : forall (X : group) (x y : X),
+ group_neg X (sg_op (group_sg X) x y) = sg_op (group_sg X) (group_neg X x) (group_neg X y).
+
+Canonical Structure Z_sg := SemiGroup Z Z.add .
+Canonical Structure Z_group := Something Z Z.add Z.opp Z.opp_add_distr.
+
+Lemma foo (x y : Z) :
+ sg_op Z_sg (group_neg Z_group x) (group_neg Z_group y) =
+ group_neg Z_group (sg_op Z_sg x y).
+Proof.
+ rewrite -group_neg_op.
+ reflexivity.
+Qed.
+
+End Test3.
diff --git a/test-suite/bugs/closed/5741.v b/test-suite/bugs/closed/5741.v
new file mode 100644
index 0000000000..f6598f192d
--- /dev/null
+++ b/test-suite/bugs/closed/5741.v
@@ -0,0 +1,4 @@
+(* Check no anomaly in info_trivial *)
+
+Goal True.
+info_trivial.
diff --git a/test-suite/output/auto.out b/test-suite/output/auto.out
index a5b55a9993..2761b87b02 100644
--- a/test-suite/output/auto.out
+++ b/test-suite/output/auto.out
@@ -18,3 +18,5 @@ Debug: 1 depth=5
Debug: 1.1 depth=4 simple apply or_intror
Debug: 1.1.1 depth=4 intro
Debug: 1.1.1.1 depth=4 exact H
+(* info trivial: *)
+exact I (in core).
diff --git a/test-suite/output/auto.v b/test-suite/output/auto.v
index a77b7b82e6..92917cdfc7 100644
--- a/test-suite/output/auto.v
+++ b/test-suite/output/auto.v
@@ -9,3 +9,7 @@ info_eauto.
Undo.
debug eauto.
Qed.
+
+Goal True.
+info_trivial.
+Qed.
diff --git a/test-suite/output/ltac_extra_args.out b/test-suite/output/ltac_extra_args.out
new file mode 100644
index 0000000000..77e799d359
--- /dev/null
+++ b/test-suite/output/ltac_extra_args.out
@@ -0,0 +1,8 @@
+The command has indeed failed with message:
+Illegal tactic application: got 1 extra argument.
+The command has indeed failed with message:
+Illegal tactic application: got 2 extra arguments.
+The command has indeed failed with message:
+Illegal tactic application: got 1 extra argument.
+The command has indeed failed with message:
+Illegal tactic application: got 2 extra arguments.
diff --git a/test-suite/output/ltac_extra_args.v b/test-suite/output/ltac_extra_args.v
new file mode 100644
index 0000000000..4caf619fee
--- /dev/null
+++ b/test-suite/output/ltac_extra_args.v
@@ -0,0 +1,10 @@
+Ltac foo := idtac.
+Ltac bar H := idtac.
+
+Goal True.
+Proof.
+ Fail foo H.
+ Fail foo H H'.
+ Fail bar H H'.
+ Fail bar H H' H''.
+Abort.
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index a0b6bfbbed..6ddeeb9b28 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -94,7 +94,7 @@ let rcs = "\036" rcs_keyword [^ '$']* "\036"
let stars = "(*" '*'* "*)"
let dot = '.' (' ' | '\t' | '\n' | '\r' | eof)
let proof_start =
- "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" | "Obligation" | "Next"
+ "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" | "Obligation" space+ (['0' - '9'])+ | "Next" space+ "Obligation"
let def_start =
"Definition" | "Fixpoint" | "Instance"
let proof_end =
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 4b97ee0dde..b0f021cdcd 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -132,10 +132,16 @@ let rec interp_vernac sid (loc,com) =
highly dynamic and depends on the structure of the
document. Hopefully this is fixed when VtBack can be removed
and Undo etc... are just interpreted regularly. *)
+
+ (* XXX: The classifier can emit warnings so we need to guard
+ against that... *)
+ let wflags = CWarnings.get_flags () in
+ CWarnings.set_flags "none";
let is_proof_step = match fst (Vernac_classifier.classify_vernac v) with
| VtProofStep _ | VtBack (_, _) | VtStartProof _ -> true
| _ -> false
in
+ CWarnings.set_flags wflags;
let nsid, ntip = Stm.add ~ontop:sid (not !Flags.quiet) (loc,v) in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 10:50:02 +0000