aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/g_tactic.mlg6
-rw-r--r--plugins/ltac/pptactic.ml5
-rw-r--r--plugins/ltac/tacexpr.ml3
-rw-r--r--plugins/ltac/tacexpr.mli3
-rw-r--r--plugins/ltac/tacintern.ml8
-rw-r--r--plugins/ltac/tacinterp.ml8
-rw-r--r--plugins/ltac/tacsubst.ml4
7 files changed, 22 insertions, 15 deletions
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index a2dd51643b..c23240b782 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -703,7 +703,11 @@ GRAMMAR EXTEND Gram
| IDENT "change"; c = conversion; cl = clause_dft_concl ->
{ let (oc, c) = c in
let p,cl = merge_occurrences loc cl oc in
- TacAtom (CAst.make ~loc @@ TacChange (p,c,cl)) }
+ TacAtom (CAst.make ~loc @@ TacChange (true,p,c,cl)) }
+ | IDENT "change_no_check"; c = conversion; cl = clause_dft_concl ->
+ { let (oc, c) = c in
+ let p,cl = merge_occurrences loc cl oc in
+ TacAtom (CAst.make ~loc @@ TacChange (false,p,c,cl)) }
] ]
;
END
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 80070a7493..79f0f521cc 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -833,9 +833,10 @@ let pr_goal_selector ~toplevel s =
pr_red_expr r
++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
)
- | TacChange (op,c,h) ->
+ | TacChange (check,op,c,h) ->
+ let name = if check then "change_no_check" else "change" in
hov 1 (
- primitive "change" ++ brk (1,1)
+ primitive name ++ brk (1,1)
++ (
match op with
None ->
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 30e316b36d..0eb7726a18 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -34,6 +34,7 @@ type rec_flag = bool (* true = recursive false = not recursive *)
type advanced_flag = bool (* true = advanced false = basic *)
type letin_flag = bool (* true = use local def false = use Leibniz *)
type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+type check_flag = bool (* true = check false = do not check *)
type ('c,'d,'id) inversion_strength =
| NonDepInversion of
@@ -125,7 +126,7 @@ type 'a gen_atomic_tactic_expr =
(* Conversion *)
| TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
- | TacChange of 'pat option * 'dtrm * 'nam clause_expr
+ | TacChange of check_flag * 'pat option * 'dtrm * 'nam clause_expr
(* Equality and inversion *)
| TacRewrite of evars_flag *
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 8b6b14322b..fd303f5d94 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -34,6 +34,7 @@ type rec_flag = bool (* true = recursive false = not recursive *)
type advanced_flag = bool (* true = advanced false = basic *)
type letin_flag = bool (* true = use local def false = use Leibniz *)
type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+type check_flag = bool (* true = check false = do not check *)
type ('c,'d,'id) inversion_strength =
| NonDepInversion of
@@ -124,7 +125,7 @@ type 'a gen_atomic_tactic_expr =
(* Conversion *)
| TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr
- | TacChange of 'pat option * 'dtrm * 'nam clause_expr
+ | TacChange of check_flag * 'pat option * 'dtrm * 'nam clause_expr
(* Equality and inversion *)
| TacRewrite of evars_flag *
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 543d4de0fe..c1f7fab123 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -551,7 +551,7 @@ let rec intern_atomic lf ist x =
| TacReduce (r,cl) ->
dump_glob_red_expr r;
TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl)
- | TacChange (None,c,cl) ->
+ | TacChange (check,None,c,cl) ->
let is_onhyps = match cl.onhyps with
| None | Some [] -> true
| _ -> false
@@ -560,17 +560,17 @@ let rec intern_atomic lf ist x =
| AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
| _ -> false
in
- TacChange (None,
+ TacChange (check,None,
(if is_onhyps && is_onconcl
then intern_type ist c else intern_constr ist c),
clause_app (intern_hyp_location ist) cl)
- | TacChange (Some p,c,cl) ->
+ | TacChange (check,Some p,c,cl) ->
let { ltacvars } = ist in
let metas,pat = intern_typed_pattern ist ~as_type:false ~ltacvars p in
let fold accu x = Id.Set.add x accu in
let ltacvars = List.fold_left fold ltacvars metas in
let ist' = { ist with ltacvars } in
- TacChange (Some pat,intern_constr ist' c,
+ TacChange (check,Some pat,intern_constr ist' c,
clause_app (intern_hyp_location ist) cl)
(* Equality and inversion *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 4398fb14ab..800be2565d 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1770,7 +1770,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl))
end
- | TacChange (None,c,cl) ->
+ | TacChange (check,None,c,cl) ->
(* spiwack: until the tactic is in the monad *)
Proofview.Trace.name_tactic (fun _ _ -> Pp.str"<change>") begin
Proofview.Goal.enter begin fun gl ->
@@ -1792,10 +1792,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
then interp_type ist env sigma c
else interp_constr ist env sigma c
in
- Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl)
+ Tactics.change ~check None c_interp (interp_clause ist (pf_env gl) (project gl) cl)
end
end
- | TacChange (Some op,c,cl) ->
+ | TacChange (check,Some op,c,cl) ->
(* spiwack: until the tactic is in the monad *)
Proofview.Trace.name_tactic (fun _ _ -> Pp.str"<change>") begin
Proofview.Goal.enter begin fun gl ->
@@ -1815,7 +1815,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
with e when to_catch e (* Hack *) ->
user_err (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
in
- Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)
+ Tactics.change ~check (Some op) c_interp (interp_clause ist env sigma cl)
end
end
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index e617f3d45e..a3eeca2267 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -158,8 +158,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
(* Conversion *)
| TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
- | TacChange (op,c,cl) ->
- TacChange (Option.map (subst_glob_constr_or_pattern subst) op,
+ | TacChange (check,op,c,cl) ->
+ TacChange (check,Option.map (subst_glob_constr_or_pattern subst) op,
subst_glob_constr subst c, cl)
(* Equality and inversion *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:41:56 +0000