aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/ltac/rewrite.ml4
-rw-r--r--plugins/omega/coq_omega.ml4
-rw-r--r--plugins/ssr/ssrtacticals.ml2
-rw-r--r--proofs/logic.ml4
-rw-r--r--proofs/logic.mli2
-rw-r--r--tactics/tactics.ml46
-rw-r--r--tactics/tactics.mli4
7 files changed, 34 insertions, 32 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 355c16bfd0..a68efa4713 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1575,7 +1575,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
let open Proofview.Notations in
(* For compatibility *)
let beta = Tactics.reduct_in_concl ~check:false (Reductionops.nf_betaiota, DEFAULTcast) in
- let beta_hyp id = Tactics.reduct_in_hyp ~check:false Reductionops.nf_betaiota (id, InHyp) in
+ let beta_hyp id = Tactics.reduct_in_hyp ~check:false ~reorder:false Reductionops.nf_betaiota (id, InHyp) in
let treat sigma res =
match res with
| None -> newfail 0 (str "Nothing to rewrite")
@@ -1596,7 +1596,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
tclTHENFIRST (assert_replacing id newt tac) (beta_hyp id)
| Some id, None ->
Proofview.Unsafe.tclEVARS undef <*>
- convert_hyp ~check:false (LocalAssum (make_annot id Sorts.Relevant, newt)) <*>
+ convert_hyp ~check:false ~reorder:false (LocalAssum (make_annot id Sorts.Relevant, newt)) <*>
beta_hyp id
| None, Some p ->
Proofview.Unsafe.tclEVARS undef <*>
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index f3bc791b8d..ffc3506a1f 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1849,12 +1849,12 @@ let destructure_hyps =
match destructurate_type env sigma typ with
| Kapp(Nat,_) ->
(tclTHEN
- (Tactics.convert_hyp ~check:false (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
+ (Tactics.convert_hyp ~check:false ~reorder:false (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
decl))
(loop lit))
| Kapp(Z,_) ->
(tclTHEN
- (Tactics.convert_hyp ~check:false (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|]))
+ (Tactics.convert_hyp ~check:false ~reorder:false (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|]))
decl))
(loop lit))
| _ -> loop lit
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 17e4114958..91ff432364 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -110,7 +110,7 @@ let endclausestac id_map clseq gl_id cl0 gl =
| _ -> EConstr.map (project gl) unmark c in
let utac hyp =
Proofview.V82.of_tactic
- (Tactics.convert_hyp ~check:false (NamedDecl.map_constr unmark hyp)) in
+ (Tactics.convert_hyp ~check:false ~reorder:false (NamedDecl.map_constr unmark hyp)) in
let utacs = List.map utac (pf_hyps gl) in
let ugtac gl' =
Proofview.V82.of_tactic
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 3fcde56e76..76eb79df39 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -548,7 +548,7 @@ and treat_case sigma goal ci lbrty lf acc' =
(lacc,sigma,fi::bacc))
(acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags
-let convert_hyp ~check env sigma d =
+let convert_hyp ~check ~reorder env sigma d =
let id = NamedDecl.get_id d in
let b = NamedDecl.get_value d in
let sign = Environ.named_context_val env in
@@ -565,7 +565,7 @@ let convert_hyp ~check env sigma d =
user_err ~hdr:"Logic.convert_hyp"
(str "Incorrect change of the body of "++ Id.print id ++ str ".");
let sign' = apply_to_hyp sign id (fun _ _ _ -> EConstr.Unsafe.to_named_decl d) in
- if check then reorder_val_context env sigma sign' (check_decl_position env sigma sign d)
+ if reorder then reorder_val_context env sigma sign' (check_decl_position env sigma sign d)
else sign'
(************************************************************************)
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 163d71f69c..406fe57985 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -62,7 +62,7 @@ type 'id move_location =
val pr_move_location :
('a -> Pp.t) -> 'a move_location -> Pp.t
-val convert_hyp : check:bool -> Environ.env -> evar_map ->
+val convert_hyp : check:bool -> reorder:bool -> Environ.env -> evar_map ->
EConstr.named_declaration -> Environ.named_context_val
val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t move_location ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 78e7ce2321..077c9aa619 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -163,12 +163,12 @@ let convert_concl ~check ty k =
end
end
-let convert_hyp ~check d =
+let convert_hyp ~check ~reorder d =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let ty = Proofview.Goal.concl gl in
- let sign = convert_hyp ~check env sigma d in
+ let sign = convert_hyp ~check ~reorder env sigma d in
let env = reset_with_named_context sign env in
Refine.refine ~typecheck:false begin fun sigma ->
Evarutil.new_evar env sigma ~principal:true ty
@@ -176,7 +176,7 @@ let convert_hyp ~check d =
end
let convert_concl_no_check = convert_concl ~check:false
-let convert_hyp_no_check = convert_hyp ~check:false
+let convert_hyp_no_check = convert_hyp ~check:false ~reorder:false
let convert_gen pb x y =
Proofview.Goal.enter begin fun gl ->
@@ -709,16 +709,16 @@ let e_change_in_concl ~check (redfun, sty) =
(convert_concl ~check c' sty)
end
-let e_change_in_hyp ~check redfun (id,where) =
+let e_change_in_hyp ~check ~reorder redfun (id,where) =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let hyp = Tacmach.New.pf_get_hyp id gl in
let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
- (convert_hyp ~check c)
+ (convert_hyp ~check ~reorder c)
end
-let e_change_in_hyps ~check f args =
+let e_change_in_hyps ~check ~reorder f args =
Proofview.Goal.enter begin fun gl ->
let fold (env, sigma) arg =
let (redfun, id, where) = f arg in
@@ -728,7 +728,7 @@ let e_change_in_hyps ~check f args =
raise (RefinerError (env, sigma, NoSuchHyp id))
in
let (sigma, d) = e_pf_change_decl redfun where hyp env sigma in
- let sign = Logic.convert_hyp ~check env sigma d in
+ let sign = Logic.convert_hyp ~check ~reorder env sigma d in
let env = reset_with_named_context sign env in
(env, sigma)
in
@@ -749,19 +749,19 @@ let reduct_in_concl ~check (redfun, sty) =
let redfun env sigma c = (sigma, redfun env sigma c) in
e_change_in_concl ~check (redfun, sty)
-let e_reduct_in_hyp ~check redfun (id, where) =
+let e_reduct_in_hyp ~check ~reorder redfun (id, where) =
let redfun _ env sigma c = redfun env sigma c in
- e_change_in_hyp ~check redfun (id, where)
+ e_change_in_hyp ~check ~reorder redfun (id, where)
-let reduct_in_hyp ~check redfun (id, where) =
+let reduct_in_hyp ~check ~reorder redfun (id, where) =
let redfun _ env sigma c = (sigma, redfun env sigma c) in
- e_change_in_hyp ~check redfun (id, where)
+ e_change_in_hyp ~check ~reorder redfun (id, where)
let revert_cast (redfun,kind as r) =
if kind == DEFAULTcast then (redfun,REVERTcast) else r
let e_reduct_option ~check redfun = function
- | Some id -> e_reduct_in_hyp ~check (fst redfun) id
+ | Some id -> e_reduct_in_hyp ~check ~reorder:check (fst redfun) id
| None -> e_change_in_concl ~check (revert_cast redfun)
let reduct_option ~check (redfun, sty) where =
@@ -833,7 +833,7 @@ let change_in_hyp ~check 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 (fun x -> change_on_subterm ~check Reduction.CONV x t occl) id
+ e_change_in_hyp ~check ~reorder:check (fun x -> change_on_subterm ~check Reduction.CONV x t occl) id
let concrete_clause_of enum_hyps cl = match cl.onhyps with
| None ->
@@ -855,7 +855,8 @@ let change ~check chg c cls =
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 f hyps
+ (* FIXME: don't check, we do it already *)
+ e_change_in_hyps ~check ~reorder:check f hyps
end
let change_concl t =
@@ -863,20 +864,20 @@ let change_concl t =
(* Pour usage interne (le niveau User est pris en compte par reduce) *)
let red_in_concl = reduct_in_concl ~check:false (red_product,REVERTcast)
-let red_in_hyp = reduct_in_hyp ~check:false red_product
+let red_in_hyp = reduct_in_hyp ~check:false ~reorder:false red_product
let red_option = reduct_option ~check:false (red_product,REVERTcast)
let hnf_in_concl = reduct_in_concl ~check:false (hnf_constr,REVERTcast)
-let hnf_in_hyp = reduct_in_hyp ~check:false hnf_constr
+let hnf_in_hyp = reduct_in_hyp ~check:false ~reorder:false hnf_constr
let hnf_option = reduct_option ~check:false (hnf_constr,REVERTcast)
let simpl_in_concl = reduct_in_concl ~check:false (simpl,REVERTcast)
-let simpl_in_hyp = reduct_in_hyp ~check:false simpl
+let simpl_in_hyp = reduct_in_hyp ~check:false ~reorder:false simpl
let simpl_option = reduct_option ~check:false (simpl,REVERTcast)
let normalise_in_concl = reduct_in_concl ~check:false (compute,REVERTcast)
-let normalise_in_hyp = reduct_in_hyp ~check:false compute
+let normalise_in_hyp = reduct_in_hyp ~check:false ~reorder:false compute
let normalise_option = reduct_option ~check:false (compute,REVERTcast)
let normalise_vm_in_concl = reduct_in_concl ~check:false (Redexpr.cbv_vm,VMcast)
let unfold_in_concl loccname = reduct_in_concl ~check:false (unfoldn loccname,REVERTcast)
-let unfold_in_hyp loccname = reduct_in_hyp ~check:false (unfoldn loccname)
+let unfold_in_hyp loccname = reduct_in_hyp ~check:false ~reorder:false (unfoldn loccname)
let unfold_option loccname = reduct_option ~check:false (unfoldn loccname,DEFAULTcast)
let pattern_option l = e_reduct_option ~check:false (pattern_occs l,DEFAULTcast)
@@ -907,7 +908,8 @@ let reduce redexp cl =
let redfun _ env sigma c = redfun env sigma c in
(redfun, id, where)
in
- e_change_in_hyps ~check f hyps
+ (* FIXME: sort out which flag is which *)
+ e_change_in_hyps ~check ~reorder:check f hyps
end
end
@@ -2654,7 +2656,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
[ Proofview.Unsafe.tclEVARS sigma;
convert_concl ~check:false newcl DEFAULTcast;
intro_gen (NamingMustBe (CAst.make id)) (decode_hyp lastlhyp) true false;
- Tacticals.New.tclMAP (convert_hyp ~check:false) depdecls;
+ Tacticals.New.tclMAP (convert_hyp ~check:false ~reorder:false) depdecls;
eq_tac ]
end
@@ -3061,7 +3063,7 @@ let unfold_body x =
Tacticals.New.afterHyp x begin fun aft ->
let hl = List.fold_right (fun decl cl -> (NamedDecl.get_id decl, InHyp) :: cl) aft [] in
let rfun _ _ c = replace_vars [x, xval] c in
- let reducth h = reduct_in_hyp ~check:false rfun h in
+ let reducth h = reduct_in_hyp ~check:false ~reorder:false rfun h in
let reductc = reduct_in_concl ~check:false (rfun, DEFAULTcast) in
Tacticals.New.tclTHENLIST [Tacticals.New.tclMAP reducth hl; reductc]
end
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 3bb9a34509..9eb8196280 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -34,7 +34,7 @@ val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool
val introduction : Id.t -> unit Proofview.tactic
val convert_concl : check:bool -> types -> cast_kind -> unit Proofview.tactic
-val convert_hyp : check:bool -> named_declaration -> unit Proofview.tactic
+val convert_hyp : check:bool -> reorder:bool -> named_declaration -> unit Proofview.tactic
val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
[@@ocaml.deprecated "use [Tactics.convert_concl]"]
val convert_hyp_no_check : named_declaration -> unit Proofview.tactic
@@ -152,7 +152,7 @@ type e_tactic_reduction = Reductionops.e_reduction_function
type change_arg = patvar_map -> env -> evar_map -> evar_map * constr
val make_change_arg : constr -> change_arg
-val reduct_in_hyp : check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic
+val reduct_in_hyp : check:bool -> reorder: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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:45:48 +0000