diff options
| -rw-r--r-- | tactics/rewrite.ml4 | 44 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2393.v | 3 | ||||
| -rw-r--r-- | test-suite/success/implicit.v | 3 | ||||
| -rw-r--r-- | test-suite/success/setoid_test.v | 36 |
4 files changed, 46 insertions, 40 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index ecc8631bf..8b277e6c2 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -298,7 +298,7 @@ let refresh_hypinfo env sigma hypinfo = match c with | Some c -> (* Refresh the clausenv to not get the same meta twice in the goal. *) - decompose_applied_relation env cl.evd c l2r; + decompose_applied_relation env sigma c l2r; | _ -> hypinfo else hypinfo @@ -307,6 +307,7 @@ let unify_eqn env sigma hypinfo t = else try let {cl=cl; prf=prf; car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=c; abs=abs} = !hypinfo in let left = if l2r then c1 else c2 in + let cl = { cl with evd = evars_reset_evd sigma cl.evd } in let env', prf, c1, c2, car, rel = match abs with | Some (absprf, absprfty) -> @@ -332,7 +333,7 @@ let unify_eqn env sigma hypinfo t = in if convertible env env'.evd ty1 ty2 then ( if occur_meta prf then - hypinfo := refresh_hypinfo env sigma !hypinfo; + hypinfo := refresh_hypinfo env env'.evd !hypinfo; env', prf, c1, c2, car, rel) else raise Reduction.NotConvertible in @@ -546,10 +547,9 @@ let apply_rule hypinfo loccs : strategy = | _ -> None let apply_lemma (evm,c) left2right loccs : strategy = - fun env sigma -> - let evars = Evd.merge sigma evm in - let hypinfo = ref (decompose_applied_relation env evars c left2right) in - apply_rule hypinfo loccs env sigma + fun env sigma t ty cstr evars -> + let hypinfo = ref (decompose_applied_relation env (goalevars evars) c left2right) in + apply_rule hypinfo loccs env sigma t ty cstr evars let make_leibniz_proof c ty r = let prf = @@ -902,10 +902,10 @@ let rewrite_strat flags occs hyp = in aux () let rewrite_with {it = c; sigma = evm} left2right loccs : strategy = - fun env sigma -> - let evars = Evd.merge sigma evm in - let hypinfo = ref (decompose_applied_relation env evars c left2right) in - rewrite_strat default_flags loccs hypinfo env sigma + fun env sigma t ty cstr evars -> + let gevars = Evd.merge evm (goalevars evars) in + let hypinfo = ref (decompose_applied_relation env gevars c left2right) in + rewrite_strat default_flags loccs hypinfo env sigma t ty cstr (gevars, cstrevars evars) let apply_strategy (s : strategy) env sigma concl cstr evars = let res = @@ -918,30 +918,6 @@ let apply_strategy (s : strategy) env sigma concl cstr evars = | Some (Some res) -> Some (Some (res.rew_prf, res.rew_evars, res.rew_car, res.rew_from, res.rew_to)) -let split_evars_once sigma evd = - Evd.fold_undefined (fun ev evi deps -> - if Intset.mem ev deps then - Intset.union (Evarutil.undefined_evars_of_evar_info evd evi) deps - else deps) evd sigma - -let existentials_of_evd evd = - Evd.fold_undefined (fun ev _ acc -> Intset.add ev acc) evd Intset.empty - -let evd_of_existentials evd exs = - Intset.fold - (fun ev acc -> - try Evd.add acc ev (Evd.find_undefined evd ev) - with Not_found -> acc) - exs Evd.empty - -let split_evars sigma evd = - let rec aux deps = - let deps' = split_evars_once deps evd in - if Intset.equal deps' deps then - evd_of_existentials evd deps - else aux deps' - in aux (existentials_of_evd sigma) - let merge_evars (goal,cstr) = Evd.merge goal cstr let solve_constraints env evars = Typeclasses.resolve_typeclasses env ~split:false ~fail:true diff --git a/test-suite/bugs/closed/shouldsucceed/2393.v b/test-suite/bugs/closed/shouldsucceed/2393.v index 6a559e75c..fb4f92619 100644 --- a/test-suite/bugs/closed/shouldsucceed/2393.v +++ b/test-suite/bugs/closed/shouldsucceed/2393.v @@ -11,6 +11,3 @@ Program Fixpoint idType (t : T) (n := sizeOf t) (b : vect n) {measure n} : T := match t with | MkT => MkT end. - -Require Import Wf_nat. -Solve Obligations using auto with arith. diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index f446cd2df..b28653831 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -120,6 +120,3 @@ Check C2 eq_refl. Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop := | C3 : I3 a (n:=0). - -Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop := - | C2 {p} : I2 a (n:=p). diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index 033b3f485..d5096ea65 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -130,3 +130,39 @@ intros f0 Q H. setoid_rewrite H. tauto. Qed. + +(** Check proper refreshing of the lemma application for multiple + different instances in a single setoid rewrite. *) + +Section mult. + Context (fold : forall {A} {B}, (A -> B) -> A -> B). + Context (add : forall A, A -> A). + Context (fold_lemma : forall {A B f} {eqA : relation B} x, eqA (fold A B f (add A x)) (fold _ _ f x)). + Context (ab : forall B, A -> B). + Context (anat : forall A, nat -> A). + +Goal forall x, (fold _ _ (fun x => ab A x) (add A x) = anat _ (fold _ _ (ab nat) (add _ x))). +Proof. intros. + setoid_rewrite fold_lemma. + change (fold A A (λ x0 : A, ab A x0) x = anat A (fold A nat (ab nat) x)). +Abort. + +End mult. + +(** Current semantics for rewriting with typeclass constraints in the lemma + fixes the instance at the first unification. Using @ to make them metavariables + allow different instances to be used. [at] can be used to select the instance + too. *) + +Require Import Arith. + +Class Foo (A : Type) := {foo_neg : A -> A ; foo_prf : forall x : A, x = foo_neg x}. +Instance: Foo nat. admit. Defined. +Instance: Foo bool. admit. Defined. + +Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y. +Proof. intros. setoid_rewrite <- foo_prf. change (beq_nat x 0 = foo_neg y). Abort. + +Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y. +Proof. intros. setoid_rewrite <- @foo_prf. change (beq_nat x 0 = y). Abort. + |