aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/coretactics.mlg7
-rw-r--r--plugins/ltac/dune8
-rw-r--r--plugins/ltac/extratactics.mlg20
-rw-r--r--plugins/ltac/g_auto.mlg15
-rw-r--r--plugins/ltac/g_ltac.mlg2
-rw-r--r--plugins/ltac/g_obligations.mlg8
-rw-r--r--plugins/ltac/profile_ltac.ml6
-rw-r--r--plugins/ltac/rewrite.ml16
-rw-r--r--plugins/ltac/tacinterp.ml12
9 files changed, 37 insertions, 57 deletions
diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg
index e39c066c95..b20c4d173d 100644
--- a/plugins/ltac/coretactics.mlg
+++ b/plugins/ltac/coretactics.mlg
@@ -259,13 +259,6 @@ TACTIC EXTEND simple_destruct
| [ "simple" "destruct" quantified_hypothesis(h) ] -> { simple_destruct h }
END
-(** Double induction *)
-
-TACTIC EXTEND double_induction DEPRECATED { Deprecation.make () }
-| [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] ->
- { Elim.h_double_induction h1 h2 }
-END
-
(* Admit *)
TACTIC EXTEND admit
diff --git a/plugins/ltac/dune b/plugins/ltac/dune
index 6558ecbfe8..9ec2b10873 100644
--- a/plugins/ltac/dune
+++ b/plugins/ltac/dune
@@ -1,15 +1,15 @@
(library
(name ltac_plugin)
- (public_name coq.plugins.ltac)
+ (public_name coq-core.plugins.ltac)
(synopsis "Coq's LTAC tactic language")
(modules :standard \ tauto)
- (libraries coq.stm))
+ (libraries coq-core.stm))
(library
(name tauto_plugin)
- (public_name coq.plugins.tauto)
+ (public_name coq-core.plugins.tauto)
(synopsis "Coq's tauto tactic")
(modules tauto)
- (libraries coq.plugins.ltac))
+ (libraries coq-core.plugins.ltac))
(coq.pp (modules extratactics g_tactic g_rewrite g_eqdecide g_auto g_obligations g_ltac profile_ltac_tactics coretactics g_class extraargs))
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 90c366ed63..d9da47134d 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -299,7 +299,7 @@ TACTIC EXTEND rewrite_star
{
-let add_rewrite_hint ~poly bases ort t lcsr =
+let add_rewrite_hint ~locality ~poly bases ort t lcsr =
let env = Global.env() in
let sigma = Evd.from_env env in
let f ce =
@@ -315,7 +315,7 @@ let add_rewrite_hint ~poly bases ort t lcsr =
in
CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in
let eqs = List.map f lcsr in
- let add_hints base = add_rew_rules base eqs in
+ let add_hints base = add_rew_rules ~locality base eqs in
List.iter add_hints bases
let classify_hint _ = VtSideff ([], VtLater)
@@ -323,15 +323,15 @@ let classify_hint _ = VtSideff ([], VtLater)
}
VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY { classify_hint }
-| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] ->
- { add_rewrite_hint ~poly:polymorphic bl o None l }
-| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
+| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] ->
+ { add_rewrite_hint ~locality ~poly:polymorphic bl o None l }
+| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
":" preident_list(bl) ] ->
- { add_rewrite_hint ~poly:polymorphic bl o (Some t) l }
-| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
- { add_rewrite_hint ~poly:polymorphic ["core"] o None l }
-| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
- { add_rewrite_hint ~poly:polymorphic ["core"] o (Some t) l }
+ { add_rewrite_hint ~locality ~poly:polymorphic bl o (Some t) l }
+| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
+ { add_rewrite_hint ~locality ~poly:polymorphic ["core"] o None l }
+| #[ polymorphic; locality = option_locality; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
+ { add_rewrite_hint ~locality ~poly:polymorphic ["core"] o (Some t) l }
END
(**********************************************************************)
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 069a342b2a..82b41e41bd 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -11,7 +11,6 @@
{
open Pp
-open Constr
open Stdarg
open Pcoq.Prim
open Pcoq.Constr
@@ -199,20 +198,6 @@ TACTIC EXTEND unify
END
{
-let deprecated_convert_concl_no_check =
- CWarnings.create
- ~name:"convert_concl_no_check" ~category:"deprecated"
- (fun () -> Pp.str "The syntax [convert_concl_no_check] is deprecated. Use [change_no_check] instead.")
-}
-
-TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> {
- deprecated_convert_concl_no_check ();
- Tactics.convert_concl ~check:false x DEFAULTcast
- }
-END
-
-{
let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid
let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index b1b96ea9a7..3da5b2bfc4 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -147,7 +147,7 @@ GRAMMAR EXTEND Gram
| 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 } ];
+ | g=failkw; n = [ n = nat_or_var -> { n } | -> { fail_default_value } ];
l = LIST0 message_token -> { TacFail (g,n,l) }
| st = simple_tactic -> { st }
| a = tactic_value -> { TacArg(CAst.make ~loc a) }
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 6bf330c830..e7902d06eb 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -151,13 +151,13 @@ VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY
END
VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY STATE read_program
-| [ "Obligations" "of" ident(name) ] -> { show_obligations (Some name) }
-| [ "Obligations" ] -> { show_obligations None }
+| [ "Obligations" "of" ident(name) ] -> { fun ~stack:_ -> show_obligations (Some name) }
+| [ "Obligations" ] -> { fun ~stack:_ -> show_obligations None }
END
VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY STATE read_program
-| [ "Preterm" "of" ident(name) ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm (Some name)) }
-| [ "Preterm" ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm None) }
+| [ "Preterm" "of" ident(name) ] -> { fun ~stack:_ ~pm -> Feedback.msg_notice (show_term ~pm (Some name)) }
+| [ "Preterm" ] -> { fun ~stack:_ ~pm -> Feedback.msg_notice (show_term ~pm None) }
END
{
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index aa2449d962..937d579012 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -436,11 +436,7 @@ let finish_timing ~prefix name =
(* ******************** *)
let print_results_filter ~cutoff ~filter =
- (* The STM doesn't provide yet a proper document query and traversal
- API, thus we need to re-check if some states are current anymore
- (due to backtracking) using the `state_of_id` API. *)
- let valid (did,id) _ = Stm.(state_of_id ~doc:(get_doc did) id) <> `Expired in
- data := SM.filter valid !data;
+ data := SM.filter (fun (doc,id) _ -> Stateid.is_valid ~doc id) !data;
let results =
SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in
let results = merge_roots results Local.(CList.last !stack) in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 6d0e0c36b3..c7bda43465 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -251,10 +251,10 @@ end) = struct
(** Folding/unfolding of the tactic constants. *)
- let unfold_impl sigma t =
+ let unfold_impl n sigma t =
match EConstr.kind sigma t with
| App (arrow, [| a; b |])(* when eq_constr arrow (Lazy.force impl) *) ->
- mkProd (make_annot Anonymous Sorts.Relevant, a, lift 1 b)
+ mkProd (make_annot n Sorts.Relevant, a, lift 1 b)
| _ -> assert false
let unfold_all sigma t =
@@ -273,16 +273,16 @@ end) = struct
| _ -> assert false)
| _ -> assert false
- let arrow_morphism env evd ta tb a b =
+ let arrow_morphism env evd n ta tb a b =
let ap = is_Prop (goalevars evd) ta and bp = is_Prop (goalevars evd) tb in
- if ap && bp then app_poly env evd impl [| a; b |], unfold_impl
+ if ap && bp then app_poly env evd impl [| a; b |], unfold_impl n
else if ap then (* Domain in Prop, CoDomain in Type *)
- (app_poly env evd arrow [| a; b |]), unfold_impl
+ (app_poly env evd arrow [| a; b |]), unfold_impl n
(* (evd, mkProd (Anonymous, a, b)), (fun x -> x) *)
else if bp then (* Dummy forall *)
- (app_poly env evd coq_all [| a; mkLambda (make_annot Anonymous Sorts.Relevant, a, lift 1 b) |]), unfold_forall
+ (app_poly env evd coq_all [| a; mkLambda (make_annot n Sorts.Relevant, a, lift 1 b) |]), unfold_forall
else (* None in Prop, use arrow *)
- (app_poly env evd arrow [| a; b |]), unfold_impl
+ (app_poly env evd arrow [| a; b |]), unfold_impl n
let rec decomp_pointwise sigma n c =
if Int.equal n 0 then c
@@ -1079,7 +1079,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let arr = if prop then PropGlobal.arrow_morphism
else TypeGlobal.arrow_morphism
in
- let (evars', mor), unfold = arr env evars tx tb x b in
+ let (evars', mor), unfold = arr env evars n.binder_name tx tb x b in
let state, res = aux { state ; env ; unfresh ;
term1 = mor ; ty1 = ty ;
cstr = (prop,cstr) ; evars = evars' } in
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index f2241e78d2..54d7c310aa 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2148,7 +2148,8 @@ let interp_redexp env sigma r =
(* Backwarding recursive needs of tactic glob/interp/eval functions *)
let _ =
- let eval lfun poly env sigma ty tac =
+ let eval ?loc ~poly env sigma tycon tac =
+ let lfun = GlobEnv.lfun env in
let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
let ist = { lfun; poly; extra; } in
let tac = eval_tactic_ist ist tac in
@@ -2156,8 +2157,13 @@ let _ =
poly seems like enough to get reasonable behavior in practice
*)
let name = Id.of_string "ltac_gen" in
- let (c, sigma) = Proof.refine_by_tactic ~name ~poly env sigma ty tac in
- (EConstr.of_constr c, sigma)
+ let sigma, ty = match tycon with
+ | Some ty -> sigma, ty
+ | None -> GlobEnv.new_type_evar env sigma ~src:(loc,Evar_kinds.InternalHole)
+ in
+ let (c, sigma) = Proof.refine_by_tactic ~name ~poly (GlobEnv.renamed_env env) sigma ty tac in
+ let j = { Environ.uj_val = EConstr.of_constr c; uj_type = ty } in
+ (j, sigma)
in
GlobEnv.register_constr_interp0 wit_tactic eval
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 11:55:45 +0000