aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/coretactics.mlg2
-rw-r--r--plugins/ltac/extraargs.mlg6
-rw-r--r--plugins/ltac/extratactics.mlg4
-rw-r--r--plugins/ltac/g_auto.mlg2
-rw-r--r--plugins/ltac/g_class.mlg12
-rw-r--r--plugins/ltac/g_ltac.mlg179
-rw-r--r--plugins/ltac/g_obligations.mlg2
-rw-r--r--plugins/ltac/g_rewrite.mlg23
-rw-r--r--plugins/ltac/g_tactic.mlg16
-rw-r--r--plugins/ltac/pltac.ml6
-rw-r--r--plugins/ltac/pltac.mli4
-rw-r--r--plugins/ltac/pptactic.ml10
-rw-r--r--plugins/ltac/pptactic.mli2
-rw-r--r--plugins/ltac/profile_ltac.ml4
-rw-r--r--plugins/ltac/rewrite.ml88
-rw-r--r--plugins/ltac/rewrite.mli2
-rw-r--r--plugins/ltac/taccoerce.ml37
-rw-r--r--plugins/ltac/tacentries.ml118
-rw-r--r--plugins/ltac/tacentries.mli3
-rw-r--r--plugins/ltac/tacintern.ml34
-rw-r--r--plugins/ltac/tacintern.mli3
-rw-r--r--plugins/ltac/tacinterp.ml51
-rw-r--r--plugins/ltac/tacinterp.mli9
-rw-r--r--plugins/ltac/tacsubst.ml2
24 files changed, 295 insertions, 324 deletions
diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg
index f1f538ab39..b7ac71181a 100644
--- a/plugins/ltac/coretactics.mlg
+++ b/plugins/ltac/coretactics.mlg
@@ -20,8 +20,6 @@ open Tacarg
open Names
open Logic
-let wit_hyp = wit_var
-
}
DECLARE PLUGIN "ltac_plugin"
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index 863c4d37d8..ff4a82f864 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -41,13 +41,13 @@ let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_simpl
let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Stdarg.wit_open_constr
let () =
let inject (loc, v) = Tacexpr.Tacexp v in
- Tacentries.create_ltac_quotation "ltac" inject (Pltac.tactic_expr, Some 5)
+ Tacentries.create_ltac_quotation "ltac" inject (Pltac.ltac_expr, Some 5)
(** Backward-compatible tactic notation entry names *)
let () =
let register name entry = Tacentries.register_tactic_notation_entry name entry in
- register "hyp" wit_var;
+ register "hyp" wit_hyp;
register "simple_intropattern" wit_simple_intropattern;
register "integer" wit_integer;
register "reference" wit_ref;
@@ -140,7 +140,7 @@ ARGUMENT EXTEND occurrences
GLOB_PRINTED BY { pr_occurrences }
| [ ne_integer_list(l) ] -> { ArgArg l }
-| [ var(id) ] -> { ArgVar id }
+| [ hyp(id) ] -> { ArgVar id }
END
{
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 4f20e5a800..a2a47c0bf4 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -33,8 +33,6 @@ open Proofview.Notations
open Attributes
open Vernacextend
-let wit_hyp = wit_var
-
}
DECLARE PLUGIN "ltac_plugin"
@@ -450,7 +448,7 @@ END
(* Subst *)
TACTIC EXTEND subst
-| [ "subst" ne_var_list(l) ] -> { subst l }
+| [ "subst" ne_hyp_list(l) ] -> { subst l }
| [ "subst" ] -> { subst_all () }
END
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 2e72ceae5a..44472a1995 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -18,8 +18,6 @@ open Pcoq.Constr
open Pltac
open Hints
-let wit_hyp = wit_var
-
}
DECLARE PLUGIN "ltac_plugin"
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 8d197e6056..8c2e633be5 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -31,12 +31,12 @@ let set_transparency cl b =
}
VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF
-| [ "Typeclasses" "Transparent" reference_list(cl) ] -> {
+| [ "Typeclasses" "Transparent" ne_reference_list(cl) ] -> {
set_transparency cl true }
END
VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings CLASSIFIED AS SIDEFF
-| [ "Typeclasses" "Opaque" reference_list(cl) ] -> {
+| [ "Typeclasses" "Opaque" ne_reference_list(cl) ] -> {
set_transparency cl false }
END
@@ -77,7 +77,7 @@ END
(* true = All transparent, false = Opaque if possible *)
VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
- | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) integer_opt(depth) ] -> {
+ | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) natural_opt(depth) ] -> {
set_typeclasses_debug d;
Option.iter set_typeclasses_strategy s;
set_typeclasses_depth depth
@@ -87,11 +87,13 @@ END
(** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *)
TACTIC EXTEND typeclasses_eauto
| [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
- { typeclasses_eauto ~strategy:Bfs ~depth:d l }
+ { typeclasses_eauto ~depth:d ~strategy:Bfs l }
| [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
{ typeclasses_eauto ~depth:d l }
+ | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) ] -> {
+ typeclasses_eauto ~depth:d ~strategy:Bfs ~only_classes:true [Class_tactics.typeclasses_db] }
| [ "typeclasses" "eauto" int_or_var_opt(d) ] -> {
- typeclasses_eauto ~only_classes:true ~depth:d [Class_tactics.typeclasses_db] }
+ typeclasses_eauto ~depth:d ~only_classes:true [Class_tactics.typeclasses_db] }
END
TACTIC EXTEND head_of_constr
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index be0d71ad46..c54f8ffa78 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -74,22 +74,22 @@ let hint = G_proofs.hint
}
GRAMMAR EXTEND Gram
- GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint
+ GLOBAL: tactic tacdef_body ltac_expr binder_tactic tactic_value command hint
tactic_mode constr_may_eval constr_eval toplevel_selector
- operconstr;
+ term;
tactic_then_last:
- [ [ "|"; lta = LIST0 (OPT tactic_expr) SEP "|" ->
+ [ [ "|"; lta = LIST0 (OPT ltac_expr) SEP "|" ->
{ Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta) }
| -> { [||] }
] ]
;
- tactic_then_gen:
- [ [ ta = tactic_expr; "|"; tg = tactic_then_gen -> { let (first,last) = tg in (ta::first, last) }
- | ta = tactic_expr; ".."; l = tactic_then_last -> { ([], Some (ta, l)) }
+ for_each_goal:
+ [ [ ta = ltac_expr; "|"; tg = for_each_goal -> { let (first,last) = tg in (ta::first, last) }
+ | ta = ltac_expr; ".."; l = tactic_then_last -> { ([], Some (ta, l)) }
| ".."; l = tactic_then_last -> { ([], Some (TacId [], l)) }
- | ta = tactic_expr -> { ([ta], None) }
- | "|"; tg = tactic_then_gen -> { let (first,last) = tg in (TacId [] :: first, last) }
+ | ta = ltac_expr -> { ([ta], None) }
+ | "|"; tg = for_each_goal -> { let (first,last) = tg in (TacId [] :: first, last) }
| -> { ([TacId []], None) }
] ]
;
@@ -97,13 +97,13 @@ GRAMMAR EXTEND Gram
for [TacExtend] *)
[ [ "[" ; l = OPT">" -> { if Option.is_empty l then true else false } ] ]
;
- tactic_expr:
+ ltac_expr:
[ "5" RIGHTA
[ te = binder_tactic -> { te } ]
| "4" LEFTA
- [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> { TacThen (ta0, ta1) }
- | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> { TacThen (ta0,ta1) }
- | ta0 = tactic_expr; ";"; l = tactic_then_locality; tg = tactic_then_gen; "]" -> {
+ [ ta0 = ltac_expr; ";"; ta1 = binder_tactic -> { TacThen (ta0, ta1) }
+ | ta0 = ltac_expr; ";"; ta1 = ltac_expr -> { TacThen (ta0,ta1) }
+ | ta0 = ltac_expr; ";"; l = tactic_then_locality; tg = for_each_goal; "]" -> {
let (first,tail) = tg in
match l , tail with
| false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last))
@@ -111,51 +111,51 @@ GRAMMAR EXTEND Gram
| false , None -> TacThen (ta0,TacDispatch first)
| true , None -> TacThens (ta0,first) } ]
| "3" RIGHTA
- [ IDENT "try"; ta = tactic_expr -> { TacTry ta }
- | IDENT "do"; n = int_or_var; ta = tactic_expr -> { TacDo (n,ta) }
- | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> { TacTimeout (n,ta) }
- | IDENT "time"; s = OPT string; ta = tactic_expr -> { TacTime (s,ta) }
- | IDENT "repeat"; ta = tactic_expr -> { TacRepeat ta }
- | IDENT "progress"; ta = tactic_expr -> { TacProgress ta }
- | IDENT "once"; ta = tactic_expr -> { TacOnce ta }
- | IDENT "exactly_once"; ta = tactic_expr -> { TacExactlyOnce ta }
- | IDENT "infoH"; ta = tactic_expr -> { TacShowHyps ta }
+ [ IDENT "try"; ta = ltac_expr -> { TacTry ta }
+ | IDENT "do"; n = int_or_var; ta = ltac_expr -> { TacDo (n,ta) }
+ | IDENT "timeout"; n = int_or_var; ta = ltac_expr -> { TacTimeout (n,ta) }
+ | IDENT "time"; s = OPT string; ta = ltac_expr -> { TacTime (s,ta) }
+ | IDENT "repeat"; ta = ltac_expr -> { TacRepeat ta }
+ | IDENT "progress"; ta = ltac_expr -> { TacProgress ta }
+ | IDENT "once"; ta = ltac_expr -> { TacOnce ta }
+ | IDENT "exactly_once"; ta = ltac_expr -> { TacExactlyOnce ta }
+ | IDENT "infoH"; ta = ltac_expr -> { TacShowHyps ta }
(*To do: put Abstract in Refiner*)
| IDENT "abstract"; tc = NEXT -> { TacAbstract (tc,None) }
| IDENT "abstract"; tc = NEXT; "using"; s = ident ->
{ TacAbstract (tc,Some s) }
- | sel = selector; ta = tactic_expr -> { TacSelect (sel, ta) } ]
+ | IDENT "only"; sel = selector; ":"; ta = ltac_expr -> { TacSelect (sel, ta) } ]
(*End of To do*)
| "2" RIGHTA
- [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> { TacOr (ta0,ta1) }
- | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> { TacOr (ta0,ta1) }
- | IDENT "tryif" ; ta = tactic_expr ;
- "then" ; tat = tactic_expr ;
- "else" ; tae = tactic_expr -> { TacIfThenCatch(ta,tat,tae) }
- | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> { TacOrelse (ta0,ta1) }
- | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> { TacOrelse (ta0,ta1) } ]
+ [ ta0 = ltac_expr; "+"; ta1 = binder_tactic -> { TacOr (ta0,ta1) }
+ | ta0 = ltac_expr; "+"; ta1 = ltac_expr -> { TacOr (ta0,ta1) }
+ | IDENT "tryif" ; ta = ltac_expr ;
+ "then" ; tat = ltac_expr ;
+ "else" ; tae = ltac_expr -> { TacIfThenCatch(ta,tat,tae) }
+ | ta0 = ltac_expr; "||"; ta1 = binder_tactic -> { TacOrelse (ta0,ta1) }
+ | ta0 = ltac_expr; "||"; ta1 = ltac_expr -> { TacOrelse (ta0,ta1) } ]
| "1" RIGHTA
[ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
{ TacMatchGoal (b,false,mrl) }
| b = match_key; IDENT "reverse"; IDENT "goal"; "with";
mrl = match_context_list; "end" ->
{ TacMatchGoal (b,true,mrl) }
- | b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" ->
+ | b = match_key; c = ltac_expr; "with"; mrl = match_list; "end" ->
{ TacMatch (b,c,mrl) }
- | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
+ | IDENT "first" ; "["; l = LIST0 ltac_expr SEP "|"; "]" ->
{ TacFirst l }
- | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
+ | IDENT "solve" ; "["; l = LIST0 ltac_expr SEP "|"; "]" ->
{ TacSolve l }
| IDENT "idtac"; l = LIST0 message_token -> { TacId l }
| g=failkw; n = [ n = int_or_var -> { n } | -> { fail_default_value } ];
l = LIST0 message_token -> { TacFail (g,n,l) }
| st = simple_tactic -> { st }
- | a = tactic_arg -> { TacArg(CAst.make ~loc a) }
- | r = reference; la = LIST0 tactic_arg_compat ->
+ | a = tactic_value -> { TacArg(CAst.make ~loc a) }
+ | r = reference; la = LIST0 tactic_arg ->
{ TacArg(CAst.make ~loc @@ TacCall (CAst.make ~loc (r,la))) } ]
| "0"
- [ "("; a = tactic_expr; ")" -> { a }
- | "["; ">"; tg = tactic_then_gen; "]" -> {
+ [ "("; a = ltac_expr; ")" -> { a }
+ | "["; ">"; tg = for_each_goal; "]" -> {
let (tf,tail) = tg in
begin match tail with
| Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl)
@@ -166,24 +166,24 @@ GRAMMAR EXTEND Gram
failkw:
[ [ IDENT "fail" -> { TacLocal } | IDENT "gfail" -> { TacGlobal } ] ]
;
- (* binder_tactic: level 5 of tactic_expr *)
+ (* binder_tactic: level 5 of ltac_expr *)
binder_tactic:
[ RIGHTA
- [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" ->
+ [ "fun"; it = LIST1 input_fun ; "=>"; body = ltac_expr LEVEL "5" ->
{ TacFun (it,body) }
| "let"; isrec = [IDENT "rec" -> { true } | -> { false } ];
llc = LIST1 let_clause SEP "with"; "in";
- body = tactic_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } ] ]
+ body = ltac_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } ] ]
;
(* Tactic arguments to the right of an application *)
- tactic_arg_compat:
- [ [ a = tactic_arg -> { a }
+ tactic_arg:
+ [ [ a = tactic_value -> { a }
| c = Constr.constr -> { (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c)) }
(* Unambiguous entries: tolerated w/o "ltac:" modifier *)
| "()" -> { TacGeneric (None, genarg_of_unit ()) } ] ]
;
(* Can be used as argument and at toplevel in tactic expressions. *)
- tactic_arg:
+ tactic_value:
[ [ c = constr_eval -> { ConstrMayEval c }
| IDENT "fresh"; l = LIST0 fresh_id -> { TacFreshId l }
| IDENT "type_term"; c=uconstr -> { TacPretype c }
@@ -223,20 +223,20 @@ GRAMMAR EXTEND Gram
| l = ident -> { Name.Name l } ] ]
;
let_clause:
- [ [ idr = identref; ":="; te = tactic_expr ->
+ [ [ idr = identref; ":="; te = ltac_expr ->
{ (CAst.map (fun id -> Name id) idr, arg_of_expr te) }
- | na = ["_" -> { CAst.make ~loc Anonymous } ]; ":="; te = tactic_expr ->
+ | na = ["_" -> { CAst.make ~loc Anonymous } ]; ":="; te = ltac_expr ->
{ (na, arg_of_expr te) }
- | idr = identref; args = LIST1 input_fun; ":="; te = tactic_expr ->
+ | idr = identref; args = LIST1 input_fun; ":="; te = ltac_expr ->
{ (CAst.map (fun id -> Name id) idr, arg_of_expr (TacFun(args,te))) } ] ]
;
match_pattern:
[ [ IDENT "context"; oid = OPT Constr.ident;
- "["; pc = Constr.lconstr_pattern; "]" ->
+ "["; pc = Constr.cpattern; "]" ->
{ Subterm (oid, pc) }
- | pc = Constr.lconstr_pattern -> { Term pc } ] ]
+ | pc = Constr.cpattern -> { Term pc } ] ]
;
- match_hyps:
+ match_hyp:
[ [ na = name; ":"; mp = match_pattern -> { Hyp (na, mp) }
| na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> { Def (na, mpv, mpt) }
| na = name; ":="; mpv = match_pattern ->
@@ -250,19 +250,19 @@ GRAMMAR EXTEND Gram
] ]
;
match_context_rule:
- [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
- "=>"; te = tactic_expr -> { Pat (largs, mp, te) }
- | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
- "]"; "=>"; te = tactic_expr -> { Pat (largs, mp, te) }
- | "_"; "=>"; te = tactic_expr -> { All te } ] ]
+ [ [ largs = LIST0 match_hyp SEP ","; "|-"; mp = match_pattern;
+ "=>"; te = ltac_expr -> { Pat (largs, mp, te) }
+ | "["; largs = LIST0 match_hyp SEP ","; "|-"; mp = match_pattern;
+ "]"; "=>"; te = ltac_expr -> { Pat (largs, mp, te) }
+ | "_"; "=>"; te = ltac_expr -> { All te } ] ]
;
match_context_list:
[ [ mrl = LIST1 match_context_rule SEP "|" -> { mrl }
| "|"; mrl = LIST1 match_context_rule SEP "|" -> { mrl } ] ]
;
match_rule:
- [ [ mp = match_pattern; "=>"; te = tactic_expr -> { Pat ([],mp,te) }
- | "_"; "=>"; te = tactic_expr -> { All te } ] ]
+ [ [ mp = match_pattern; "=>"; te = ltac_expr -> { Pat ([],mp,te) }
+ | "_"; "=>"; te = ltac_expr -> { All te } ] ]
;
match_list:
[ [ mrl = LIST1 match_rule SEP "|" -> { mrl }
@@ -282,13 +282,13 @@ GRAMMAR EXTEND Gram
(* Definitions for tactics *)
tacdef_body:
[ [ name = Constr.global; it=LIST1 input_fun;
- redef = ltac_def_kind; body = tactic_expr ->
+ redef = ltac_def_kind; body = ltac_expr ->
{ if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body))
else
let id = reference_to_id name in
Tacexpr.TacticDefinition (id, TacFun (it, body)) }
| name = Constr.global; redef = ltac_def_kind;
- body = tactic_expr ->
+ body = ltac_expr ->
{ if redef then Tacexpr.TacticRedefinition (name, body)
else
let id = reference_to_id name in
@@ -296,7 +296,7 @@ GRAMMAR EXTEND Gram
] ]
;
tactic:
- [ [ tac = tactic_expr -> { tac } ] ]
+ [ [ tac = ltac_expr -> { tac } ] ]
;
range_selector:
@@ -314,15 +314,12 @@ GRAMMAR EXTEND Gram
{ let open Goal_select in
Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l } ] ]
;
- selector_body:
+ selector:
[ [ l = range_selector_or_nth -> { l }
| test_bracket_ident; "["; id = ident; "]" -> { Goal_select.SelectId id } ] ]
;
- selector:
- [ [ IDENT "only"; sel = selector_body; ":" -> { sel } ] ]
- ;
toplevel_selector:
- [ [ sel = selector_body; ":" -> { sel }
+ [ [ sel = selector; ":" -> { sel }
| "!"; ":" -> { Goal_select.SelectAlreadyFocused }
| IDENT "all"; ":" -> { Goal_select.SelectAll } ] ]
;
@@ -343,8 +340,8 @@ GRAMMAR EXTEND Gram
tac = Pltac.tactic ->
{ Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ]
;
- operconstr: LEVEL "0"
- [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
+ term: LEVEL "0"
+ [ [ IDENT "ltac"; ":"; "("; tac = Pltac.ltac_expr; ")" ->
{ let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in
CAst.make ~loc @@ CHole (None, IntroAnonymous, Some arg) } ] ]
;
@@ -355,28 +352,8 @@ GRAMMAR EXTEND Gram
open Stdarg
open Tacarg
open Vernacextend
-open Goptions
open Libnames
-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 = Declare.Proof.map_fold_endline ~f:(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 (p,status) =
- Proof.solve n info (Tacinterp.hide_interp global tcom None) ?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) pstate in
- if not status then Feedback.feedback Feedback.AddedAxiom;
- pstate
-
let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s
}
@@ -409,34 +386,34 @@ END
{
-let is_anonymous_abstract = function
- | TacAbstract (_,None) -> true
- | TacSolve [TacAbstract (_,None)] -> true
- | _ -> false
let rm_abstract = function
- | TacAbstract (t,_) -> t
- | TacSolve [TacAbstract (t,_)] -> TacSolve [t]
- | x -> x
+ | TacAbstract (t,_) -> t, true
+ | TacSolve [TacAbstract (t,_)] -> TacSolve [t], true
+ | x -> x, false
let is_explicit_terminator = function TacSolve _ -> true | _ -> false
}
VERNAC { tactic_mode } EXTEND VernacSolve STATE proof
-| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+| [ ltac_selector_opt(g) ltac_info_opt(info) tactic(t) ltac_use_default(with_end_tac) ] =>
{ classify_as_proofstep } -> {
let g = Option.default (Goal_select.get_default_goal_selector ()) g in
- vernac_solve g n t def
+ let global = match g with Goal_select.SelectAll | Goal_select.SelectList _ -> true | _ -> false in
+ let t = Tacinterp.hide_interp { Tacinterp.global; ast = t; } in
+ ComTactic.solve g ~info t ~with_end_tac
}
-| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+END
+
+VERNAC { tactic_mode } EXTEND VernacSolveParallel STATE proof
+| [ "par" ":" ltac_info_opt(info) tactic(t) ltac_use_default(with_end_tac) ] =>
{
- let anon_abstracting_tac = is_anonymous_abstract t in
let solving_tac = is_explicit_terminator t in
- let parallel = `Yes (solving_tac,anon_abstracting_tac) in
let pbr = if solving_tac then Some "par" else None in
- VtProofStep{ parallel = parallel; proof_block_detection = pbr }
+ VtProofStep{ proof_block_detection = pbr }
} -> {
- let t = rm_abstract t in
- vernac_solve Goal_select.SelectAll n t def
+ let t, abstract = rm_abstract t in
+ let t = Tacinterp.hide_interp { Tacinterp.global = true; ast = t; } in
+ ComTactic.solve_parallel ~info t ~abstract ~with_end_tac
}
END
@@ -489,7 +466,7 @@ END
VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY
| [ "Print" "Ltac" reference(r) ] ->
- { Feedback.msg_notice (Tacintern.print_ltac r) }
+ { Feedback.msg_notice (Tacentries.print_ltac r) }
END
VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index fc24475a62..6bf330c830 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -111,6 +111,8 @@ END
VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF STATE program
| [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] ->
{ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) }
+| [ "Solve" "Obligations" "of" ident(name) ] ->
+ { try_solve_obligations (Some name) None }
| [ "Solve" "Obligations" "with" tactic(t) ] ->
{ try_solve_obligations None (Some (Tacinterp.interp t)) }
| [ "Solve" "Obligations" ] ->
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 8331927cda..a3f03b5bb5 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -29,8 +29,6 @@ open Pvernac.Vernac_
open Pltac
open Vernacextend
-let wit_hyp = wit_var
-
}
DECLARE PLUGIN "ltac_plugin"
@@ -69,12 +67,12 @@ END
{
type raw_strategy = (constr_expr, Tacexpr.raw_red_expr) strategy_ast
-type glob_strategy = (glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast
+type glob_strategy = (glob_constr_and_expr, Tacexpr.glob_red_expr) strategy_ast
let interp_strategy ist gl s =
let sigma = project gl in
- sigma, strategy_of_ast s
-let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (fun c -> c) s
+ sigma, strategy_of_ast ist s
+let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (Tacintern.intern_red_expr ist) s
let subst_strategy s str = str
let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>"
@@ -82,12 +80,9 @@ let pr_raw_strategy env sigma prc prlc _ (s : raw_strategy) =
let prr = Pptactic.pr_red_expr env sigma (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in
Rewrite.pr_strategy (prc env sigma) prr s
let pr_glob_strategy env sigma prc prlc _ (s : glob_strategy) =
- let prr = Pptactic.pr_red_expr env sigma
- (Ppconstr.pr_constr_expr,
- Ppconstr.pr_lconstr_expr,
- Pputils.pr_or_by_notation Libnames.pr_qualid,
- Ppconstr.pr_constr_expr)
- in
+ let prpat env sigma (_,c,_) = prc env sigma c in
+ let prcst = Pputils.pr_or_var Pptactic.(pr_and_short_name (pr_evaluable_reference_env env)) in
+ let prr = Pptactic.pr_red_expr env sigma (prc, prlc, prcst, prpat) in
Rewrite.pr_strategy (prc env sigma) prr s
}
@@ -132,15 +127,15 @@ END
{
let db_strat db = StratUnary (Topdown, StratHints (false, db))
-let cl_rewrite_clause_db db = cl_rewrite_clause_strat (strategy_of_ast (db_strat db))
+let cl_rewrite_clause_db ist db = cl_rewrite_clause_strat (strategy_of_ast ist (db_strat db))
}
TACTIC EXTEND rewrite_strat
| [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> { cl_rewrite_clause_strat s (Some id) }
| [ "rewrite_strat" rewstrategy(s) ] -> { cl_rewrite_clause_strat s None }
-| [ "rewrite_db" preident(db) "in" hyp(id) ] -> { cl_rewrite_clause_db db (Some id) }
-| [ "rewrite_db" preident(db) ] -> { cl_rewrite_clause_db db None }
+| [ "rewrite_db" preident(db) "in" hyp(id) ] -> { cl_rewrite_clause_db ist db (Some id) }
+| [ "rewrite_db" preident(db) ] -> { cl_rewrite_clause_db ist db None }
END
{
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index e51b1f051d..ecfe6c1664 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -121,8 +121,8 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
end
| _ -> ElimOnConstr clbind
-let mkNumeral n =
- Numeral (NumTok.Signed.of_int_string (string_of_int n))
+let mkNumber n =
+ Number (NumTok.Signed.of_int_string (string_of_int n))
let mkTacCase with_evar = function
| [(clear,ElimOnConstr cl),(None,None),None],None ->
@@ -130,7 +130,7 @@ let mkTacCase with_evar = function
(* Reinterpret numbers as a notation for terms *)
| [(clear,ElimOnAnonHyp n),(None,None),None],None ->
TacCase (with_evar,
- (clear,(CAst.make @@ CPrim (mkNumeral n),
+ (clear,(CAst.make @@ CPrim (mkNumber n),
NoBindings)))
(* Reinterpret ident as notations for variables in the context *)
(* because we don't know if they are quantified or not *)
@@ -280,7 +280,7 @@ GRAMMAR EXTEND Gram
| "[="; tc = intropatterns; "]" -> { IntroInjection tc } ] ]
;
naming_intropattern:
- [ [ prefix = pattern_ident -> { IntroFresh prefix }
+ [ [ prefix = pattern_ident -> { IntroFresh prefix.CAst.v }
| "?" -> { IntroAnonymous }
| id = ident -> { IntroIdentifier id } ] ]
;
@@ -291,7 +291,7 @@ GRAMMAR EXTEND Gram
;
simple_intropattern:
[ [ pat = simple_intropattern_closed;
- l = LIST0 ["%"; c = operconstr LEVEL "0" -> { c } ] ->
+ l = LIST0 ["%"; c = term LEVEL "0" -> { c } ] ->
{ let {CAst.loc=loc0;v=pat} = pat in
let f c pat =
let loc1 = Constrexpr_ops.constr_loc c in
@@ -320,7 +320,7 @@ GRAMMAR EXTEND Gram
with_bindings:
[ [ "with"; bl = bindings -> { bl } | -> { NoBindings } ] ]
;
- red_flags:
+ red_flag:
[ [ IDENT "beta" -> { [FBeta] }
| IDENT "iota" -> { [FMatch;FFix;FCofix] }
| IDENT "match" -> { [FMatch] }
@@ -337,7 +337,7 @@ GRAMMAR EXTEND Gram
] ]
;
strategy_flag:
- [ [ s = LIST1 red_flags -> { Redops.make_red_flag (List.flatten s) }
+ [ [ s = LIST1 red_flag -> { Redops.make_red_flag (List.flatten s) }
| d = delta_flag -> { all_with d }
] ]
;
@@ -460,7 +460,7 @@ GRAMMAR EXTEND Gram
[ [ "as"; id = ident -> { Names.Name.Name id } | -> { Names.Name.Anonymous } ] ]
;
by_tactic:
- [ [ "by"; tac = tactic_expr LEVEL "3" -> { Some tac }
+ [ [ "by"; tac = ltac_expr LEVEL "3" -> { Some tac }
| -> { None } ] ]
;
rewriter :
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index b7b54143df..94e398fe5d 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -37,8 +37,10 @@ let clause_dft_concl =
(* Main entries for ltac *)
-let tactic_arg = Entry.create "tactic_arg"
-let tactic_expr = Entry.create "tactic_expr"
+let tactic_value = Entry.create "tactic_value"
+let tactic_arg = tactic_value
+let ltac_expr = Entry.create "ltac_expr"
+let tactic_expr = ltac_expr
let binder_tactic = Entry.create "binder_tactic"
let tactic = Entry.create "tactic"
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 8565c4b4d6..3a4a081c93 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -31,8 +31,12 @@ val simple_tactic : raw_tactic_expr Entry.t
val simple_intropattern : constr_expr intro_pattern_expr CAst.t Entry.t
val in_clause : Names.lident Locus.clause_expr Entry.t
val clause_dft_concl : Names.lident Locus.clause_expr Entry.t
+val tactic_value : raw_tactic_arg Entry.t
val tactic_arg : raw_tactic_arg Entry.t
+ [@@deprecated "Deprecated in 8.13; use 'tactic_value' instead"]
+val ltac_expr : raw_tactic_expr Entry.t
val tactic_expr : raw_tactic_expr Entry.t
+ [@@deprecated "Deprecated in 8.13; use 'ltac_expr' instead"]
val binder_tactic : raw_tactic_expr Entry.t
val tactic : raw_tactic_expr Entry.t
val tactic_eoi : raw_tactic_expr Entry.t
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 85bb901046..edd56ee0f7 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -179,7 +179,7 @@ let string_of_genarg_arg (ArgumentType arg) =
| ConstrTypeOf c ->
hov 1 (keyword "type of" ++ spc() ++ prc env sigma c)
| ConstrTerm c when test c ->
- h 0 (str "(" ++ prc env sigma c ++ str ")")
+ h (str "(" ++ prc env sigma c ++ str ")")
| ConstrTerm c ->
prc env sigma c
@@ -1135,8 +1135,8 @@ let pr_goal_selector ~toplevel s =
pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env));
pr_lconstr = (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env));
pr_pattern = (fun env sigma -> pr_pat_and_constr_expr (pr_glob_constr_env env));
- pr_lpattern = (fun env sigma -> pr_pat_and_constr_expr (pr_lglob_constr_env env));
pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env));
+ pr_lpattern = (fun env sigma -> pr_pat_and_constr_expr (pr_lglob_constr_env env));
pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant);
pr_name = pr_lident;
pr_generic = Pputils.pr_glb_generic;
@@ -1323,7 +1323,7 @@ let () =
register_basic_print0 wit_smart_global
(pr_or_by_notation pr_qualid) (pr_or_var (pr_located pr_global)) pr_global;
register_basic_print0 wit_ident pr_id pr_id pr_id;
- register_basic_print0 wit_var pr_lident pr_lident pr_id;
+ register_basic_print0 wit_hyp pr_lident pr_lident pr_id;
register_print0 wit_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env [@warning "-3"];
register_print0 wit_simple_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env;
Genprint.register_print0
@@ -1334,8 +1334,8 @@ let () =
;
Genprint.register_print0
wit_constr
- (lift_env Ppconstr.pr_lconstr_expr)
- (lift_env (fun env sigma (c, _) -> pr_lglob_constr_pptac env sigma c))
+ (lift_env Ppconstr.pr_constr_expr)
+ (lift_env (fun env sigma (c, _) -> pr_glob_constr_pptac env sigma c))
(make_constr_printer Printer.pr_econstr_n_env)
;
Genprint.register_print0
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 6a9fb5c2ea..5e199dad62 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -8,7 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-(** This module implements pretty-printers for tactic_expr syntactic
+(** This module implements pretty-printers for ltac_expr syntactic
objects and their subcomponents. *)
open Genarg
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 0dbf16a821..9c15d24dd3 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -146,7 +146,7 @@ let header =
fnl ()
let rec print_node ~filter all_total indent prefix (s, e) =
- h 0 (
+ h (
padr_with '-' 40 (prefix ^ s ^ " ")
++ padl 7 (format_ratio (e.local /. all_total))
++ padl 7 (format_ratio (e.total /. all_total))
@@ -212,7 +212,7 @@ let to_string ~filter ?(cutoff=0.0) node =
in
let filter s n = filter s && (all_total <= 0.0 || n /. all_total >= cutoff /. 100.0) in
let msg =
- h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++
+ h (str "total time: " ++ padl 11 (format_sec (all_total))) ++
fnl () ++
fnl () ++
header ++
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 5ef76dbdc1..26e2b18a02 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -769,7 +769,7 @@ let get_rew_prf evars r = match r.rew_prf with
let poly_subrelation sort =
if sort then PropGlobal.subrelation else TypeGlobal.subrelation
-let resolve_subrelation env avoid car rel sort prf rel' res =
+let resolve_subrelation env car rel sort prf rel' res =
if Termops.eq_constr (fst res.rew_evars) rel rel' then res
else
let evars, app = app_poly_check env res.rew_evars (poly_subrelation sort) [|car; rel; rel'|] in
@@ -779,7 +779,7 @@ let resolve_subrelation env avoid car rel sort prf rel' res =
rew_prf = RewPrf (rel', appsub);
rew_evars = evars }
-let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) evars =
+let resolve_morphism env m args args' (b,cstr) evars =
let evars, morph_instance, proj, sigargs, m', args, args' =
let first = match (Array.findi (fun _ b -> not (Option.is_empty b)) args') with
| Some i -> i
@@ -843,18 +843,18 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
let proof = applist (proj, List.rev projargs) in
let newt = applist (m', List.rev typeargs) in
match respars with
- [ a, Some r ] -> evars, proof, substl subst a, substl subst r, oldt, fnewt newt
+ [ a, Some r ] -> evars, proof, substl subst a, substl subst r, newt
| _ -> assert(false)
-let apply_constraint env avoid car rel prf cstr res =
+let apply_constraint env car rel prf cstr res =
match snd cstr with
| None -> res
- | Some r -> resolve_subrelation env avoid car rel (fst cstr) prf r res
+ | Some r -> resolve_subrelation env car rel (fst cstr) prf r res
-let coerce env avoid cstr res =
+let coerce env cstr res =
let evars, (rel, prf) = get_rew_prf res.rew_evars res in
let res = { res with rew_evars = evars } in
- apply_constraint env avoid res.rew_car rel prf cstr res
+ apply_constraint env res.rew_car rel prf cstr res
let apply_rule unify loccs : int pure_strategy =
let (nowhere_except_in,occs) = convert_occs loccs in
@@ -863,7 +863,7 @@ let apply_rule unify loccs : int pure_strategy =
then List.mem occ occs
else not (List.mem occ occs)
in
- { strategy = fun { state = occ ; env ; unfresh ;
+ { strategy = fun { state = occ ; env ;
term1 = t ; ty1 = ty ; cstr ; evars } ->
let unif = if isEvar (goalevars evars) t then None else unify env evars t in
match unif with
@@ -874,7 +874,7 @@ let apply_rule unify loccs : int pure_strategy =
else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity)
else
let res = { rew with rew_car = ty } in
- let res = Success (coerce env unfresh cstr res) in
+ let res = Success (coerce env cstr res) in
(occ, res)
}
@@ -968,7 +968,7 @@ let fold_match ?(force=false) env sigma c =
let unfold_match env sigma sk app =
match EConstr.kind sigma app with
- | App (f', args) when Constant.equal (fst (destConst sigma f')) sk ->
+ | App (f', args) when QConstant.equal env (fst (destConst sigma f')) sk ->
let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in
let v = EConstr.of_constr v in
Reductionops.whd_beta env sigma (mkApp (v, args))
@@ -1017,10 +1017,10 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
| None -> false
| Some r -> not (is_rew_cast r.rew_prf)) args'
then
- let evars', prf, car, rel, c1, c2 =
- resolve_morphism env unfresh t m args args' (prop, cstr') evars'
+ let evars', prf, car, rel, c2 =
+ resolve_morphism env m args args' (prop, cstr') evars'
in
- let res = { rew_car = ty; rew_from = c1;
+ let res = { rew_car = ty; rew_from = t;
rew_to = c2; rew_prf = RewPrf (rel, prf);
rew_evars = evars' }
in Success res
@@ -1071,7 +1071,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let res =
match prf with
| RewPrf (rel, prf) ->
- Success (apply_constraint env unfresh res.rew_car
+ Success (apply_constraint env res.rew_car
rel prf (prop,cstr) res)
| _ -> Success res
in state, res
@@ -1094,20 +1094,6 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
| Fail | Identity -> res
in state, res
- (* if x' = None && flags.under_lambdas then *)
- (* let lam = mkLambda (n, x, b) in *)
- (* let lam', occ = aux env lam occ None in *)
- (* let res = *)
- (* match lam' with *)
- (* | None -> None *)
- (* | Some (prf, (car, rel, c1, c2)) -> *)
- (* Some (resolve_morphism env sigma t *)
- (* ~fnewt:unfold_all *)
- (* (Lazy.force coq_all) [| x ; lam |] [| None; lam' |] *)
- (* cstr evars) *)
- (* in res, occ *)
- (* else *)
-
| Prod (n, dom, codom) ->
let lam = mkLambda (n, dom, codom) in
let (evars', app), unfold =
@@ -1131,31 +1117,13 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
B. Barras' idea is to have a context of relations, of length 1, with Σ for gluing
dependent relations and using projections to get them out.
*)
- (* | Lambda (n, t, b) when flags.under_lambdas -> *)
- (* let n' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n in *)
- (* let n'' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n' in *)
- (* let n''' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n'' in *)
- (* let rel = new_cstr_evar cstr env (mkApp (Lazy.force coq_relation, [|t|])) in *)
- (* let env' = Environ.push_rel_context [(n'',None,lift 2 rel);(n'',None,lift 1 t);(n', None, t)] env in *)
- (* let b' = s env' avoid b (Typing.type_of env' (goalevars evars) (lift 2 b)) (unlift_cstr env (goalevars evars) cstr) evars in *)
- (* (match b' with *)
- (* | Some (Some r) -> *)
- (* let prf = match r.rew_prf with *)
- (* | RewPrf (rel, prf) -> *)
- (* let rel = pointwise_or_dep_relation n' t r.rew_car rel in *)
- (* let prf = mkLambda (n', t, prf) in *)
- (* RewPrf (rel, prf) *)
- (* | x -> x *)
- (* in *)
- (* Some (Some { r with *)
- (* rew_prf = prf; *)
- (* rew_car = mkProd (n, t, r.rew_car); *)
- (* rew_from = mkLambda(n, t, r.rew_from); *)
- (* rew_to = mkLambda (n, t, r.rew_to) }) *)
- (* | _ -> b') *)
| Lambda (n, t, b) when flags.under_lambdas ->
let n' = map_annot (Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env)) n in
+ let unfresh = match n'.binder_name with
+ | Anonymous -> unfresh
+ | Name id -> Id.Set.add id unfresh
+ in
let open Context.Rel.Declaration in
let env' = EConstr.push_rel (LocalAssum (n', t)) env in
let bty = Retyping.get_type_of env' (goalevars evars) b in
@@ -1196,7 +1164,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
| Success r ->
let case = mkCase (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs) in
let res = make_leibniz_proof env case ty r in
- state, Success (coerce env unfresh (prop,cstr) res)
+ state, Success (coerce env (prop,cstr) res)
| Fail | Identity ->
if Array.for_all (Int.equal 0) ci.ci_cstr_ndecls then
let evars', eqty = app_poly_sort prop env evars coq_eq [| ty |] in
@@ -1237,7 +1205,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
in
let res =
match res with
- | Success r -> Success (coerce env unfresh (prop,cstr) r)
+ | Success r -> Success (coerce env (prop,cstr) r)
| Fail | Identity -> res
in state, res
| _ -> state, Fail
@@ -1670,9 +1638,9 @@ let cl_rewrite_clause l left2right occs clause =
let cl_rewrite_clause_strat strat clause =
cl_rewrite_clause_strat false strat clause
-let apply_glob_constr c l2r occs = (); fun ({ state = () ; env = env } as input) ->
+let apply_glob_constr ist c l2r occs = (); fun ({ state = () ; env = env } as input) ->
let c sigma =
- let (sigma, c) = Pretyping.understand_tcc env sigma c in
+ let (sigma, c) = Tacinterp.interp_open_constr ist env sigma c in
(sigma, (c, NoBindings))
in
let flags = general_rewrite_unif_flags () in
@@ -1749,12 +1717,12 @@ let rec pr_strategy prc prr = function
| StratEval r -> str "eval" ++ spc () ++ prr r
| StratFold c -> str "fold" ++ spc () ++ prc c
-let rec strategy_of_ast = function
+let rec strategy_of_ast ist = function
| StratId -> Strategies.id
| StratFail -> Strategies.fail
| StratRefl -> Strategies.refl
| StratUnary (f, s) ->
- let s' = strategy_of_ast s in
+ let s' = strategy_of_ast ist s in
let f' = match f with
| Subterms -> all_subterms
| Subterm -> one_subterm
@@ -1768,13 +1736,13 @@ let rec strategy_of_ast = function
| Repeat -> Strategies.repeat
in f' s'
| StratBinary (f, s, t) ->
- let s' = strategy_of_ast s in
- let t' = strategy_of_ast t in
+ let s' = strategy_of_ast ist s in
+ let t' = strategy_of_ast ist t in
let f' = match f with
| Compose -> Strategies.seq
| Choice -> Strategies.choice
in f' s' t'
- | StratConstr (c, b) -> { strategy = apply_glob_constr (fst c) b AllOccurrences }
+ | StratConstr (c, b) -> { strategy = apply_glob_constr ist c b AllOccurrences }
| StratHints (old, id) -> if old then Strategies.old_hints id else Strategies.hints id
| StratTerms l -> { strategy =
(fun ({ state = () ; env } as input) ->
@@ -1783,7 +1751,7 @@ let rec strategy_of_ast = function
}
| StratEval r -> { strategy =
(fun ({ state = () ; env ; evars } as input) ->
- let (sigma,r_interp) = Tacinterp.interp_redexp env (goalevars evars) r in
+ let (sigma,r_interp) = Tacinterp.interp_red_expr ist env (goalevars evars) r in
(Strategies.reduce r_interp).strategy { input with
evars = (sigma,cstrevars evars) }) }
| StratFold c -> Strategies.fold_glob (fst c)
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 60a66dd861..8e0ce183c2 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -62,7 +62,7 @@ type rewrite_result =
type strategy
-val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strategy
+val strategy_of_ast : interp_sign -> (glob_constr_and_expr, glob_red_expr) strategy_ast -> strategy
val map_strategy : ('a -> 'b) -> ('c -> 'd) ->
('a, 'c) strategy_ast -> ('b, 'd) strategy_ast
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index f7037176d2..4c1fe6417e 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -161,8 +161,8 @@ let coerce_var_to_ident fresh env sigma v =
match out_gen (topwit wit_intro_pattern) v with
| { CAst.v=IntroNaming (IntroIdentifier id)} -> id
| _ -> fail ()
- else if has_type v (topwit wit_var) then
- out_gen (topwit wit_var) v
+ else if has_type v (topwit wit_hyp) then
+ out_gen (topwit wit_hyp) v
else match Value.to_constr v with
| None -> fail ()
| Some c ->
@@ -184,8 +184,8 @@ let id_of_name = function
| Some (IntroNaming (IntroIdentifier id)) -> id
| Some _ -> fail ()
| None ->
- if has_type v (topwit wit_var) then
- out_gen (topwit wit_var) v
+ if has_type v (topwit wit_hyp) then
+ out_gen (topwit wit_hyp) v
else
match Value.to_constr v with
| None -> fail ()
@@ -222,8 +222,8 @@ let coerce_to_intro_pattern sigma v =
match is_intro_pattern v with
| Some pat -> pat
| None ->
- if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
+ if has_type v (topwit wit_hyp) then
+ let id = out_gen (topwit wit_hyp) v in
IntroNaming (IntroIdentifier id)
else match Value.to_constr v with
| Some c when isVar sigma c ->
@@ -259,8 +259,8 @@ let coerce_to_constr env v =
([], c)
else if has_type v (topwit wit_constr_under_binders) then
out_gen (topwit wit_constr_under_binders) v
- else if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
+ else if has_type v (topwit wit_hyp) then
+ let id = out_gen (topwit wit_hyp) v in
(try [], constr_of_id env id with Not_found -> fail ())
else fail ()
@@ -282,8 +282,8 @@ let coerce_to_evaluable_ref env sigma v =
| Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> EvalVarRef id
| Some _ -> fail ()
| None ->
- if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
+ if has_type v (topwit wit_hyp) then
+ let id = out_gen (topwit wit_hyp) v in
if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id
else fail ()
else if has_type v (topwit wit_ref) then
@@ -328,8 +328,8 @@ let coerce_to_hyp env sigma v =
| Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> id
| Some _ -> fail ()
| None ->
- if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
+ if has_type v (topwit wit_hyp) then
+ let id = out_gen (topwit wit_hyp) v in
if is_variable env id then id else fail ()
else match Value.to_constr v with
| Some c when isVar sigma c -> destVar sigma c
@@ -360,8 +360,8 @@ let coerce_to_quantified_hypothesis sigma v =
| Some (IntroNaming (IntroIdentifier id)) -> NamedHyp id
| Some _ -> raise (CannotCoerceTo "a quantified hypothesis")
| None ->
- if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
+ if has_type v (topwit wit_hyp) then
+ let id = out_gen (topwit wit_hyp) v in
NamedHyp id
else if has_type v (topwit wit_int) then
AnonHyp (out_gen (topwit wit_int) v)
@@ -394,8 +394,13 @@ type appl =
(* Values for interpretation *)
type tacvalue =
- | VFun of appl * Tacexpr.ltac_trace * Loc.t option * Val.t Id.Map.t *
- Name.t list * Tacexpr.glob_tactic_expr
+ | VFun of
+ appl *
+ Tacexpr.ltac_trace *
+ Loc.t option * (* when executing a global Ltac function: the location where this function was called *)
+ Val.t Id.Map.t * (* closure *)
+ Name.t list * (* binders *)
+ Tacexpr.glob_tactic_expr (* body *)
| VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr
let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index f0ca813b08..29e29044f1 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -31,21 +31,9 @@ type argument = Genarg.ArgT.any Extend.user_symbol
(**********************************************************************)
(* Interpret entry names of the form "ne_constr_list" as entry keys *)
-let coincide s pat off =
- let len = String.length pat in
- let break = ref true in
- let i = ref 0 in
- while !break && !i < len do
- let c = Char.code s.[off + !i] in
- let d = Char.code pat.[!i] in
- break := Int.equal c d;
- incr i
- done;
- !break
-
let atactic n =
if n = 5 then Pcoq.Symbol.nterm Pltac.binder_tactic
- else Pcoq.Symbol.nterml Pltac.tactic_expr (string_of_int n)
+ else Pcoq.Symbol.nterml Pltac.ltac_expr (string_of_int n)
type entry_name = EntryName :
'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.Symbol.t -> entry_name
@@ -70,28 +58,37 @@ let check_separator ?loc = function
| Some _ -> user_err ?loc (str "Separator is only for arguments with suffix _list_sep.")
let rec parse_user_entry ?loc s sep =
- let l = String.length s in
- if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
- let entry = parse_user_entry ?loc (String.sub s 3 (l-8)) None in
+ let open CString in
+ let matches pre suf s =
+ String.length s > (String.length pre + String.length suf) &&
+ is_prefix pre s && is_suffix suf s
+ in
+ let basename pre suf s =
+ let plen = String.length pre in
+ String.sub s plen (String.length s - (plen + String.length suf))
+ in
+ let tactic_len = String.length "tactic" in
+ if matches "ne_" "_list" s then
+ let entry = parse_user_entry ?loc (basename "ne_" "_list" s) None in
check_separator ?loc sep;
Ulist1 entry
- else if l > 12 && coincide s "ne_" 0 &&
- coincide s "_list_sep" (l-9) then
- let entry = parse_user_entry ?loc (String.sub s 3 (l-12)) None in
+ else if matches "ne_" "_list_sep" s then
+ let entry = parse_user_entry ?loc (basename "ne_" "_list_sep" s) None in
Ulist1sep (entry, get_separator sep)
- else if l > 5 && coincide s "_list" (l-5) then
- let entry = parse_user_entry ?loc (String.sub s 0 (l-5)) None in
+ else if matches "" "_list" s then
+ let entry = parse_user_entry ?loc (basename "" "_list" s) None in
check_separator ?loc sep;
Ulist0 entry
- else if l > 9 && coincide s "_list_sep" (l-9) then
- let entry = parse_user_entry ?loc (String.sub s 0 (l-9)) None in
+ else if matches "" "_list_sep" s then
+ let entry = parse_user_entry ?loc (basename "" "_list_sep" s) None in
Ulist0sep (entry, get_separator sep)
- else if l > 4 && coincide s "_opt" (l-4) then
- let entry = parse_user_entry ?loc (String.sub s 0 (l-4)) None in
+ else if matches "" "_opt" s then
+ let entry = parse_user_entry ?loc (basename "" "_opt" s) None in
check_separator ?loc sep;
Uopt entry
- else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then
- let n = Char.code s.[6] - 48 in
+ else if String.length s = tactic_len + 1 && is_prefix "tactic" s
+ && '5' >= s.[tactic_len] && s.[tactic_len] >= '0' then
+ let n = Char.code s.[tactic_len] - Char.code '0' in
check_separator ?loc sep;
Uentryl ("tactic", n)
else
@@ -119,7 +116,7 @@ let get_tactic_entry n =
else if Int.equal n 5 then
Pltac.binder_tactic, None
else if 1<=n && n<5 then
- Pltac.tactic_expr, Some (Gramlib.Gramext.Level (string_of_int n))
+ Pltac.ltac_expr, Some (Gramlib.Gramext.Level (string_of_int n))
else
user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^"."))
@@ -159,7 +156,7 @@ let rec prod_item_of_symbol lev = function
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);
+ assert (CString.is_suffix "tactic" (ArgT.repr tag));
get_tacentry n lev
(** Tactic grammar extensions *)
@@ -219,7 +216,9 @@ let interp_prod_item = function
| None ->
if String.Map.mem s !entry_names then String.Map.find s !entry_names
else begin match ArgT.name s with
- | None -> user_err Pp.(str ("Unknown entry "^s^"."))
+ | None ->
+ if s = "var" then user_err Pp.(str ("var is deprecated, use hyp.")) (* to remove in 8.14 *)
+ else user_err Pp.(str ("Unknown entry "^s^"."))
| Some arg -> arg
end
| Some n ->
@@ -384,7 +383,7 @@ let add_ml_tactic_notation name ~level ?deprecation prods =
in
List.iteri iter (List.rev prods);
(* We call [extend_atomic_tactic] only for "basic tactics" (the ones
- at tactic_expr level 0) *)
+ at ltac_expr level 0) *)
if Int.equal level 0 then extend_atomic_tactic name prods
(**********************************************************************)
@@ -421,7 +420,7 @@ let create_ltac_quotation name cast (e, l) =
in
let action _ v _ _ _ loc = cast (Some loc, v) in
let gram = (level, assoc, [Pcoq.Production.make rule action]) in
- Pcoq.grammar_extend Pltac.tactic_arg {pos=None; data=[gram]}
+ Pcoq.grammar_extend Pltac.tactic_value {pos=None; data=[gram]}
(** Command *)
@@ -529,16 +528,40 @@ let print_ltacs () =
let locatable_ltac = "Ltac"
+let split_ltac_fun = function
+ | Tacexpr.TacFun (l,t) -> (l,t)
+ | t -> ([],t)
+
+let pr_ltac_fun_arg n = spc () ++ Name.print n
+
+let print_ltac_body qid tac =
+ let filter mp =
+ try Some (Nametab.shortest_qualid_of_module mp)
+ with Not_found -> None
+ in
+ let mods = List.map_filter filter tac.Tacenv.tac_redef in
+ let redefined = match mods with
+ | [] -> mt ()
+ | mods ->
+ let redef = prlist_with_sep fnl pr_qualid mods in
+ fnl () ++ str "Redefined by:" ++ fnl () ++ redef
+ in
+ let l,t = split_ltac_fun tac.Tacenv.tac_body in
+ hv 2 (
+ hov 2 (str "Ltac" ++ spc() ++ pr_qualid qid ++
+ prlist pr_ltac_fun_arg l ++ spc () ++ str ":=")
+ ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined
+
let () =
let open Prettyp in
- let locate qid = try Some (Tacenv.locate_tactic qid) with Not_found -> None in
- let locate_all = Tacenv.locate_extended_all_tactic in
- let shortest_qualid = Tacenv.shortest_qualid_of_tactic in
- let name kn = str "Ltac" ++ spc () ++ pr_path (Tacenv.path_of_tactic kn) in
- let print kn =
- let qid = qualid_of_path (Tacenv.path_of_tactic kn) in
- Tacintern.print_ltac qid
- in
+ let locate qid = try Some (qid, Tacenv.locate_tactic qid) with Not_found -> None in
+ let locate_all qid = List.map (fun kn -> (qid,kn)) (Tacenv.locate_extended_all_tactic qid) in
+ let shortest_qualid (qid,kn) = Tacenv.shortest_qualid_of_tactic kn in
+ let name (qid,kn) = str "Ltac" ++ spc () ++ pr_path (Tacenv.path_of_tactic kn) in
+ let print (qid,kn) =
+ let entries = Tacenv.ltac_entries () in
+ let tac = KNmap.find kn entries in
+ print_ltac_body qid tac in
let about = name in
register_locatable locatable_ltac {
locate;
@@ -552,14 +575,25 @@ let () =
let print_located_tactic qid =
Feedback.msg_notice (Prettyp.print_located_other locatable_ltac qid)
+let print_ltac id =
+ try
+ let kn = Tacenv.locate_tactic id in
+ let entries = Tacenv.ltac_entries () in
+ let tac = KNmap.find kn entries in
+ print_ltac_body id tac
+ with
+ Not_found ->
+ user_err ~hdr:"print_ltac"
+ (pr_qualid id ++ spc() ++ str "is not a user defined tactic.")
+
(** Grammar *)
let () =
let entries = [
- AnyEntry Pltac.tactic_expr;
+ AnyEntry Pltac.ltac_expr;
AnyEntry Pltac.binder_tactic;
AnyEntry Pltac.simple_tactic;
- AnyEntry Pltac.tactic_arg;
+ AnyEntry Pltac.tactic_value;
] in
register_grammars_by_name "tactic" entries
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 6ee3ce091b..fc9ab54eba 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -69,6 +69,9 @@ val print_ltacs : unit -> unit
val print_located_tactic : Libnames.qualid -> unit
(** Display the absolute name of a tactic. *)
+val print_ltac : Libnames.qualid -> Pp.t
+(** Display the definition of a tactic. *)
+
(** {5 Low-level registering of tactics} *)
type (_, 'a) ml_ty_sig =
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index dea216045e..47f1d3bf66 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -769,38 +769,6 @@ let glob_tactic_env l env x =
(intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars })
x
-let split_ltac_fun = function
- | TacFun (l,t) -> (l,t)
- | t -> ([],t)
-
-let pr_ltac_fun_arg n = spc () ++ Name.print n
-
-let print_ltac id =
- try
- let kn = Tacenv.locate_tactic id in
- let entries = Tacenv.ltac_entries () in
- let tac = KNmap.find kn entries in
- let filter mp =
- try Some (Nametab.shortest_qualid_of_module mp)
- with Not_found -> None
- in
- let mods = List.map_filter filter tac.Tacenv.tac_redef in
- let redefined = match mods with
- | [] -> mt ()
- | mods ->
- let redef = prlist_with_sep fnl pr_qualid mods in
- fnl () ++ str "Redefined by:" ++ fnl () ++ redef
- in
- let l,t = split_ltac_fun tac.Tacenv.tac_body in
- hv 2 (
- hov 2 (str "Ltac" ++ spc() ++ pr_qualid id ++
- prlist pr_ltac_fun_arg l ++ spc () ++ str ":=")
- ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined
- with
- Not_found ->
- user_err ~hdr:"print_ltac"
- (pr_qualid id ++ spc() ++ str "is not a user defined tactic.")
-
(** Registering *)
let lift intern = (); fun ist x -> (ist, intern ist x)
@@ -835,7 +803,7 @@ let () =
Genintern.register_intern0 wit_ref (lift intern_global_reference);
Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c));
Genintern.register_intern0 wit_ident intern_ident';
- Genintern.register_intern0 wit_var (lift intern_hyp);
+ Genintern.register_intern0 wit_hyp (lift intern_hyp);
Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg);
Genintern.register_intern0 wit_ltac (lift intern_ltac);
Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis);
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index 22ec15566b..f779aa470c 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -55,9 +55,6 @@ val intern_hyp : glob_sign -> lident -> lident
val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument
-(** printing *)
-val print_ltac : Libnames.qualid -> Pp.t
-
(** Reduction expressions *)
val intern_red_expr : glob_sign -> raw_red_expr -> glob_red_expr
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index ff6a36a049..3d734d3a66 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -153,11 +153,15 @@ let add_extra_loc loc extra =
match loc with
| None -> extra
| Some loc -> TacStore.set extra f_loc loc
-let add_loc loc ist =
+let extract_loc ist = TacStore.get ist.extra f_loc
+
+let ensure_loc loc ist =
match loc with
| None -> ist
- | Some loc -> { ist with extra = TacStore.set ist.extra f_loc loc }
-let extract_loc ist = TacStore.get ist.extra f_loc
+ | Some loc ->
+ match extract_loc ist with
+ | None -> { ist with extra = TacStore.set ist.extra f_loc loc }
+ | Some _ -> ist
let print_top_val env v = Pptactic.pr_value Pptactic.ltop v
@@ -971,8 +975,8 @@ let interp_destruction_arg ist gl arg =
match v with
| {v=IntroNaming (IntroIdentifier id)} -> try_cast_id id
| _ -> error ()
- else if has_type v (topwit wit_var) then
- let id = out_gen (topwit wit_var) v in
+ else if has_type v (topwit wit_hyp) then
+ let id = out_gen (topwit wit_hyp) v in
try_cast_id id
else if has_type v (topwit wit_int) then
keep,ElimOnAnonHyp (out_gen (topwit wit_int) v)
@@ -1175,7 +1179,7 @@ and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with
| TacFirst l -> Tacticals.New.tclFIRST (List.map (interp_tactic ist) l)
| TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l)
| TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac)
- | TacArg {CAst.loc} -> Ftactic.run (val_interp (add_loc loc ist) tac) (fun v -> tactic_of_value ist v)
+ | TacArg {CAst.loc} -> Ftactic.run (val_interp (ensure_loc loc ist) tac) (fun v -> tactic_of_value ist v)
| TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
(* For extensions *)
| TacAlias {loc; v=(s,l)} ->
@@ -1238,7 +1242,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
| ArgVar {loc;v=id} ->
let v =
try Id.Map.find id ist.lfun
- with Not_found -> in_gen (topwit wit_var) id
+ with Not_found -> in_gen (topwit wit_hyp) id
in
let open Ftactic in
force_vrec ist v >>= begin fun v ->
@@ -1254,9 +1258,12 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
let extra = TacStore.set extra f_trace trace in
let ist = { lfun = Id.Map.empty; poly; extra } in
let appl = GlbAppl[r,[]] in
+ (* We call a global ltac reference: add a loc on its executation only if not
+ already in another global reference *)
+ let ist = ensure_loc loc ist in
Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false
- (catch_error_tac_loc (* interp *) loc false trace
- (val_interp ~appl (add_loc (* exec *) loc ist) (Tacenv.interp_ltac r)))
+ (catch_error_tac_loc (* loc for interpretation *) loc false trace
+ (val_interp ~appl ist (Tacenv.interp_ltac r)))
and interp_tacarg ist arg : Val.t Ftactic.t =
match arg with
@@ -1325,7 +1332,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
; extra = TacStore.set ist.extra f_trace []
} in
Profile_ltac.do_profile "interp_app" trace ~count_call:false
- (catch_error_tac_loc loc false trace (val_interp (add_loc loc ist) body)) >>= fun v ->
+ (catch_error_tac_loc loc false trace (val_interp (ensure_loc loc ist) body)) >>= fun v ->
Ftactic.return (name_vfun (push_appl appl largs) v)
end
begin fun (e, info) ->
@@ -1529,7 +1536,7 @@ and interp_genarg ist x : Val.t Ftactic.t =
let open Ftactic.Notations in
(* Ad-hoc handling of some types. *)
let tag = genarg_tag x in
- if argument_type_eq tag (unquote (topwit (wit_list wit_var))) then
+ if argument_type_eq tag (unquote (topwit (wit_list wit_hyp))) then
interp_genarg_var_list ist x
else if argument_type_eq tag (unquote (topwit (wit_list wit_constr))) then
interp_genarg_constr_list ist x
@@ -1573,9 +1580,9 @@ and interp_genarg_var_list ist x =
Ftactic.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
- let lc = Genarg.out_gen (glbwit (wit_list wit_var)) x in
+ let lc = Genarg.out_gen (glbwit (wit_list wit_hyp)) x in
let lc = interp_hyp_list ist env sigma lc in
- let lc = in_list (val_tag wit_var) lc in
+ let lc = in_list (val_tag wit_hyp) lc in
Ftactic.return lc
end
@@ -1996,16 +2003,20 @@ let interp_tac_gen lfun avoid_ids debug t =
let interp t = interp_tac_gen Id.Map.empty Id.Set.empty (get_debug()) t
+(* MUST be marshallable! *)
+type ltac_expr = {
+ global: bool;
+ ast: Tacexpr.raw_tactic_expr;
+}
+
(* Used to hide interpretation for pretty-print, now just launch tactics *)
(* [global] means that [t] should be internalized outside of goals. *)
-let hide_interp global t ot =
+let hide_interp {global;ast} =
let hide_interp env =
let ist = Genintern.empty_glob_sign env in
- let te = intern_pure_tactic ist t in
+ let te = intern_pure_tactic ist ast in
let t = eval_tactic te in
- match ot with
- | None -> t
- | Some t' -> Tacticals.New.tclTHEN t t'
+ t
in
if global then
Proofview.tclENV >>= fun env ->
@@ -2015,6 +2026,8 @@ let hide_interp global t ot =
hide_interp (Proofview.Goal.env gl)
end
+let ComTactic.Interpreter hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp
+
(***************************************************************************)
(** Register standard arguments *)
@@ -2090,7 +2103,7 @@ let () =
register_interp0 wit_ref (lift interp_reference);
register_interp0 wit_pre_ident (lift interp_pre_ident);
register_interp0 wit_ident (lift interp_ident);
- register_interp0 wit_var (lift interp_hyp);
+ register_interp0 wit_hyp (lift interp_hyp);
register_interp0 wit_intropattern (lifts interp_intro_pattern) [@warning "-3"];
register_interp0 wit_simple_intropattern (lifts interp_intro_pattern);
register_interp0 wit_clause_dft_concl (lift interp_clause);
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index cbb17bf0fa..a74f4592f7 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -77,6 +77,9 @@ val val_interp : interp_sign -> glob_tactic_expr -> (value -> unit Proofview.tac
val interp_ltac_constr : interp_sign -> glob_tactic_expr -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic
(** Interprets redexp arguments *)
+val interp_red_expr : interp_sign -> Environ.env -> Evd.evar_map -> glob_red_expr -> Evd.evar_map * red_expr
+
+(** Interprets redexp arguments from a raw one *)
val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr
(** Interprets tactic expressions *)
@@ -126,8 +129,12 @@ val interp_tac_gen : value Id.Map.t -> Id.Set.t ->
val interp : raw_tactic_expr -> unit Proofview.tactic
(** Hides interpretation for pretty-print *)
+type ltac_expr = {
+ global: bool;
+ ast: Tacexpr.raw_tactic_expr;
+}
-val hide_interp : bool -> raw_tactic_expr -> unit Proofview.tactic option -> unit Proofview.tactic
+val hide_interp : ltac_expr -> ComTactic.interpretable
(** Internals that can be useful for syntax extensions. *)
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index fd869b225f..ec44ae4698 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -282,7 +282,7 @@ let () =
Genintern.register_subst0 wit_smart_global subst_global_reference;
Genintern.register_subst0 wit_pre_ident (fun _ v -> v);
Genintern.register_subst0 wit_ident (fun _ v -> v);
- Genintern.register_subst0 wit_var (fun _ v -> v);
+ Genintern.register_subst0 wit_hyp (fun _ v -> v);
Genintern.register_subst0 wit_intropattern subst_intro_pattern [@warning "-3"];
Genintern.register_subst0 wit_simple_intropattern subst_intro_pattern;
Genintern.register_subst0 wit_tactic subst_tactic;
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 00:19:05 +0000