diff options
| -rw-r--r-- | tactics/eauto.ml4 | 6 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 6 |
2 files changed, 7 insertions, 5 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index fd5310e04..bc3ad026c 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -545,10 +545,12 @@ let autounfold_one db cl gl = let (ids, csts) = Hint_db.unfolds db in (Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db in - let did, c' = unfold_head (pf_env gl) st (match cl with Some (id, _) -> pf_get_hyp_typ gl id | None -> pf_concl gl) in + let did, c' = unfold_head (pf_env gl) st + (match cl with Some (id, _) -> pf_get_hyp_typ gl id | None -> pf_concl gl) + in if did then match cl with - | Some hyp -> change_in_hyp None c' hyp gl + | Some hyp -> change_in_hyp None (fun env sigma -> sigma, c') hyp gl | None -> convert_concl_no_check c' DEFAULTcast gl else tclFAIL 0 (str "Nothing to unfold") gl diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 9cb22e5ea..6adec45bc 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -640,7 +640,7 @@ let hResolve id c occ t gl = let sigma = Evd.merge_universe_context sigma ctx in let t_constr_type = Retyping.get_type_of env sigma t_constr in tclTHEN (Refiner.tclEVARS sigma) - (change_in_concl None (mkLetIn (Anonymous,t_constr,t_constr_type,pf_concl gl))) gl + (change_concl (mkLetIn (Anonymous,t_constr,t_constr_type,pf_concl gl))) gl let hResolve_auto id c t gl = let rec resolve_auto n = @@ -669,7 +669,7 @@ let hget_evar n gl = if n <= 0 then error "Incorrect existential variable index."; let ev = List.nth evl (n-1) in let ev_type = existential_type sigma ev in - change_in_concl None (mkLetIn (Anonymous,mkEvar ev,ev_type,pf_concl gl)) gl + change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,pf_concl gl)) gl TACTIC EXTEND hget_evar | [ "hget_evar" int_or_var(n) ] -> [ Proofview.V82.tactic (hget_evar (out_arg n)) ] @@ -715,7 +715,7 @@ let mkCaseEq a : unit Proofview.tactic = let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in Proofview.V82.tactic begin - change_in_concl None + change_concl (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl) end end; |