aboutsummaryrefslogtreecommitdiff
path: root/user-contrib
diff options
context:
space:
mode:
Diffstat (limited to 'user-contrib')
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg22
-rw-r--r--user-contrib/Ltac2/tac2core.ml79
-rw-r--r--user-contrib/Ltac2/tac2entries.ml16
-rw-r--r--user-contrib/Ltac2/tac2entries.mli2
-rw-r--r--user-contrib/Ltac2/tac2tactics.ml2
5 files changed, 52 insertions, 69 deletions
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 5e04959e9a..57d59fc2ef 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -826,12 +826,12 @@ END
let () =
-let open Extend in
let open Tok in
-let (++) r s = Next (r, s) in
+let (++) r s = Pcoq.Rule.next r s in
let rules = [
- Rule (
- Stop ++ Aentry test_dollar_ident ++ Atoken (PKEYWORD "$") ++ Aentry Prim.ident,
+ Pcoq.(
+ Production.make
+ (Rule.stop ++ Symbol.nterm test_dollar_ident ++ Symbol.token (PKEYWORD "$") ++ Symbol.nterm Prim.ident)
begin fun id _ _ loc ->
let id = Loc.tag ~loc id in
let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_quotation) id in
@@ -839,8 +839,9 @@ let rules = [
end
);
- Rule (
- Stop ++ Aentry test_ampersand_ident ++ Atoken (PKEYWORD "&") ++ Aentry Prim.ident,
+ Pcoq.(
+ Production.make
+ (Rule.stop ++ Symbol.nterm test_ampersand_ident ++ Symbol.token (PKEYWORD "&") ++ Symbol.nterm Prim.ident)
begin fun id _ _ loc ->
let tac = Tac2quote.of_exact_hyp ~loc (CAst.make ~loc id) in
let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in
@@ -848,9 +849,10 @@ let rules = [
end
);
- Rule (
- Stop ++ Atoken (PIDENT (Some "ltac2")) ++ Atoken (PKEYWORD ":") ++
- Atoken (PKEYWORD "(") ++ Aentry tac2expr ++ Atoken (PKEYWORD ")"),
+ Pcoq.(
+ Production.make
+ (Rule.stop ++ Symbol.token (PIDENT (Some "ltac2")) ++ Symbol.token (PKEYWORD ":") ++
+ Symbol.token (PKEYWORD "(") ++ Symbol.nterm tac2expr ++ Symbol.token (PKEYWORD ")"))
begin fun _ tac _ _ _ loc ->
let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in
CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg))
@@ -859,7 +861,7 @@ let rules = [
] in
Hook.set Tac2entries.register_constr_quotations begin fun () ->
- Pcoq.grammar_extend Pcoq.Constr.operconstr (Some (Gramlib.Gramext.Level "0"), [(None, None, rules)])
+ Pcoq.grammar_extend Pcoq.Constr.operconstr {pos=Some (Gramlib.Gramext.Level "0"); data=[(None, None, rules)]}
end
}
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 38b05bed6b..72df4d75c8 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -20,7 +20,7 @@ open Proofview.Notations
let constr_flags =
let open Pretyping in
{
- use_typeclasses = true;
+ use_typeclasses = Pretyping.UseTC;
solve_unification_constraints = true;
fail_evar = true;
expand_evars = true;
@@ -31,7 +31,7 @@ let constr_flags =
let open_constr_no_classes_flags =
let open Pretyping in
{
- use_typeclasses = false;
+ use_typeclasses = Pretyping.NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
@@ -1431,7 +1431,7 @@ let q_unit = CAst.make @@ CTacCst (AbsKn (Tuple 0))
let add_generic_scope s entry arg =
let parse = function
| [] ->
- let scope = Extend.Aentry entry in
+ let scope = Pcoq.Symbol.nterm entry in
let act x = CAst.make @@ CTacExt (arg, x) in
Tac2entries.ScopeRule (scope, act)
| arg -> scope_fail s arg
@@ -1442,14 +1442,14 @@ open CAst
let () = add_scope "keyword" begin function
| [SexprStr {loc;v=s}] ->
- let scope = Extend.Atoken (Tok.PKEYWORD s) in
+ let scope = Pcoq.Symbol.token (Tok.PKEYWORD s) in
Tac2entries.ScopeRule (scope, (fun _ -> q_unit))
| arg -> scope_fail "keyword" arg
end
let () = add_scope "terminal" begin function
| [SexprStr {loc;v=s}] ->
- let scope = Extend.Atoken (CLexer.terminal s) in
+ let scope = Pcoq.Symbol.token (CLexer.terminal s) in
Tac2entries.ScopeRule (scope, (fun _ -> q_unit))
| arg -> scope_fail "terminal" arg
end
@@ -1457,13 +1457,13 @@ end
let () = add_scope "list0" begin function
| [tok] ->
let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
- let scope = Extend.Alist0 scope in
+ let scope = Pcoq.Symbol.list0 scope in
let act l = Tac2quote.of_list act l in
Tac2entries.ScopeRule (scope, act)
| [tok; SexprStr {v=str}] ->
let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
- let sep = Extend.Atoken (CLexer.terminal str) in
- let scope = Extend.Alist0sep (scope, sep) in
+ let sep = Pcoq.Symbol.token (CLexer.terminal str) in
+ let scope = Pcoq.Symbol.list0sep scope sep false in
let act l = Tac2quote.of_list act l in
Tac2entries.ScopeRule (scope, act)
| arg -> scope_fail "list0" arg
@@ -1472,13 +1472,13 @@ end
let () = add_scope "list1" begin function
| [tok] ->
let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
- let scope = Extend.Alist1 scope in
+ let scope = Pcoq.Symbol.list1 scope in
let act l = Tac2quote.of_list act l in
Tac2entries.ScopeRule (scope, act)
| [tok; SexprStr {v=str}] ->
let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
- let sep = Extend.Atoken (CLexer.terminal str) in
- let scope = Extend.Alist1sep (scope, sep) in
+ let sep = Pcoq.Symbol.token (CLexer.terminal str) in
+ let scope = Pcoq.Symbol.list1sep scope sep false in
let act l = Tac2quote.of_list act l in
Tac2entries.ScopeRule (scope, act)
| arg -> scope_fail "list1" arg
@@ -1487,7 +1487,7 @@ end
let () = add_scope "opt" begin function
| [tok] ->
let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
- let scope = Extend.Aopt scope in
+ let scope = Pcoq.Symbol.opt scope in
let act opt = match opt with
| None ->
CAst.make @@ CTacCst (AbsKn (Other Core.c_none))
@@ -1500,7 +1500,7 @@ end
let () = add_scope "self" begin function
| [] ->
- let scope = Extend.Aself in
+ let scope = Pcoq.Symbol.self in
let act tac = tac in
Tac2entries.ScopeRule (scope, act)
| arg -> scope_fail "self" arg
@@ -1508,7 +1508,7 @@ end
let () = add_scope "next" begin function
| [] ->
- let scope = Extend.Anext in
+ let scope = Pcoq.Symbol.next in
let act tac = tac in
Tac2entries.ScopeRule (scope, act)
| arg -> scope_fail "next" arg
@@ -1517,12 +1517,12 @@ end
let () = add_scope "tactic" begin function
| [] ->
(* Default to level 5 parsing *)
- let scope = Extend.Aentryl (tac2expr, "5") in
+ let scope = Pcoq.Symbol.nterml tac2expr "5" in
let act tac = tac in
Tac2entries.ScopeRule (scope, act)
| [SexprInt {loc;v=n}] as arg ->
let () = if n < 0 || n > 6 then scope_fail "tactic" arg in
- let scope = Extend.Aentryl (tac2expr, string_of_int n) in
+ let scope = Pcoq.Symbol.nterml tac2expr (string_of_int n) in
let act tac = tac in
Tac2entries.ScopeRule (scope, act)
| arg -> scope_fail "tactic" arg
@@ -1543,12 +1543,12 @@ let () = add_scope "constr" (fun arg ->
arg
in
let act e = Tac2quote.of_constr ~delimiters e in
- Tac2entries.ScopeRule (Extend.Aentry Pcoq.Constr.constr, act)
+ Tac2entries.ScopeRule (Pcoq.Symbol.nterm Pcoq.Constr.constr, act)
)
let add_expr_scope name entry f =
add_scope name begin function
- | [] -> Tac2entries.ScopeRule (Extend.Aentry entry, f)
+ | [] -> Tac2entries.ScopeRule (Pcoq.Symbol.nterm entry, f)
| arg -> scope_fail name arg
end
@@ -1578,28 +1578,7 @@ let () = add_generic_scope "pattern" Pcoq.Constr.constr Tac2quote.wit_pattern
(** seq scope, a bit hairy *)
-open Extend
-exception SelfSymbol
-
-let rec generalize_symbol :
- type a tr s. (s, tr, a) Extend.symbol -> (s, Extend.norec, a) Extend.symbol = function
-| Atoken tok -> Atoken tok
-| Alist1 e -> Alist1 (generalize_symbol e)
-| Alist1sep (e, sep) ->
- let e = generalize_symbol e in
- let sep = generalize_symbol sep in
- Alist1sep (e, sep)
-| Alist0 e -> Alist0 (generalize_symbol e)
-| Alist0sep (e, sep) ->
- let e = generalize_symbol e in
- let sep = generalize_symbol sep in
- Alist0sep (e, sep)
-| Aopt e -> Aopt (generalize_symbol e)
-| Aself -> raise SelfSymbol
-| Anext -> raise SelfSymbol
-| Aentry e -> Aentry e
-| Aentryl (e, l) -> Aentryl (e, l)
-| Arules r -> Arules r
+open Pcoq
type _ converter =
| CvNil : (Loc.t -> raw_tacexpr) converter
@@ -1611,16 +1590,21 @@ let rec apply : type a. a converter -> raw_tacexpr list -> a = function
| CvCns (c, Some f) -> fun accu x -> apply c (f x :: accu)
type seqrule =
-| Seqrule : (Tac2expr.raw_tacexpr, Extend.norec, 'act, Loc.t -> raw_tacexpr) rule * 'act converter -> seqrule
+| Seqrule : (Tac2expr.raw_tacexpr, Gramlib.Grammar.norec, 'act, Loc.t -> raw_tacexpr) Rule.t * 'act converter -> seqrule
let rec make_seq_rule = function
| [] ->
- Seqrule (Stop, CvNil)
+ Seqrule (Pcoq.Rule.stop, CvNil)
| tok :: rem ->
let Tac2entries.ScopeRule (scope, f) = Tac2entries.parse_scope tok in
- let scope = generalize_symbol scope in
+ let scope =
+ match Pcoq.generalize_symbol scope with
+ | None ->
+ CErrors.user_err (str "Recursive symbols (self / next) are not allowed in local rules")
+ | Some scope -> scope
+ in
let Seqrule (r, c) = make_seq_rule rem in
- let r = NextNoRec (r, scope) in
+ let r = Pcoq.Rule.next_norec r scope in
let f = match tok with
| SexprStr _ -> None (* Leave out mere strings *)
| _ -> Some f
@@ -1629,11 +1613,8 @@ let rec make_seq_rule = function
let () = add_scope "seq" begin fun toks ->
let scope =
- try
- let Seqrule (r, c) = make_seq_rule (List.rev toks) in
- Arules [Rules (r, apply c [])]
- with SelfSymbol ->
- CErrors.user_err (str "Recursive symbols (self / next) are not allowed in local rules")
+ let Seqrule (r, c) = make_seq_rule (List.rev toks) in
+ Pcoq.(Symbol.rules [Rules.make r (apply c [])])
in
Tac2entries.ScopeRule (scope, (fun e -> e))
end
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index e9945794d3..ebc63ddd01 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -558,7 +558,7 @@ type 'a token =
| TacNonTerm of Name.t * 'a
type scope_rule =
-| ScopeRule : (raw_tacexpr, _, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule
+| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.Symbol.t * ('a -> raw_tacexpr) -> scope_rule
type scope_interpretation = sexpr list -> scope_rule
@@ -583,7 +583,7 @@ let parse_scope = function
CErrors.user_err ?loc (str "Unknown scope" ++ spc () ++ Names.Id.print id)
| SexprStr {v=str} ->
let v_unit = CAst.make @@ CTacCst (AbsKn (Tuple 0)) in
- ScopeRule (Extend.Atoken (Tok.PIDENT (Some str)), (fun _ -> v_unit))
+ ScopeRule (Pcoq.Symbol.token (Tok.PIDENT (Some str)), (fun _ -> v_unit))
| tok ->
let loc = loc_of_token tok in
CErrors.user_err ?loc (str "Invalid parsing token")
@@ -611,19 +611,19 @@ type synext = {
type krule =
| KRule :
- (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Extend.rule *
+ (raw_tacexpr, _, 'act, Loc.t -> raw_tacexpr) Pcoq.Rule.t *
((Loc.t -> (Name.t * raw_tacexpr) list -> raw_tacexpr) -> 'act) -> krule
let rec get_rule (tok : scope_rule token list) : krule = match tok with
-| [] -> KRule (Extend.Stop, fun k loc -> k loc [])
+| [] -> KRule (Pcoq.Rule.stop, fun k loc -> k loc [])
| TacNonTerm (na, ScopeRule (scope, inj)) :: tok ->
let KRule (rule, act) = get_rule tok in
- let rule = Extend.Next (rule, scope) in
+ let rule = Pcoq.Rule.next rule scope in
let act k e = act (fun loc acc -> k loc ((na, inj e) :: acc)) in
KRule (rule, act)
| TacTerm t :: tok ->
let KRule (rule, act) = get_rule tok in
- let rule = Extend.Next (rule, Extend.Atoken (CLexer.terminal t)) in
+ let rule = Pcoq.(Rule.next rule (Symbol.token (CLexer.terminal t))) in
let act k _ = act k in
KRule (rule, act)
@@ -637,13 +637,13 @@ let perform_notation syn st =
let bnd = List.map map args in
CAst.make ~loc @@ CTacLet (false, bnd, syn.synext_exp)
in
- let rule = Extend.Rule (rule, act mk) in
+ let rule = Pcoq.Production.make rule (act mk) in
let lev = match syn.synext_lev with
| None -> None
| Some lev -> Some (string_of_int lev)
in
let rule = (lev, None, [rule]) in
- ([Pcoq.ExtendRule (Pltac.tac2expr, (None, [rule]))], st)
+ ([Pcoq.ExtendRule (Pltac.tac2expr, {Pcoq.pos=None; data=[rule]})], st)
let ltac2_notation =
Pcoq.create_grammar_command "ltac2-notation" perform_notation
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index fed43a4dd5..edad118dc9 100644
--- a/user-contrib/Ltac2/tac2entries.mli
+++ b/user-contrib/Ltac2/tac2entries.mli
@@ -36,7 +36,7 @@ val perform_eval : pstate:Proof_global.t option -> raw_tacexpr -> unit
(** {5 Notations} *)
type scope_rule =
-| ScopeRule : (raw_tacexpr, _, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule
+| ScopeRule : (raw_tacexpr, _, 'a) Pcoq.Symbol.t * ('a -> raw_tacexpr) -> scope_rule
type scope_interpretation = sexpr list -> scope_rule
diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml
index 30ee1a0b4c..9ca38d64df 100644
--- a/user-contrib/Ltac2/tac2tactics.ml
+++ b/user-contrib/Ltac2/tac2tactics.ml
@@ -20,7 +20,7 @@ let return = Proofview.tclUNIT
let thaw r f = Tac2ffi.app_fun1 f Tac2ffi.unit r ()
let tactic_infer_flags with_evar = {
- Pretyping.use_typeclasses = true;
+ Pretyping.use_typeclasses = Pretyping.UseTC;
Pretyping.solve_unification_constraints = true;
Pretyping.fail_evar = not with_evar;
Pretyping.expand_evars = true;
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 07:39:44 +0000