aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extratactics.mlg22
-rw-r--r--plugins/ltac/g_auto.mlg15
-rw-r--r--plugins/ltac/g_ltac.mlg2
-rw-r--r--plugins/ltac/g_tactic.mlg8
-rw-r--r--plugins/ltac/rewrite.ml14
5 files changed, 27 insertions, 34 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 4a2c298caa..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
(**********************************************************************)
@@ -774,7 +774,7 @@ let rec find_a_destructable_match sigma t =
let cl = [cl, (None, None), None], None in
let dest = TacAtom (CAst.make @@ TacInductionDestruct(false, false, cl)) in
match EConstr.kind sigma t with
- | Case (_,_,_,x,_) when closed0 sigma x ->
+ | Case (_,_,_,_,_,x,_) when closed0 sigma x ->
if isVar sigma x then
(* TODO check there is no rel n. *)
raise (Found (Tacinterp.eval_tactic dest))
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_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 43957bbde5..cb430efb40 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -182,6 +182,11 @@ let merge_occurrences loc cl = function
in
(Some p, ans)
+let deprecated_conversion_at_with =
+ CWarnings.create
+ ~name:"conversion_at_with" ~category:"deprecated"
+ (fun () -> Pp.str "The syntax [at ... with ...] is deprecated. Use [with ... at ...] instead.")
+
(* Auxiliary grammar rules *)
open Pvernac.Vernac_
@@ -230,7 +235,8 @@ GRAMMAR EXTEND Gram
[ [ c = constr -> { (None, c) }
| c1 = constr; "with"; c2 = constr -> { (Some (AllOccurrences,c1),c2) }
| c1 = constr; "at"; occs = occs_nums; "with"; c2 = constr ->
- { (Some (occs,c1), c2) } ] ]
+ { deprecated_conversion_at_with (); (* 8.14 *)
+ (Some (occs,c1), c2) } ] ]
;
occs_nums:
[ [ nl = LIST1 nat_or_var -> { OnlyOccurrences nl }
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 59533eb3e3..6d0e0c36b3 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -918,7 +918,8 @@ let reset_env env =
Environ.push_rel_context (Environ.rel_context env) env'
let fold_match ?(force=false) env sigma c =
- let (ci, p, iv, c, brs) = destCase sigma c in
+ let case = destCase sigma c in
+ let (ci, p, iv, c, brs) = EConstr.expand_case env sigma case in
let cty = Retyping.get_type_of env sigma c in
let dep, pred, exists, sk =
let env', ctx, body =
@@ -986,7 +987,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let argty = Retyping.get_type_of env (goalevars evars) arg in
let state, res = s.strategy { state ; env ;
unfresh ;
- term1 = arg ; ty1 = argty ;
+ term1 = arg ; ty1 = argty ;
cstr = (prop,None) ;
evars } in
let res' =
@@ -1153,7 +1154,8 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
| Fail | Identity -> b'
in state, res
- | Case (ci, p, iv, c, brs) ->
+ | Case (ci, u, pms, p, iv, c, brs) ->
+ let (ci, p, iv, c, brs) = EConstr.expand_case env (goalevars evars) (ci, u, pms, p, iv, c, brs) in
let cty = Retyping.get_type_of env (goalevars evars) c in
let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in
let cstr' = Some eqty in
@@ -1163,7 +1165,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let state, res =
match c' with
| Success r ->
- let case = mkCase (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs) in
+ let case = mkCase (EConstr.contract_case env (goalevars evars) (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 (prop,cstr) res)
| Fail | Identity ->
@@ -1185,7 +1187,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
in
match found with
| Some r ->
- let ctxc = mkCase (ci, lift 1 p, map_invert (lift 1) iv, lift 1 c, Array.of_list (List.rev (brs' c'))) in
+ let ctxc = mkCase (EConstr.contract_case env (goalevars evars) (ci, lift 1 p, map_invert (lift 1) iv, lift 1 c, Array.of_list (List.rev (brs' c')))) in
state, Success (make_leibniz_proof env ctxc ty r)
| None -> state, c'
else
@@ -1386,7 +1388,7 @@ module Strategies =
let fold_glob c : 'a pure_strategy = { strategy =
fun { state ; env ; term1 = t ; ty1 = ty ; cstr ; evars } ->
-(* let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
+(* let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in
let unfolded =
try Tacred.try_red_product env sigma c
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 01:04:06 +0000