aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extratactics.mlg12
-rw-r--r--plugins/ltac/g_auto.mlg2
-rw-r--r--plugins/ltac/g_ltac.mlg12
-rw-r--r--plugins/ltac/g_tactic.mlg8
-rw-r--r--plugins/ltac/tacentries.ml52
-rw-r--r--plugins/ltac/tacinterp.ml8
-rw-r--r--plugins/ltac/tactic_option.ml9
7 files changed, 45 insertions, 58 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 9b80cbd803..7b1aa7a07a 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -47,7 +47,7 @@ DECLARE PLUGIN "ltac_plugin"
let with_delayed_uconstr ist c tac =
let flags = {
- Pretyping.use_typeclasses = false;
+ Pretyping.use_typeclasses = Pretyping.NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
@@ -345,7 +345,7 @@ open EConstr
open Vars
let constr_flags () = {
- Pretyping.use_typeclasses = true;
+ Pretyping.use_typeclasses = Pretyping.UseTC;
Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics ();
Pretyping.fail_evar = false;
Pretyping.expand_evars = true;
@@ -375,22 +375,22 @@ let refine_tac ist simple with_classes c =
TACTIC EXTEND refine
| [ "refine" uconstr(c) ] ->
- { refine_tac ist false true c }
+ { refine_tac ist false Pretyping.UseTC c }
END
TACTIC EXTEND simple_refine
| [ "simple" "refine" uconstr(c) ] ->
- { refine_tac ist true true c }
+ { refine_tac ist true Pretyping.UseTC c }
END
TACTIC EXTEND notcs_refine
| [ "notypeclasses" "refine" uconstr(c) ] ->
- { refine_tac ist false false c }
+ { refine_tac ist false Pretyping.NoUseTC c }
END
TACTIC EXTEND notcs_simple_refine
| [ "simple" "notypeclasses" "refine" uconstr(c) ] ->
- { refine_tac ist true false c }
+ { refine_tac ist true Pretyping.NoUseTC c }
END
(* Solve unification constraints using heuristics or fail if any remain *)
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 3c30c881fb..b4527694ae 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -53,7 +53,7 @@ END
let eval_uconstrs ist cs =
let flags = {
- Pretyping.use_typeclasses = false;
+ Pretyping.use_typeclasses = Pretyping.NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 50c3ed1248..2bd4211c90 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -359,21 +359,15 @@ open Vernacextend
open Goptions
open Libnames
-let print_info_trace = ref None
-
-let () = declare_int_option {
- optdepr = false;
- optkey = ["Info" ; "Level"];
- optread = (fun () -> !print_info_trace);
- optwrite = fun n -> print_info_trace := n;
-}
+let print_info_trace =
+ declare_intopt_option_and_ref ~depr:false ~key:["Info" ; "Level"]
let vernac_solve ~pstate n info tcom b =
let open Goal_select in
let pstate, status = Proof_global.map_fold_proof_endline (fun etac p ->
let with_end_tac = if b then Some etac else None in
let global = match n with SelectAll | SelectList _ -> true | _ -> false in
- let info = Option.append info !print_info_trace in
+ let info = Option.append info (print_info_trace ()) in
let (p,status) =
Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
in
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 5a26ac8827..6a158bde17 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -185,10 +185,6 @@ let merge_occurrences loc cl = function
in
(Some p, ans)
-let warn_deprecated_eqn_syntax =
- CWarnings.create ~name:"deprecated-eqn-syntax" ~category:"deprecated"
- (fun arg -> strbrk (Printf.sprintf "Syntax \"_eqn:%s\" is deprecated. Please use \"eqn:%s\" instead." arg arg))
-
(* Auxiliary grammar rules *)
open Pvernac.Vernac_
@@ -461,10 +457,6 @@ GRAMMAR EXTEND Gram
;
eqn_ipat:
[ [ IDENT "eqn"; ":"; pat = naming_intropattern -> { Some (CAst.make ~loc pat) }
- | IDENT "_eqn"; ":"; pat = naming_intropattern ->
- { warn_deprecated_eqn_syntax ~loc "H"; Some (CAst.make ~loc pat) }
- | IDENT "_eqn" ->
- { warn_deprecated_eqn_syntax ~loc "?"; Some (CAst.make ~loc IntroAnonymous) }
| -> { None } ] ]
;
as_name:
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 4af5699317..4127d28bae 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -44,11 +44,11 @@ let coincide s pat off =
!break
let atactic n =
- if n = 5 then Aentry Pltac.binder_tactic
- else Aentryl (Pltac.tactic_expr, string_of_int n)
+ if n = 5 then Pcoq.Symbol.nterm Pltac.binder_tactic
+ else Pcoq.Symbol.nterml Pltac.tactic_expr (string_of_int n)
type entry_name = EntryName :
- 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Extend.symbol -> entry_name
+ 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.Symbol.t -> entry_name
(** Quite ad-hoc *)
let get_tacentry n m =
@@ -57,8 +57,8 @@ let get_tacentry n m =
&& not (Int.equal m 5) (* Because tactic5 is at binder_tactic *)
&& not (Int.equal m 0) (* Because tactic0 is at simple_tactic *)
in
- if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Aself)
- else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Anext)
+ if check_lvl n then EntryName (rawwit Tacarg.wit_tactic, Pcoq.Symbol.self)
+ else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Pcoq.Symbol.next)
else EntryName (rawwit Tacarg.wit_tactic, atactic n)
let get_separator = function
@@ -140,23 +140,23 @@ let head_is_ident tg = match tg.tacgram_prods with
let rec prod_item_of_symbol lev = function
| Extend.Ulist1 s ->
let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
- EntryName (Rawwit (ListArg typ), Alist1 e)
+ EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list1 e)
| Extend.Ulist0 s ->
let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
- EntryName (Rawwit (ListArg typ), Alist0 e)
+ EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list0 e)
| Extend.Ulist1sep (s, sep) ->
let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
- EntryName (Rawwit (ListArg typ), Alist1sep (e, Atoken (CLexer.terminal sep)))
+ EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list1sep e (Pcoq.Symbol.token (CLexer.terminal sep)) false)
| Extend.Ulist0sep (s, sep) ->
let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
- EntryName (Rawwit (ListArg typ), Alist0sep (e, Atoken (CLexer.terminal sep)))
+ EntryName (Rawwit (ListArg typ), Pcoq.Symbol.list0sep e (Pcoq.Symbol.token (CLexer.terminal sep)) false)
| Extend.Uopt s ->
let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in
- EntryName (Rawwit (OptArg typ), Aopt e)
+ EntryName (Rawwit (OptArg typ), Pcoq.Symbol.opt e)
| Extend.Uentry arg ->
let ArgT.Any tag = arg in
let wit = ExtraArg tag in
- EntryName (Rawwit wit, Extend.Aentry (genarg_grammar wit))
+ EntryName (Rawwit wit, Pcoq.Symbol.nterm (genarg_grammar wit))
| Extend.Uentryl (s, n) ->
let ArgT.Any tag = s in
assert (coincide (ArgT.repr tag) "tactic" 0);
@@ -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, (pos, [(None, None, [rules])])) in
+ let r = ExtendRule (entry, { pos; data=[(None, None, [rules])]}) in
([r], state)
let tactic_grammar =
@@ -399,23 +399,29 @@ let create_ltac_quotation name cast (e, l) =
in
let () = ltac_quotations := String.Set.add name !ltac_quotations in
let entry = match l with
- | None -> Aentry e
- | Some l -> Aentryl (e, string_of_int l)
+ | None -> Pcoq.Symbol.nterm e
+ | Some l -> Pcoq.Symbol.nterml e (string_of_int l)
in
(* let level = Some "1" in *)
let level = None in
let assoc = None in
let rule =
- Next (Next (Next (Next (Next (Stop,
- Atoken (CLexer.terminal name)),
- Atoken (CLexer.terminal ":")),
- Atoken (CLexer.terminal "(")),
- entry),
- Atoken (CLexer.terminal ")"))
+ Pcoq.(
+ Rule.next
+ (Rule.next
+ (Rule.next
+ (Rule.next
+ (Rule.next
+ Rule.stop
+ (Symbol.token (CLexer.terminal name)))
+ (Symbol.token (CLexer.terminal ":")))
+ (Symbol.token (CLexer.terminal "(")))
+ entry)
+ (Symbol.token (CLexer.terminal ")")))
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, [gram])
+ let gram = (level, assoc, [Pcoq.Production.make rule action]) in
+ Pcoq.grammar_extend Pltac.tactic_arg {pos=None; data=[gram]}
(** Command *)
@@ -759,7 +765,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, rules)]) in
+ let () = Pcoq.grammar_extend e {pos=None; data=[(None, None, rules)]} in
e
in
let (rpr, gpr, tpr) = arg.arg_printer in
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 9e0b9d3254..b0e26e1def 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -546,7 +546,7 @@ let interp_gen kind ist pattern_mode flags env sigma c =
(evd,c)
let constr_flags () = {
- use_typeclasses = true;
+ use_typeclasses = UseTC;
solve_unification_constraints = true;
fail_evar = true;
expand_evars = true;
@@ -564,7 +564,7 @@ let interp_constr = interp_constr_gen WithoutTypeConstraint
let interp_type = interp_constr_gen IsType
let open_constr_use_classes_flags () = {
- use_typeclasses = true;
+ use_typeclasses = UseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
@@ -573,7 +573,7 @@ let open_constr_use_classes_flags () = {
}
let open_constr_no_classes_flags () = {
- use_typeclasses = false;
+ use_typeclasses = NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
@@ -582,7 +582,7 @@ let open_constr_no_classes_flags () = {
}
let pure_open_constr_flags = {
- use_typeclasses = false;
+ use_typeclasses = NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = false;
diff --git a/plugins/ltac/tactic_option.ml b/plugins/ltac/tactic_option.ml
index c72a527537..4f00f17892 100644
--- a/plugins/ltac/tactic_option.ml
+++ b/plugins/ltac/tactic_option.ml
@@ -13,15 +13,11 @@ open Pp
let declare_tactic_option ?(default=Tacexpr.TacId []) name =
let locality = Summary.ref false ~name:(name^"-locality") in
- let default_tactic_expr : Tacexpr.glob_tactic_expr ref =
- Summary.ref default ~name:(name^"-default-tacexpr")
- in
let default_tactic : Tacexpr.glob_tactic_expr ref =
- Summary.ref !default_tactic_expr ~name:(name^"-default-tactic")
+ Summary.ref default ~name:(name^"-default-tactic")
in
let set_default_tactic local t =
locality := local;
- default_tactic_expr := t;
default_tactic := t
in
let cache (_, (local, tac)) = set_default_tactic local tac in
@@ -42,12 +38,11 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name =
subst_function = subst}
in
let put local tac =
- set_default_tactic local tac;
Lib.add_anonymous_leaf (input (local, tac))
in
let get () = !locality, Tacinterp.eval_tactic !default_tactic in
let print () =
- Pptactic.pr_glob_tactic (Global.env ()) !default_tactic_expr ++
+ Pptactic.pr_glob_tactic (Global.env ()) !default_tactic ++
(if !locality then str" (locally defined)" else str" (globally defined)")
in
put, get, print
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 11:36:42 +0000