aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--clib/exninfo.ml10
-rw-r--r--clib/exninfo.mli3
-rw-r--r--coqpp/coqpp_main.ml2
-rw-r--r--doc/sphinx/proof-engine/ltac2.rst10
-rw-r--r--engine/logic_monad.ml5
-rw-r--r--engine/logic_monad.mli2
-rw-r--r--engine/proofview.ml2
-rw-r--r--ide/idetop.ml2
-rw-r--r--parsing/pcoq.ml52
-rw-r--r--parsing/pcoq.mli5
-rw-r--r--plugins/ltac/tacentries.ml6
-rw-r--r--plugins/ltac/tactic_debug.ml30
-rw-r--r--test-suite/bugs/closed/bug_11549.v5
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg14
-rw-r--r--user-contrib/Ltac2/tac2core.ml2
-rw-r--r--user-contrib/Ltac2/tac2entries.ml2
-rw-r--r--vernac/egramcoq.ml67
-rw-r--r--vernac/egramml.ml2
-rw-r--r--vernac/pvernac.ml2
-rw-r--r--vernac/vernacextend.ml2
20 files changed, 131 insertions, 94 deletions
diff --git a/clib/exninfo.ml b/clib/exninfo.ml
index ee998c2f17..34a4555a9a 100644
--- a/clib/exninfo.ml
+++ b/clib/exninfo.ml
@@ -81,16 +81,6 @@ let iraise (e,i) =
| Some bt ->
Printexc.raise_with_backtrace e bt
-let raise ?info e = match info with
-| None ->
- let () = Mutex.lock lock in
- let id = Thread.id (Thread.self ()) in
- let () = current := remove_assoc id !current in
- let () = Mutex.unlock lock in
- raise e
-| Some i ->
- iraise (e,i)
-
let find_and_remove () =
let () = Mutex.lock lock in
let id = Thread.id (Thread.self ()) in
diff --git a/clib/exninfo.mli b/clib/exninfo.mli
index 36cc44cf82..725cd82809 100644
--- a/clib/exninfo.mli
+++ b/clib/exninfo.mli
@@ -79,6 +79,3 @@ val capture : exn -> iexn
val iraise : iexn -> 'a
(** Raise the given enriched exception. *)
-
-val raise : ?info:info -> exn -> 'a
-(** Raise the given exception with additional information. *)
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 72b7cb2f84..e723d4ea1b 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -266,7 +266,7 @@ let print_rule fmt r =
let print_entry fmt e =
let print_position_opt fmt pos = print_opt fmt print_position pos in
let print_rules fmt rules = print_list fmt print_rule rules in
- fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ None@ @[(%a, %a)@]@]@ in@ "
+ fprintf fmt "let () =@ @[Pcoq.grammar_extend@ %s@ @[(%a, %a)@]@]@ in@ "
e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules
let print_ast fmt ext =
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index b722b1af74..9362a7729e 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -3,10 +3,6 @@
Ltac2
=====
-.. coqtop:: none
-
- From Ltac2 Require Import Ltac2.
-
The Ltac tactic language is probably one of the ingredients of the success of
Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac:
@@ -88,6 +84,12 @@ which allows to ensure that Ltac2 satisfies the same equations as a generic ML
with unspecified effects would do, e.g. function reduction is substitution
by a value.
+To import Ltac2, use the following command:
+
+.. coqtop:: in
+
+ From Ltac2 Require Import Ltac2.
+
Type Syntax
~~~~~~~~~~~
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 605877cfba..1caf2c2722 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -83,7 +83,7 @@ struct
(** [Pervasives.raise]. Except that exceptions are wrapped with
{!Exception}. *)
- let raise ?info = fun e -> (); fun () -> Exninfo.raise ?info (Exception e)
+ let raise (e, info) () = Exninfo.iraise (Exception e, info)
(** [try ... with ...] but restricted to {!Exception}. *)
let catch = fun s h -> ();
@@ -93,7 +93,8 @@ struct
h (e, info) ()
let read_line = fun () -> try read_line () with e ->
- let (e, info) = CErrors.push e in raise ~info e ()
+ let (e, info) = CErrors.push e in
+ raise (e, info) ()
let print_char = fun c -> (); fun () -> print_char c
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index 75920455ce..5002d24af0 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -70,7 +70,7 @@ module NonLogical : sig
(** [Pervasives.raise]. Except that exceptions are wrapped with
{!Exception}. *)
- val raise : ?info:Exninfo.info -> exn -> 'a t
+ val raise : Exninfo.iexn -> 'a t
(** [try ... with ...] but restricted to {!Exception}. *)
val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 31e4dae2de..a26ce71141 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -938,7 +938,7 @@ let tclTIMEOUT n t =
return (Util.Inr (Logic_monad.Tac_Timeout, info))
| Logic_monad.TacticFailure e ->
return (Util.Inr (e, info))
- | e -> Logic_monad.NonLogical.raise ~info e
+ | e -> Logic_monad.NonLogical.raise (e, info)
end
end >>= function
| Util.Inl (res,s,m,i) ->
diff --git a/ide/idetop.ml b/ide/idetop.ml
index ae2301a0a7..60036ef876 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -70,7 +70,7 @@ let ide_cmd_checks ~last_valid { CAst.loc; v } =
with e ->
let (e, info) = CErrors.push e in
let info = Stateid.add info ~valid:last_valid Stateid.dummy in
- Exninfo.raise ~info e
+ Exninfo.iraise (e, info)
in
if is_debug v.expr then
user_error "Debug mode not available in the IDE"
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 26afdcb9d5..92c3b7c6e8 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -212,7 +212,8 @@ type 'a extend_statement =
'a single_extend_statement list
type extend_rule =
-| ExtendRule : 'a G.Entry.e * gram_reinit option * 'a extend_statement -> extend_rule
+| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule
+| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule
module EntryCommand = Dyn.Make ()
module EntryData = struct type _ t = Ex : 'b G.Entry.e String.Map.t -> ('a * 'b) t end
@@ -231,33 +232,39 @@ let camlp5_entries = ref EntryDataMap.empty
(** Deletion *)
-let grammar_delete e reinit (pos,rls) =
+let grammar_delete e (pos,rls) =
List.iter
(fun (n,ass,lev) ->
List.iter (fun (AnyProduction (pil,_)) -> G.safe_delete_rule e pil) (List.rev lev))
- (List.rev rls);
- match reinit with
- | Some (a,ext) ->
- let lev = match pos with
+ (List.rev rls)
+
+let grammar_delete_reinit e reinit (pos, rls) =
+ grammar_delete e (pos, rls);
+ let a, ext = reinit in
+ let lev = match pos with
| Some (Gramext.Level n) -> n
| _ -> assert false
- in
- let warning msg = Feedback.msg_warning Pp.(str msg) in
- (G.safe_extend ~warning:(Some warning) e) (Some ext) [Some lev,Some a,[]]
- | None -> ()
+ in
+ let warning msg = Feedback.msg_warning Pp.(str msg) in
+ (G.safe_extend ~warning:(Some warning) e) (Some ext) [Some lev,Some a,[]]
(** Extension *)
-let grammar_extend e reinit ext =
+let grammar_extend e ext =
let ext = of_coq_extend_statement ext in
- let undo () = grammar_delete e reinit ext in
+ let undo () = grammar_delete e ext in
let pos, ext = fix_extend_statement ext in
let redo () = G.safe_extend ~warning:None e pos ext in
camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state;
redo ()
-let grammar_extend_sync e reinit ext =
- camlp5_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp5_state;
+let grammar_extend_sync e ext =
+ camlp5_state := ByGrammar (ExtendRule (e, ext)) :: !camlp5_state;
+ let pos, ext = fix_extend_statement (of_coq_extend_statement ext) in
+ G.safe_extend ~warning:None e pos ext
+
+let grammar_extend_sync_reinit e reinit ext =
+ camlp5_state := ByGrammar (ExtendRuleReinit (e, reinit, ext)) :: !camlp5_state;
let pos, ext = fix_extend_statement (of_coq_extend_statement ext) in
G.safe_extend ~warning:None e pos ext
@@ -278,8 +285,12 @@ let rec remove_grammars n =
if n>0 then
match !camlp5_state with
| [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove.")
- | ByGrammar (ExtendRule (g, reinit, ext)) :: t ->
- grammar_delete g reinit (of_coq_extend_statement ext);
+ | ByGrammar (ExtendRuleReinit (g, reinit, ext)) :: t ->
+ grammar_delete_reinit g reinit (of_coq_extend_statement ext);
+ camlp5_state := t;
+ remove_grammars (n-1)
+ | ByGrammar (ExtendRule (g, ext)) :: t ->
+ grammar_delete g (of_coq_extend_statement ext);
camlp5_state := t;
remove_grammars (n-1)
| ByEXTEND (undo,redo)::t ->
@@ -507,6 +518,12 @@ let create_entry_command name (interp : ('a, 'b) entry_extension) : ('a, 'b) ent
let () = entry_interp := EntryInterpMap.add obj (EntryInterp.Ex interp) !entry_interp in
obj
+let iter_extend_sync = function
+ | ExtendRule (e, ext) ->
+ grammar_extend_sync e ext
+ | ExtendRuleReinit (e, reinit, ext) ->
+ grammar_extend_sync_reinit e reinit ext
+
let extend_grammar_command tag g =
let modify = GrammarInterpMap.find tag !grammar_interp in
let grammar_state = match !grammar_stack with
@@ -514,8 +531,7 @@ let extend_grammar_command tag g =
| (_, st) :: _ -> st
in
let (rules, st) = modify g grammar_state in
- let iter (ExtendRule (e, reinit, ext)) = grammar_extend_sync e reinit ext in
- let () = List.iter iter rules in
+ let () = List.iter iter_extend_sync rules in
let nb = List.length rules in
grammar_stack := (GramExt (nb, GrammarCommand.Dyn (tag, g)), st) :: !grammar_stack
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 404fbdb4fd..f2fc007a7b 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -225,7 +225,7 @@ type 'a extend_statement =
Gramlib.Gramext.position option *
'a single_extend_statement list
-val grammar_extend : 'a Entry.t -> gram_reinit option -> 'a extend_statement -> unit
+val grammar_extend : 'a Entry.t -> 'a extend_statement -> unit
(** Extend the grammar of Coq, without synchronizing it with the backtracking
mechanism. This means that grammar extensions defined this way will survive
an undo. *)
@@ -242,7 +242,8 @@ type 'a grammar_command
marshallable. *)
type extend_rule =
-| ExtendRule : 'a Entry.t * gram_reinit option * 'a extend_statement -> extend_rule
+| ExtendRule : 'a Entry.t * 'a extend_statement -> extend_rule
+| ExtendRuleReinit : 'a Entry.t * gram_reinit * 'a extend_statement -> extend_rule
type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t
(** Grammar extension entry point. Given some ['a] and a current grammar state,
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 13a2f3b8c0..8b4520947b 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -191,7 +191,7 @@ let add_tactic_entry (kn, ml, tg) state =
in
let prods = List.map map tg.tacgram_prods in
let rules = make_rule mkact prods in
- let r = ExtendRule (entry, None, (pos, [(None, None, [rules])])) in
+ let r = ExtendRule (entry, (pos, [(None, None, [rules])])) in
([r], state)
let tactic_grammar =
@@ -415,7 +415,7 @@ let create_ltac_quotation name cast (e, l) =
in
let action _ v _ _ _ loc = cast (Some loc, v) in
let gram = (level, assoc, [Rule (rule, action)]) in
- Pcoq.grammar_extend Pltac.tactic_arg None (None, [gram])
+ Pcoq.grammar_extend Pltac.tactic_arg (None, [gram])
(** Command *)
@@ -759,7 +759,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) =
e
| Vernacextend.Arg_rules rules ->
let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
- let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in
+ let () = Pcoq.grammar_extend e (None, [(None, None, rules)]) in
e
in
let (rpr, gpr, tpr) = arg.arg_printer in
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 0e9465839a..392f9b2ffd 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -107,13 +107,29 @@ let db_initialize =
let int_of_string s =
try Proofview.NonLogical.return (int_of_string s)
- with e -> Proofview.NonLogical.raise e
+ with e ->
+ let e = Exninfo.capture e in
+ Proofview.NonLogical.raise e
let string_get s i =
try Proofview.NonLogical.return (String.get s i)
- with e -> Proofview.NonLogical.raise e
+ with e ->
+ let e = Exninfo.capture e in
+ Proofview.NonLogical.raise e
+
+let check_positive n =
+ try
+ if n < 0 then
+ raise (Invalid_argument "number must be positive")
+ else
+ Proofview.NonLogical.return ()
+ with e ->
+ let e = Exninfo.capture e in
+ Proofview.NonLogical.raise e
-let run_invalid_arg () = Proofview.NonLogical.raise (Invalid_argument "run_com")
+let run_invalid_arg () =
+ let info = Exninfo.null in
+ Proofview.NonLogical.raise (Invalid_argument "run_com", info)
(* Gives the number of steps or next breakpoint of a run command *)
let run_com inst =
@@ -125,7 +141,7 @@ let run_com inst =
let s = String.sub inst i (String.length inst - i) in
if inst.[0] >= '0' && inst.[0] <= '9' then
int_of_string s >>= fun num ->
- (if num<0 then run_invalid_arg () else return ()) >>
+ check_positive num >>
(skip:=num) >> (skipped:=0)
else
breakpoint:=Some (possibly_unquote s)
@@ -156,11 +172,11 @@ let rec prompt level =
let open Proofview.NonLogical in
Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >>
if Util.(!batch) then return (DebugOn (level+1)) else
- let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in
+ let exit = (skip:=0) >> (skipped:=0) >> raise (Sys.Break, Exninfo.null) in
Proofview.NonLogical.catch Proofview.NonLogical.read_line
begin function (e, info) -> match e with
| End_of_file -> exit
- | e -> raise ~info e
+ | e -> raise (e, info)
end
>>= fun inst ->
match inst with
@@ -176,7 +192,7 @@ let rec prompt level =
Proofview.NonLogical.catch (run_com inst >> runtrue >> return (DebugOn (level+1)))
begin function (e, info) -> match e with
| Failure _ | Invalid_argument _ -> prompt level
- | e -> raise ~info e
+ | e -> raise (e, info)
end
end
diff --git a/test-suite/bugs/closed/bug_11549.v b/test-suite/bugs/closed/bug_11549.v
new file mode 100644
index 0000000000..7608e1c4d8
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11549.v
@@ -0,0 +1,5 @@
+From Ltac2 Require Ltac2.
+
+Notation "t $ r" := (t r)
+ (at level 65, right associativity, only parsing).
+Check S $ O.
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index d05640f22d..e95ac3b02b 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -25,6 +25,10 @@ let err () = raise Stream.Failure
type lookahead = Gramlib.Plexing.location_function -> int -> Tok.t Stream.t -> int option
+let check_no_space tok m strm =
+ let n = Stream.count strm in
+ if G_prim.contiguous tok n (n+m-1) then Some m else None
+
let entry_of_lookahead s (lk : lookahead) =
let run tok strm = match lk tok 0 strm with None -> err () | Some _ -> () in
Pcoq.Entry.of_parser s run
@@ -51,7 +55,7 @@ let lk_int tok n strm = match stream_nth n strm with
| NUMERAL { NumTok.int = _; frac = ""; exp = "" } -> Some (n + 1)
| _ -> None
-let lk_ident_or_anti = lk_ident <+> (lk_kw "$" >> lk_ident)
+let lk_ident_or_anti = lk_ident <+> (lk_kw "$" >> lk_ident >> check_no_space)
let rec lk_ident_list n strm =
((lk_ident >> lk_ident_list) <+> lk_empty) n strm
@@ -80,10 +84,6 @@ let test_lpar_id_rpar =
lk_kw "(" >> lk_ident >> lk_kw ")"
end
-let check_no_space tok m strm =
- let n = Stream.count strm in
- if G_prim.contiguous tok n (n+m-1) then Some m else None
-
let test_ampersand_ident =
entry_of_lookahead "test_ampersand_ident" begin
lk_kw "&" >> lk_ident >> check_no_space
@@ -91,7 +91,7 @@ let test_ampersand_ident =
let test_dollar_ident =
entry_of_lookahead "test_dollar_ident" begin
- lk_kw "$" >> lk_ident
+ lk_kw "$" >> lk_ident >> check_no_space
end
let test_ltac1_env =
@@ -889,7 +889,7 @@ let rules = [
] in
Hook.set Tac2entries.register_constr_quotations begin fun () ->
- Pcoq.grammar_extend Pcoq.Constr.operconstr None (Some (Gramlib.Gramext.Level "0"), [(None, None, rules)])
+ Pcoq.grammar_extend Pcoq.Constr.operconstr (Some (Gramlib.Gramext.Level "0"), [(None, None, rules)])
end
}
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 431589aa30..196b28b274 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -161,7 +161,7 @@ let set_bt info =
let throw ?(info = Exninfo.null) e =
set_bt info >>= fun info ->
let info = Exninfo.add info fatal_flag () in
- Proofview.tclLIFT (Proofview.NonLogical.raise ~info e)
+ Proofview.tclLIFT (Proofview.NonLogical.raise (e, info))
let fail ?(info = Exninfo.null) e =
set_bt info >>= fun info ->
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index a8bf4bc96f..2a0c109a42 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -643,7 +643,7 @@ let perform_notation syn st =
| Some lev -> Some (string_of_int lev)
in
let rule = (lev, None, [rule]) in
- ([Pcoq.ExtendRule (Pltac.tac2expr, None, (None, [rule]))], st)
+ ([Pcoq.ExtendRule (Pltac.tac2expr, (None, [rule]))], st)
let ltac2_notation =
Pcoq.create_grammar_command "ltac2-notation" perform_notation
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 72e6d41969..ead86bd12f 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -96,38 +96,38 @@ let create_pos = function
let find_position_gen current ensure assoc lev =
match lev with
| None ->
- current, (None, None, None, None)
+ current, (None, None, None, None)
| Some n ->
- let after = ref None in
- let init = ref None in
- let rec add_level q = function
- | (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l
- | (p,a,reinit)::l when Int.equal p n ->
- if reinit then
- let a' = create_assoc assoc in
- (init := Some (a',create_pos q); (p,a',false)::l)
- else if admissible_assoc (a,assoc) then
- raise Exit
- else
- error_level_assoc p a (Option.get assoc)
- | l -> after := q; (n,create_assoc assoc,ensure)::l
- in
- try
- let updated = add_level None current in
- let assoc = create_assoc assoc in
- begin match !init with
+ let after = ref None in
+ let init = ref None in
+ let rec add_level q = function
+ | (p,_,_ as pa)::l when p > n -> pa :: add_level (Some p) l
+ | (p,a,reinit)::l when Int.equal p n ->
+ if reinit then
+ let a' = create_assoc assoc in
+ (init := Some (a',create_pos q); (p,a',false)::l)
+ else if admissible_assoc (a,assoc) then
+ raise Exit
+ else
+ error_level_assoc p a (Option.get assoc)
+ | l -> after := q; (n,create_assoc assoc,ensure)::l
+ in
+ try
+ let updated = add_level None current in
+ let assoc = create_assoc assoc in
+ begin match !init with
| None ->
(* Create the entry *)
- updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None)
+ updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None)
| _ ->
(* The reinit flag has been updated *)
- updated, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, !init)
- end
- with
- (* Nothing has changed *)
- Exit ->
- (* Just inherit the existing associativity and name (None) *)
- current, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, None)
+ updated, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, !init)
+ end
+ with
+ (* Nothing has changed *)
+ Exit ->
+ (* Just inherit the existing associativity and name (None) *)
+ current, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, None)
let rec list_mem_assoc_triple x = function
| [] -> false
@@ -505,7 +505,11 @@ let target_to_bool : type r. r target -> bool = function
let prepare_empty_levels forpat (where,(pos,p4assoc,name,reinit)) =
let empty = (pos, [(name, p4assoc, [])]) in
- ExtendRule (target_entry where forpat, reinit, empty)
+ match reinit with
+ | None ->
+ ExtendRule (target_entry where forpat, empty)
+ | Some reinit ->
+ ExtendRuleReinit (target_entry where forpat, reinit, empty)
let different_levels (custom,opt_level) (custom',string_level) =
match opt_level with
@@ -552,7 +556,12 @@ let extend_constr state forpat ng =
| MayRecRNo symbs -> Rule (symbs, act)
| MayRecRMay symbs -> Rule (symbs, act) in
name, p4assoc, [r] in
- let r = ExtendRule (entry, reinit, (pos, [rule])) in
+ let r = match reinit with
+ | None ->
+ ExtendRule (entry, (pos, [rule]))
+ | Some reinit ->
+ ExtendRuleReinit (entry, reinit, (pos, [rule]))
+ in
(accu @ empty_rules @ [r], state)
in
List.fold_left fold ([], state) ng.notgram_prods
diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index 62eb561f3c..2b1d99c7a9 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -90,4 +90,4 @@ let extend_vernac_command_grammar s nt gl =
vernac_exts := (s,gl) :: !vernac_exts;
let mkact loc l = VernacExtend (s, l) in
let rules = [make_rule mkact gl] in
- grammar_extend nt None (None, [None, None, rules])
+ grammar_extend nt (None, [None, None, rules])
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index 826e88cabf..2425f3d6c1 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -58,7 +58,7 @@ module Vernac_ =
Rule (Next (Stop, Atoken Tok.PEOI), act_eoi);
Rule (Next (Stop, Aentry vernac_control), act_vernac);
] in
- Pcoq.grammar_extend main_entry None (None, [None, None, rule])
+ Pcoq.grammar_extend main_entry (None, [None, None, rule])
let select_tactic_entry spec =
match spec with
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index e29086d726..f41df06f85 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -254,7 +254,7 @@ let vernac_argument_extend ~name arg =
e
| Arg_rules rules ->
let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
- let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in
+ let () = Pcoq.grammar_extend e (None, [(None, None, rules)]) in
e
in
let pr = arg.arg_printer in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 23:42:02 +0000