aboutsummaryrefslogtreecommitdiff
path: root/user-contrib
diff options
context:
space:
mode:
Diffstat (limited to 'user-contrib')
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg129
-rw-r--r--user-contrib/Ltac2/tac2core.ml4
-rw-r--r--user-contrib/Ltac2/tac2entries.ml29
-rw-r--r--user-contrib/Ltac2/tac2entries.mli4
4 files changed, 82 insertions, 84 deletions
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 5ae8f4ae6e..6749169e8c 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -71,8 +71,9 @@ let test_ltac1_env =
lk_ident_list >> lk_kw "|-"
end
-let tac2expr = Tac2entries.Pltac.tac2expr
-let tac2type = Entry.create "tac2type"
+let ltac2_expr = Tac2entries.Pltac.ltac2_expr
+let _ltac2_expr = ltac2_expr
+let ltac2_type = Entry.create "ltac2_type"
let tac2def_val = Entry.create "tac2def_val"
let tac2def_typ = Entry.create "tac2def_typ"
let tac2def_ext = Entry.create "tac2def_ext"
@@ -80,7 +81,7 @@ let tac2def_syn = Entry.create "tac2def_syn"
let tac2def_mut = Entry.create "tac2def_mut"
let tac2mode = Entry.create "ltac2_command"
-let ltac1_expr = Pltac.tactic_expr
+let ltac_expr = Pltac.ltac_expr
let tac2expr_in_env = Tac2entries.Pltac.tac2expr_in_env
let inj_wit wit loc x = CAst.make ~loc @@ CTacExt (wit, x)
@@ -101,7 +102,7 @@ let pattern_of_qualid qid =
}
GRAMMAR EXTEND Gram
- GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext tac2def_syn
+ GLOBAL: ltac2_expr ltac2_type tac2def_val tac2def_typ tac2def_ext tac2def_syn
tac2def_mut tac2expr_in_env;
tac2pat:
[ "1" LEFTA
@@ -125,7 +126,7 @@ GRAMMAR EXTEND Gram
atomic_tac2pat:
[ [ ->
{ CAst.make ~loc @@ CPatRef (AbsKn (Tuple 0), []) }
- | p = tac2pat; ":"; t = tac2type ->
+ | p = tac2pat; ":"; t = ltac2_type ->
{ CAst.make ~loc @@ CPatCnv (p, t) }
| p = tac2pat; ","; pl = LIST0 tac2pat SEP "," ->
{ let pl = p :: pl in
@@ -133,17 +134,17 @@ GRAMMAR EXTEND Gram
| p = tac2pat -> { p }
] ]
;
- tac2expr:
+ ltac2_expr:
[ "6" RIGHTA
[ e1 = SELF; ";"; e2 = SELF -> { CAst.make ~loc @@ CTacSeq (e1, e2) } ]
| "5"
- [ "fun"; it = LIST1 input_fun ; "=>"; body = tac2expr LEVEL "6" ->
+ [ "fun"; it = LIST1 input_fun ; "=>"; body = ltac2_expr LEVEL "6" ->
{ CAst.make ~loc @@ CTacFun (it, body) }
| "let"; isrec = rec_flag;
lc = LIST1 let_clause SEP "with"; "in";
- e = tac2expr LEVEL "6" ->
+ e = ltac2_expr LEVEL "6" ->
{ CAst.make ~loc @@ CTacLet (isrec, lc, e) }
- | "match"; e = tac2expr LEVEL "5"; "with"; bl = branches; "end" ->
+ | "match"; e = ltac2_expr LEVEL "5"; "with"; bl = branches; "end" ->
{ CAst.make ~loc @@ CTacCse (e, bl) }
]
| "4" LEFTA [ ]
@@ -151,25 +152,25 @@ GRAMMAR EXTEND Gram
{ let el = e0 :: el in
CAst.make ~loc @@ CTacApp (CAst.make ~loc @@ CTacCst (AbsKn (Tuple (List.length el))), el) } ]
| "2" RIGHTA
- [ e1 = tac2expr; "::"; e2 = tac2expr ->
+ [ e1 = ltac2_expr; "::"; e2 = ltac2_expr ->
{ CAst.make ~loc @@ CTacApp (CAst.make ~loc @@ CTacCst (AbsKn (Other Tac2core.Core.c_cons)), [e1; e2]) }
]
| "1" LEFTA
- [ e = tac2expr; el = LIST1 tac2expr LEVEL "0" ->
+ [ e = ltac2_expr; el = LIST1 ltac2_expr LEVEL "0" ->
{ CAst.make ~loc @@ CTacApp (e, el) }
| e = SELF; ".("; qid = Prim.qualid; ")" ->
{ CAst.make ~loc @@ CTacPrj (e, RelId qid) }
- | e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = tac2expr LEVEL "5" ->
+ | e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = ltac2_expr LEVEL "5" ->
{ CAst.make ~loc @@ CTacSet (e, RelId qid, r) } ]
| "0"
[ "("; a = SELF; ")" -> { a }
- | "("; a = SELF; ":"; t = tac2type; ")" ->
+ | "("; a = SELF; ":"; t = ltac2_type; ")" ->
{ CAst.make ~loc @@ CTacCnv (a, t) }
| "()" ->
{ CAst.make ~loc @@ CTacCst (AbsKn (Tuple 0)) }
| "("; ")" ->
{ CAst.make ~loc @@ CTacCst (AbsKn (Tuple 0)) }
- | "["; a = LIST0 tac2expr LEVEL "5" SEP ";"; "]" ->
+ | "["; a = LIST0 ltac2_expr LEVEL "5" SEP ";"; "]" ->
{ Tac2quote.of_list ~loc (fun x -> x) a }
| "{"; a = tac2rec_fieldexprs; "}" ->
{ CAst.make ~loc @@ CTacRec a }
@@ -183,7 +184,7 @@ GRAMMAR EXTEND Gram
]
;
branch:
- [ [ pat = tac2pat LEVEL "1"; "=>"; e = tac2expr LEVEL "6" -> { (pat, e) } ] ]
+ [ [ pat = tac2pat LEVEL "1"; "=>"; e = ltac2_expr LEVEL "6" -> { (pat, e) } ] ]
;
rec_flag:
[ [ IDENT "rec" -> { true }
@@ -193,7 +194,7 @@ GRAMMAR EXTEND Gram
[ [ IDENT "mutable" -> { true }
| -> { false } ] ]
;
- typ_param:
+ ltac2_typevar:
[ [ "'"; id = Prim.ident -> { id } ] ]
;
tactic_atom:
@@ -210,19 +211,19 @@ GRAMMAR EXTEND Gram
| IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> { Tac2quote.of_constr c }
| IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> { Tac2quote.of_open_constr c }
| IDENT "ident"; ":"; "("; c = lident; ")" -> { Tac2quote.of_ident c }
- | IDENT "pattern"; ":"; "("; c = Constr.lconstr_pattern; ")" -> { inj_pattern loc c }
+ | IDENT "pattern"; ":"; "("; c = Constr.cpattern; ")" -> { inj_pattern loc c }
| IDENT "reference"; ":"; "("; c = globref; ")" -> { inj_reference loc c }
| IDENT "ltac1"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1 loc qid }
| IDENT "ltac1val"; ":"; "("; qid = ltac1_expr_in_env; ")" -> { inj_ltac1val loc qid }
] ]
;
ltac1_expr_in_env:
- [ [ test_ltac1_env; ids = LIST0 locident; "|-"; e = ltac1_expr -> { ids, e }
- | e = ltac1_expr -> { [], e }
+ [ [ test_ltac1_env; ids = LIST0 locident; "|-"; e = ltac_expr -> { ids, e }
+ | e = ltac_expr -> { [], e }
] ]
;
tac2expr_in_env :
- [ [ test_ltac1_env; ids = LIST0 locident; "|-"; e = tac2expr ->
+ [ [ test_ltac1_env; ids = LIST0 locident; "|-"; e = ltac2_expr ->
{ let check { CAst.v = id; CAst.loc = loc } =
if Tac2env.is_constructor (Libnames.qualid_of_ident ?loc id) then
CErrors.user_err ?loc Pp.(str "Invalid bound Ltac2 identifier " ++ Id.print id)
@@ -230,11 +231,11 @@ GRAMMAR EXTEND Gram
let () = List.iter check ids in
(ids, e)
}
- | tac = tac2expr -> { [], tac }
+ | tac = ltac2_expr -> { [], tac }
] ]
;
let_clause:
- [ [ binder = let_binder; ":="; te = tac2expr ->
+ [ [ binder = let_binder; ":="; te = ltac2_expr ->
{ let (pat, fn) = binder in
let te = match fn with
| None -> te
@@ -252,23 +253,23 @@ GRAMMAR EXTEND Gram
| _ -> CErrors.user_err ~loc (str "Invalid pattern") }
] ]
;
- tac2type:
+ ltac2_type:
[ "5" RIGHTA
- [ t1 = tac2type; "->"; t2 = tac2type -> { CAst.make ~loc @@ CTypArrow (t1, t2) } ]
+ [ t1 = ltac2_type; "->"; t2 = ltac2_type -> { CAst.make ~loc @@ CTypArrow (t1, t2) } ]
| "2"
- [ t = tac2type; "*"; tl = LIST1 tac2type LEVEL "1" SEP "*" ->
+ [ t = ltac2_type; "*"; tl = LIST1 ltac2_type LEVEL "1" SEP "*" ->
{ let tl = t :: tl in
CAst.make ~loc @@ CTypRef (AbsKn (Tuple (List.length tl)), tl) } ]
| "1" LEFTA
[ t = SELF; qid = Prim.qualid -> { CAst.make ~loc @@ CTypRef (RelId qid, [t]) } ]
| "0"
- [ "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = OPT Prim.qualid ->
+ [ "("; p = LIST1 ltac2_type LEVEL "5" SEP ","; ")"; qid = OPT Prim.qualid ->
{ match p, qid with
| [t], None -> t
| _, None -> CErrors.user_err ~loc (Pp.str "Syntax error")
| ts, Some qid -> CAst.make ~loc @@ CTypRef (RelId qid, p)
}
- | id = typ_param -> { CAst.make ~loc @@ CTypVar (Name id) }
+ | id = ltac2_typevar -> { CAst.make ~loc @@ CTypVar (Name id) }
| "_" -> { CAst.make ~loc @@ CTypVar Anonymous }
| qid = Prim.qualid -> { CAst.make ~loc @@ CTypRef (RelId qid, []) }
]
@@ -284,7 +285,7 @@ GRAMMAR EXTEND Gram
[ [ b = tac2pat LEVEL "0" -> { b } ] ]
;
tac2def_body:
- [ [ name = binder; it = LIST0 input_fun; ":="; e = tac2expr ->
+ [ [ name = binder; it = LIST0 input_fun; ":="; e = ltac2_expr ->
{ let e = if List.is_empty it then e else CAst.make ~loc @@ CTacFun (it, e) in
(name, e) }
] ]
@@ -295,10 +296,10 @@ GRAMMAR EXTEND Gram
] ]
;
tac2def_mut:
- [ [ "Set"; qid = Prim.qualid; old = OPT [ "as"; id = locident -> { id } ]; ":="; e = tac2expr -> { StrMut (qid, old, e) } ] ]
+ [ [ "Set"; qid = Prim.qualid; old = OPT [ "as"; id = locident -> { id } ]; ":="; e = ltac2_expr -> { StrMut (qid, old, e) } ] ]
;
tac2typ_knd:
- [ [ t = tac2type -> { CTydDef (Some t) }
+ [ [ t = ltac2_type -> { CTydDef (Some t) }
| "["; ".."; "]" -> { CTydOpn }
| "["; t = tac2alg_constructors; "]" -> { CTydAlg t }
| "{"; t = tac2rec_fields; "}"-> { CTydRec t } ] ]
@@ -309,7 +310,7 @@ GRAMMAR EXTEND Gram
;
tac2alg_constructor:
[ [ c = Prim.ident -> { (c, []) }
- | c = Prim.ident; "("; args = LIST0 tac2type SEP ","; ")"-> { (c, args) } ] ]
+ | c = Prim.ident; "("; args = LIST0 ltac2_type SEP ","; ")"-> { (c, args) } ] ]
;
tac2rec_fields:
[ [ f = tac2rec_field; ";"; l = tac2rec_fields -> { f :: l }
@@ -318,7 +319,7 @@ GRAMMAR EXTEND Gram
| -> { [] } ] ]
;
tac2rec_field:
- [ [ mut = mut_flag; id = Prim.ident; ":"; t = tac2type -> { (id, mut, t) } ] ]
+ [ [ mut = mut_flag; id = Prim.ident; ":"; t = ltac2_type -> { (id, mut, t) } ] ]
;
tac2rec_fieldexprs:
[ [ f = tac2rec_fieldexpr; ";"; l = tac2rec_fieldexprs -> { f :: l }
@@ -327,12 +328,12 @@ GRAMMAR EXTEND Gram
| -> { [] } ] ]
;
tac2rec_fieldexpr:
- [ [ qid = Prim.qualid; ":="; e = tac2expr LEVEL "1" -> { RelId qid, e } ] ]
+ [ [ qid = Prim.qualid; ":="; e = ltac2_expr LEVEL "1" -> { RelId qid, e } ] ]
;
tac2typ_prm:
[ [ -> { [] }
- | id = typ_param -> { [CAst.make ~loc id] }
- | "("; ids = LIST1 [ id = typ_param -> { CAst.make ~loc id } ] SEP "," ;")" -> { ids }
+ | id = ltac2_typevar -> { [CAst.make ~loc id] }
+ | "("; ids = LIST1 [ id = ltac2_typevar -> { CAst.make ~loc id } ] SEP "," ;")" -> { ids }
] ]
;
tac2typ_def:
@@ -350,7 +351,7 @@ GRAMMAR EXTEND Gram
] ]
;
tac2def_ext:
- [ [ "@"; IDENT "external"; id = locident; ":"; t = tac2type LEVEL "5"; ":=";
+ [ [ "@"; IDENT "external"; id = locident; ":"; t = ltac2_type LEVEL "5"; ":=";
plugin = Prim.string; name = Prim.string ->
{ let ml = { mltac_plugin = plugin; mltac_tactic = name } in
StrPrm (id, t, ml) }
@@ -361,11 +362,11 @@ GRAMMAR EXTEND Gram
| id = Prim.ident -> { CAst.make ~loc (Some id) }
] ]
;
- sexpr:
+ ltac2_scope:
[ [ s = Prim.string -> { SexprStr (CAst.make ~loc s) }
| n = Prim.integer -> { SexprInt (CAst.make ~loc n) }
| id = syn_node -> { SexprRec (loc, id, []) }
- | id = syn_node; "("; tok = LIST1 sexpr SEP "," ; ")" ->
+ | id = syn_node; "("; tok = LIST1 ltac2_scope SEP "," ; ")" ->
{ SexprRec (loc, id, tok) }
] ]
;
@@ -375,8 +376,8 @@ GRAMMAR EXTEND Gram
] ]
;
tac2def_syn:
- [ [ "Notation"; toks = LIST1 sexpr; n = syn_level; ":=";
- e = tac2expr ->
+ [ [ "Notation"; toks = LIST1 ltac2_scope; n = syn_level; ":=";
+ e = ltac2_expr ->
{ StrSyn (toks, n, e) }
] ]
;
@@ -497,7 +498,7 @@ GRAMMAR EXTEND Gram
;
simple_intropattern:
[ [ pat = simple_intropattern_closed ->
-(* l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] -> *)
+(* l = LIST0 ["%"; c = term LEVEL "0" -> c] -> *)
(** TODO: handle %pat *)
{ pat }
] ]
@@ -654,26 +655,26 @@ GRAMMAR EXTEND Gram
[ [ r = oriented_rewriter -> { r } ] ]
;
tactic_then_last:
- [ [ "|"; lta = LIST0 (OPT tac2expr LEVEL "6") SEP "|" -> { lta }
+ [ [ "|"; lta = LIST0 (OPT ltac2_expr LEVEL "6") SEP "|" -> { lta }
| -> { [] }
] ]
;
- tactic_then_gen:
- [ [ ta = tac2expr; "|"; tg = tactic_then_gen -> { let (first,last) = tg in (Some ta :: first, last) }
- | ta = tac2expr; ".."; l = tactic_then_last -> { ([], Some (Some ta, l)) }
+ for_each_goal:
+ [ [ ta = ltac2_expr; "|"; tg = for_each_goal -> { let (first,last) = tg in (Some ta :: first, last) }
+ | ta = ltac2_expr; ".."; l = tactic_then_last -> { ([], Some (Some ta, l)) }
| ".."; l = tactic_then_last -> { ([], Some (None, l)) }
- | ta = tac2expr -> { ([Some ta], None) }
- | "|"; tg = tactic_then_gen -> { let (first,last) = tg in (None :: first, last) }
+ | ta = ltac2_expr -> { ([Some ta], None) }
+ | "|"; tg = for_each_goal -> { let (first,last) = tg in (None :: first, last) }
| -> { ([None], None) }
] ]
;
q_dispatch:
- [ [ d = tactic_then_gen -> { CAst.make ~loc d } ] ]
+ [ [ d = for_each_goal -> { CAst.make ~loc d } ] ]
;
q_occurrences:
[ [ occs = occs -> { occs } ] ]
;
- red_flag:
+ ltac2_red_flag:
[ [ IDENT "beta" -> { CAst.make ~loc @@ QBeta }
| IDENT "iota" -> { CAst.make ~loc @@ QIota }
| IDENT "match" -> { CAst.make ~loc @@ QMatch }
@@ -702,7 +703,7 @@ GRAMMAR EXTEND Gram
] ]
;
strategy_flag:
- [ [ s = LIST1 red_flag -> { CAst.make ~loc s }
+ [ [ s = LIST1 ltac2_red_flag -> { CAst.make ~loc s }
| d = delta_flag ->
{ CAst.make ~loc
[CAst.make ~loc QBeta; CAst.make ~loc QIota; CAst.make ~loc QZeta; d] }
@@ -721,11 +722,11 @@ GRAMMAR EXTEND Gram
;
match_pattern:
[ [ IDENT "context"; id = OPT Prim.ident;
- "["; pat = Constr.lconstr_pattern; "]" -> { CAst.make ~loc @@ QConstrMatchContext (id, pat) }
- | pat = Constr.lconstr_pattern -> { CAst.make ~loc @@ QConstrMatchPattern pat } ] ]
+ "["; pat = Constr.cpattern; "]" -> { CAst.make ~loc @@ QConstrMatchContext (id, pat) }
+ | pat = Constr.cpattern -> { CAst.make ~loc @@ QConstrMatchPattern pat } ] ]
;
match_rule:
- [ [ mp = match_pattern; "=>"; tac = tac2expr ->
+ [ [ mp = match_pattern; "=>"; tac = ltac2_expr ->
{ CAst.make ~loc @@ (mp, tac) }
] ]
;
@@ -748,16 +749,16 @@ GRAMMAR EXTEND Gram
] ]
;
gmatch_rule:
- [ [ mp = gmatch_pattern; "=>"; tac = tac2expr ->
+ [ [ mp = gmatch_pattern; "=>"; tac = ltac2_expr ->
{ CAst.make ~loc @@ (mp, tac) }
] ]
;
- gmatch_list:
+ goal_match_list:
[ [ mrl = LIST1 gmatch_rule SEP "|" -> { CAst.make ~loc @@ mrl }
| "|"; mrl = LIST1 gmatch_rule SEP "|" -> { CAst.make ~loc @@ mrl } ] ]
;
q_goal_matching:
- [ [ m = gmatch_list -> { m } ] ]
+ [ [ m = goal_match_list -> { m } ] ]
;
move_location:
[ [ "at"; IDENT "top" -> { CAst.make ~loc @@ QMoveFirst }
@@ -789,7 +790,7 @@ GRAMMAR EXTEND Gram
] ]
;
by_tactic:
- [ [ "by"; tac = tac2expr -> { Some tac }
+ [ [ "by"; tac = ltac2_expr -> { Some tac }
| -> { None }
] ]
;
@@ -812,8 +813,8 @@ END
(*
GRAMMAR EXTEND Gram
- Pcoq.Constr.operconstr: LEVEL "0"
- [ [ IDENT "ltac2"; ":"; "("; tac = tac2expr; ")" ->
+ Pcoq.Constr.term: LEVEL "0"
+ [ [ IDENT "ltac2"; ":"; "("; tac = ltac2_expr; ")" ->
{ let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_constr) tac in
CAst.make ~loc (CHole (None, Namegen.IntroAnonymous, Some arg)) }
| test_ampersand_ident; "&"; id = Prim.ident ->
@@ -858,7 +859,7 @@ let rules = [
Pcoq.(
Production.make
(Rule.stop ++ Symbol.token (PIDENT (Some "ltac2")) ++ Symbol.token (PKEYWORD ":") ++
- Symbol.token (PKEYWORD "(") ++ Symbol.nterm tac2expr ++ Symbol.token (PKEYWORD ")"))
+ Symbol.token (PKEYWORD "(") ++ Symbol.nterm ltac2_expr ++ 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))
@@ -867,7 +868,7 @@ let rules = [
] in
Hook.set Tac2entries.register_constr_quotations begin fun () ->
- Pcoq.grammar_extend Pcoq.Constr.operconstr {pos=Some (Gramlib.Gramext.Level "0"); data=[(None, None, rules)]}
+ Pcoq.grammar_extend Pcoq.Constr.term {pos=Some (Gramlib.Gramext.Level "0"); data=[(None, None, rules)]}
end
}
@@ -890,7 +891,7 @@ END
VERNAC ARGUMENT EXTEND ltac2_expr
PRINTED BY { pr_ltac2expr }
-| [ tac2expr(e) ] -> { e }
+| [ _ltac2_expr(e) ] -> { e }
END
{
@@ -920,10 +921,10 @@ open Vernacextend
}
VERNAC { tac2mode } EXTEND VernacLtac2
-| ![proof] [ ltac2_expr(t) ltac_use_default(default) ] =>
+| ![proof] [ ltac2_expr(t) ltac_use_default(with_end_tac) ] =>
{ classify_as_proofstep } -> {
(* let g = Option.default (Proof_global.get_default_goal_selector ()) g in *)
- fun ~pstate -> Tac2entries.call ~pstate ~default t }
+ fun ~pstate -> Tac2entries.call ~pstate ~with_end_tac t }
END
GRAMMAR EXTEND Gram
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 3ce50865c0..5d49d1635c 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1541,12 +1541,12 @@ end
let () = add_scope "tactic" begin function
| [] ->
(* Default to level 5 parsing *)
- let scope = Pcoq.Symbol.nterml tac2expr "5" in
+ let scope = Pcoq.Symbol.nterml ltac2_expr "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 = Pcoq.Symbol.nterml tac2expr (string_of_int n) in
+ let scope = Pcoq.Symbol.nterml ltac2_expr (string_of_int n) in
let act tac = tac in
Tac2entries.ScopeRule (scope, act)
| arg -> scope_fail "tactic" arg
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 30340cd632..eebd6635fa 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -24,7 +24,8 @@ open Tac2intern
module Pltac =
struct
-let tac2expr = Pcoq.Entry.create "tac2expr"
+let ltac2_expr = Pcoq.Entry.create "ltac2_expr"
+let tac2expr = ltac2_expr
let tac2expr_in_env = Pcoq.Entry.create "tac2expr_in_env"
let q_ident = Pcoq.Entry.create "q_ident"
@@ -643,7 +644,7 @@ let perform_notation syn st =
| Some lev -> Some (string_of_int lev)
in
let rule = (lev, None, [rule]) in
- ([Pcoq.ExtendRule (Pltac.tac2expr, {Pcoq.pos=None; data=[rule]})], st)
+ ([Pcoq.ExtendRule (Pltac.ltac2_expr, {Pcoq.pos=None; data=[rule]})], st)
let ltac2_notation =
Pcoq.create_grammar_command "ltac2-notation" perform_notation
@@ -911,25 +912,19 @@ let print_ltac qid =
(** Calling tactics *)
-let solve ~pstate default tac =
- let pstate, status = Declare.Proof.map_fold_endline pstate ~f:(fun etac p ->
- let with_end_tac = if default then Some etac else None in
- let g = Goal_select.get_default_goal_selector () in
- let (p, status) = Proof.solve g None tac ?with_end_tac p in
- (* in case a strict subtree was completed,
- go back to the top of the prooftree *)
- let p = Proof.maximal_unfocus Vernacentries.command_focus p in
- p, status)
- in
- if not status then Feedback.feedback Feedback.AddedAxiom;
- pstate
-
-let call ~pstate ~default e =
+let ltac2_interp e =
let loc = e.loc in
let (e, t) = intern ~strict:false [] e in
let () = check_unit ?loc t in
let tac = Tac2interp.interp Tac2interp.empty_environment e in
- solve ~pstate default (Proofview.tclIGNORE tac)
+ Proofview.tclIGNORE tac
+
+let ComTactic.Interpreter ltac2_interp = ComTactic.register_tactic_interpreter "ltac2" ltac2_interp
+
+let call ~pstate ~with_end_tac tac =
+ ComTactic.solve ~pstate ~with_end_tac
+ (Goal_select.get_default_goal_selector())
+ ~info:None (ltac2_interp tac)
(** Primitive algebraic types than can't be defined Coq-side *)
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index fc56a54e3a..782968c6e1 100644
--- a/user-contrib/Ltac2/tac2entries.mli
+++ b/user-contrib/Ltac2/tac2entries.mli
@@ -53,7 +53,7 @@ val print_ltac : Libnames.qualid -> unit
(** {5 Eval loop} *)
(** Evaluate a tactic expression in the current environment *)
-val call : pstate:Declare.Proof.t -> default:bool -> raw_tacexpr -> Declare.Proof.t
+val call : pstate:Declare.Proof.t -> with_end_tac:bool -> raw_tacexpr -> Declare.Proof.t
(** {5 Toplevel exceptions} *)
@@ -63,7 +63,9 @@ val backtrace : backtrace Exninfo.t
module Pltac :
sig
+val ltac2_expr : raw_tacexpr Pcoq.Entry.t
val tac2expr : raw_tacexpr Pcoq.Entry.t
+ [@@deprecated "Deprecated in 8.13; use 'ltac2_expr' instead"]
val tac2expr_in_env : (Id.t CAst.t list * raw_tacexpr) Pcoq.Entry.t
(** Quoted entries. To be used for complex notations. *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 06:41:58 +0000