aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/btauto/refl_btauto.ml2
-rw-r--r--plugins/fourier/fourierR.ml2
-rw-r--r--plugins/funind/recdef.ml3
-rw-r--r--plugins/micromega/coq_micromega.ml4
-rw-r--r--plugins/romega/refl_omega.ml2
-rw-r--r--tactics/rewrite.ml4
-rw-r--r--tactics/tacinterp.ml24
-rw-r--r--tactics/tactics.ml30
-rw-r--r--tactics/tactics.mli10
-rw-r--r--test-suite/bugs/closed/HoTT_coq_036.v6
-rw-r--r--test-suite/bugs/closed/HoTT_coq_054.v4
11 files changed, 52 insertions, 39 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 6a0f4d852..dbd89019e 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -247,7 +247,7 @@ module Btauto = struct
let fr = reify env fr in
let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (Tactics.change_in_concl None changed_gl);
+ Proofview.V82.tactic (Tactics.change_concl changed_gl);
Proofview.V82.tactic (Tactics.apply (Lazy.force soundness));
Proofview.V82.tactic (Tactics.normalise_vm_in_concl);
try_unification env
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 1f6ece602..7c134da7a 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -587,7 +587,7 @@ let rec fourier gl=
else tac_zero_infeq_false gl (rational_to_fraction cres)
in
tac:=(tclTHENS (my_cut ineq)
- [tclTHEN (change_in_concl None
+ [tclTHEN (change_concl
(mkAppL [| get coq_not; ineq|]
))
(tclTHEN (apply (if sres then get coq_Rnot_lt_lt
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index f141d3619..38cbd0c53 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -668,7 +668,8 @@ let mkDestructEq :
[Simple.generalize new_hyps;
(fun g2 ->
change_in_concl None
- (pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) Evd.empty (pf_concl g2)) g2);
+ (fun env sigma ->
+ sigma, pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) Evd.empty (pf_concl g2)) g2);
Proofview.V82.of_tactic (simplest_case expr)]), to_revert
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index d11454b27..ebd042022 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1378,7 +1378,7 @@ let micromega_order_change spec cert cert_typ env ff gl =
let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[|spec.coeff|])) in
let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in
let vm = dump_varmap (spec.typ) env in
- Tactics.change_in_concl None
+ Tactics.change_concl
(set
[
("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
@@ -1666,7 +1666,7 @@ let micromega_order_changer cert env ff gl =
let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in
let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in
let vm = dump_varmap (typ) env in
- Tactics.change_in_concl None
+ Tactics.change_concl
(set
[
("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index c5a0f798c..e22816c13 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1282,7 +1282,7 @@ let resolution env full_reified_goal systems_list =
Tactics.generalize
(l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >>
- Tactics.change_in_concl None reified >>
+ Tactics.change_concl reified >>
Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|]) >>
show_goal >>
Tactics.normalise_vm_in_concl >>
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 8794557ef..aa32e0e5c 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1396,13 +1396,13 @@ let cl_rewrite_clause_tac ?abs strat meta clause gl =
| Some id, Some p ->
cut_replacing id newt (Tacmach.refine p)
| Some id, None ->
- change_in_hyp None newt (id, InHypTypeOnly)
+ change_in_hyp None (fun env sigma -> sigma, newt) (id, InHypTypeOnly)
| None, Some p ->
let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
tclTHENLAST
(Tacmach.internal_cut false name newt)
(tclTHEN (Proofview.V82.of_tactic (Tactics.revert [name])) (Tacmach.refine p))
- | None, None -> change_in_concl None newt
+ | None, None -> change_in_concl None (fun env sigma -> sigma, newt)
in tclTHEN (evartac undef) tac
in
let tac =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ca582c82f..97cb50a28 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1710,13 +1710,11 @@ and interp_atomic ist tac : unit Proofview.tactic =
| AllOccurrences | NoOccurrences -> true
| _ -> false
in
- let (sigma,c_interp) =
+ let c_interp env sigma =
if is_onhyps && is_onconcl
- then pf_interp_type ist gl c
- else pf_interp_constr ist gl c
+ then interp_type ist env sigma c
+ else interp_constr ist env sigma c
in
- tclTHEN
- (tclEVARS sigma)
(Tactics.change None c_interp (interp_clause ist (pf_env gl) cl))
gl
end
@@ -1728,16 +1726,14 @@ and interp_atomic ist tac : unit Proofview.tactic =
Proofview.V82.tactic begin fun gl ->
let sign,op = interp_typed_pattern ist env sigma op in
let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
- let env' = Environ.push_named_context sign env in
- let (sigma',c_interp) =
- try interp_constr ist env' sigma c
- with e when to_catch e (* Hack *) ->
- errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
+ let c_interp env sigma =
+ let env' = Environ.push_named_context sign env in
+ try interp_constr ist env' sigma c
+ with e when to_catch e (* Hack *) ->
+ errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
in
- tclTHEN
- (tclEVARS sigma')
- (Tactics.change (Some op) c_interp (interp_clause ist env cl))
- gl
+ (Tactics.change (Some op) c_interp (interp_clause ist env cl))
+ gl
end
end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c7fc4197e..f65f295b2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -345,19 +345,30 @@ let e_reduct_in_hyp redfun (id,where) gl =
(e_pf_reduce_decl redfun where (pf_get_hyp gl id))
convert_hyp_no_check gl
+type change_arg = env -> evar_map -> evar_map * constr
+
(* Now we introduce different instances of the previous tacticals *)
let change_and_check cv_pb t env sigma c =
- let evd, b = infer_conv ~pb:cv_pb env sigma t c in
- if b then evd, t
- else
- errorlabstrm "convert-check-hyp" (str "Not convertible.")
-
+ let sigma, t' = t env sigma in
+ let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in
+ if b then sigma, t'
+ else raise ConstrMatching.PatternMatchingFailure
+
+let change_and_check_subst cv_pb subst t env sigma c =
+ let t' env sigma =
+ let sigma, t = t env sigma in
+ sigma, replace_vars (Id.Map.bindings subst) t
+ in change_and_check cv_pb t' env sigma c
+
(* Use cumulativity only if changing the conclusion not a subterm *)
let change_on_subterm cv_pb t = function
- | None -> change_and_check cv_pb t
+ | None -> fun env sigma c ->
+ (try change_and_check cv_pb t env sigma c
+ with ConstrMatching.PatternMatchingFailure ->
+ errorlabstrm "convert-check-hyp" (str "Not convertible."))
| Some occl ->
- e_contextually false occl
- (fun subst -> change_and_check Reduction.CONV (replace_vars (Id.Map.bindings subst) t))
+ e_contextually false occl
+ (fun subst -> change_and_check_subst Reduction.CONV subst t)
let change_in_concl occl t =
e_reduct_in_concl ((change_on_subterm Reduction.CUMUL t occl),DEFAULTcast)
@@ -378,6 +389,9 @@ let change chg c cls gl =
change_option (bind_change_occurrences occs chg) c None)
cls gl
+let change_concl t =
+ change_in_concl None (fun env sigma -> sigma, t)
+
(* Pour usage interne (le niveau User est pris en compte par reduce) *)
let red_in_concl = reduct_in_concl (red_product,REVERTcast)
let red_in_hyp = reduct_in_hyp red_product
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 6574d88c5..5951a4af8 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -117,12 +117,14 @@ val exact_proof : Constrexpr.constr_expr -> tactic
type tactic_reduction = env -> evar_map -> constr -> constr
+type change_arg = env -> evar_map -> evar_map * constr
+
val reduct_in_hyp : tactic_reduction -> hyp_location -> tactic
val reduct_option : tactic_reduction * cast_kind -> goal_location -> tactic
val reduct_in_concl : tactic_reduction * cast_kind -> tactic
-val change_in_concl : (occurrences * constr_pattern) option -> constr ->
- tactic
-val change_in_hyp : (occurrences * constr_pattern) option -> constr ->
+val change_in_concl : (occurrences * constr_pattern) option -> change_arg -> tactic
+val change_concl : constr -> tactic
+val change_in_hyp : (occurrences * constr_pattern) option -> change_arg ->
hyp_location -> tactic
val red_in_concl : tactic
val red_in_hyp : hyp_location -> tactic
@@ -144,7 +146,7 @@ val unfold_in_hyp :
val unfold_option :
(occurrences * evaluable_global_reference) list -> goal_location -> tactic
val change :
- constr_pattern option -> constr -> clause -> tactic
+ constr_pattern option -> change_arg -> clause -> tactic
val pattern_option :
(occurrences * constr) list -> goal_location -> tactic
val reduce : red_expr -> clause -> tactic
diff --git a/test-suite/bugs/closed/HoTT_coq_036.v b/test-suite/bugs/closed/HoTT_coq_036.v
index f10856bc7..4c3e078a5 100644
--- a/test-suite/bugs/closed/HoTT_coq_036.v
+++ b/test-suite/bugs/closed/HoTT_coq_036.v
@@ -29,8 +29,8 @@ Module Version1.
assert (Hf : focus ((S tt) = (S tt))) by constructor.
let C1 := constr:(CObject) in
let C2 := constr:(fun C => @Object (CObject C) C) in
- unify C1 C2.
- progress change CObject with (fun C => @Object (CObject C) C) in *.
+ unify C1 C2; idtac C1 C2. Show Universes.
+ progress change @CObject with (fun C => @Object (CObject C) C) in *.
simpl in *.
match type of Hf with
| focus ?V => exact V
@@ -112,7 +112,7 @@ Module OtherBug.
Parameter ObjectOf' : forall (objC : Type) (C : SpecializedCategory objC)
(objD : Type) (D : SpecializedCategory objD), Prop.
- Definition CommaCategory_Object (A : Category) : Type.
+ Definition CommaCategory_Object (A : Category@{i}) : Type.
assert (Hf : focus (@ObjectOf' _ (@Build_Category unit TerminalCategory) _ A)) by constructor.
progress change CObject with (fun C => @Object (CObject C) C) in *;
simpl in *.
diff --git a/test-suite/bugs/closed/HoTT_coq_054.v b/test-suite/bugs/closed/HoTT_coq_054.v
index f79fe1c1e..b47bb3a20 100644
--- a/test-suite/bugs/closed/HoTT_coq_054.v
+++ b/test-suite/bugs/closed/HoTT_coq_054.v
@@ -47,10 +47,10 @@ Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
| inl y' => ap g
| inr y' => idmap
end
- | inr x' => match y as y return match y with
+ | inr x' => match y as y return match y return Type with
inr y' => x' = y'
| _ => Empty
- end -> match f y with
+ end -> match f y return Type with
| inr y' => h x' = y'
| _ => Empty end with
| inl y' => idmap
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 12:22:16 +0000