aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-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
-rw-r--r--tactics/tactics.ml33
-rw-r--r--tactics/tactics.mli8
9 files changed, 46 insertions, 32 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 *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b70dd63211..16bede0d1b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -802,15 +802,21 @@ let change_and_check cv_pb mayneedglobalcheck deep t env sigma c =
| Some sigma -> (sigma, t')
(* Use cumulativity only if changing the conclusion not a subterm *)
-let change_on_subterm cv_pb deep t where env sigma c =
+let change_on_subterm check cv_pb deep t where env sigma c =
let mayneedglobalcheck = ref false in
let (sigma, c) = match where with
- | None -> change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty) env sigma c
+ | None ->
+ if check then
+ change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty) env sigma c
+ else
+ t Id.Map.empty env sigma
| Some occl ->
e_contextually false occl
(fun subst ->
- change_and_check Reduction.CONV mayneedglobalcheck true (t subst))
- env sigma c in
+ if check then
+ change_and_check Reduction.CONV mayneedglobalcheck true (t subst)
+ else
+ fun env sigma _c -> t subst env sigma) env sigma c in
if !mayneedglobalcheck then
begin
try ignore (Typing.unsafe_type_of env sigma c)
@@ -819,14 +825,15 @@ let change_on_subterm cv_pb deep t where env sigma c =
end;
(sigma, c)
-let change_in_concl occl t =
- e_change_in_concl ~check:false ((change_on_subterm Reduction.CUMUL false t occl),DEFAULTcast)
+let change_in_concl ?(check=true) occl t =
+ (* No need to check in e_change_in_concl, the check is done in change_on_subterm *)
+ e_change_in_concl ~check:false ((change_on_subterm check Reduction.CUMUL false t occl),DEFAULTcast)
-let change_in_hyp occl t id =
+let change_in_hyp ?(check=true) occl t id =
(* FIXME: we set the [check] flag only to reorder hypotheses in case of
introduction of dependencies in new variables. We should separate this
check from the conversion function. *)
- e_change_in_hyp ~check:true (fun x -> change_on_subterm Reduction.CONV x t occl) id
+ e_change_in_hyp ~check:true (fun x -> change_on_subterm check Reduction.CONV x t occl) id
let concrete_clause_of enum_hyps cl = match cl.onhyps with
| None ->
@@ -835,24 +842,24 @@ let concrete_clause_of enum_hyps cl = match cl.onhyps with
| Some l ->
List.map (fun ((occs, id), w) -> (id, occs, w)) l
-let change chg c cls =
+let change ?(check=true) chg c cls =
Proofview.Goal.enter begin fun gl ->
let hyps = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in
begin match cls.concl_occs with
| NoOccurrences -> Proofview.tclUNIT ()
- | occs -> change_in_concl (bind_change_occurrences occs chg) c
+ | occs -> change_in_concl ~check (bind_change_occurrences occs chg) c
end
<*>
let f (id, occs, where) =
let occl = bind_change_occurrences occs chg in
- let redfun deep env sigma t = change_on_subterm Reduction.CONV deep c occl env sigma t in
+ let redfun deep env sigma t = change_on_subterm check Reduction.CONV deep c occl env sigma t in
(redfun, id, where)
in
e_change_in_hyps ~check:true f hyps
end
let change_concl t =
- change_in_concl None (make_change_arg t)
+ change_in_concl ~check:true None (make_change_arg t)
(* Pour usage interne (le niveau User est pris en compte par reduce) *)
let red_in_concl = reduct_in_concl (red_product,REVERTcast)
@@ -3280,7 +3287,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
if Int.equal i nparams then
let t = applist (hd, params@args) in
Tacticals.New.tclTHEN
- (change_in_hyp None (make_change_arg t) (hyp0,InHypTypeOnly))
+ (change_in_hyp ~check:false None (make_change_arg t) (hyp0,InHypTypeOnly))
(tac avoid)
else
let c = List.nth argl (i-1) in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index e7b95a820e..b3914816ac 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -155,10 +155,10 @@ val make_change_arg : constr -> change_arg
val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic
val reduct_option : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic
val reduct_in_concl : ?check:bool -> tactic_reduction * cast_kind -> unit Proofview.tactic
-val e_reduct_in_concl : ?check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic
-val change_in_concl : (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic
+val e_reduct_in_concl : ?check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic
+val change_in_concl : ?check:bool -> (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic
val change_concl : constr -> unit Proofview.tactic
-val change_in_hyp : (occurrences * constr_pattern) option -> change_arg ->
+val change_in_hyp : ?check:bool -> (occurrences * constr_pattern) option -> change_arg ->
hyp_location -> unit Proofview.tactic
val red_in_concl : unit Proofview.tactic
val red_in_hyp : hyp_location -> unit Proofview.tactic
@@ -180,7 +180,7 @@ val unfold_in_hyp :
val unfold_option :
(occurrences * evaluable_global_reference) list -> goal_location -> unit Proofview.tactic
val change :
- constr_pattern option -> change_arg -> clause -> unit Proofview.tactic
+ ?check:bool -> constr_pattern option -> change_arg -> clause -> unit Proofview.tactic
val pattern_option :
(occurrences * constr) list -> goal_location -> unit Proofview.tactic
val reduce : red_expr -> clause -> unit Proofview.tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:33:10 +0000