diff options
| -rw-r--r-- | pretyping/evarsolve.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/2830.v | 83 |
2 files changed, 84 insertions, 1 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index a63f1b1c84..f29d982c2d 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -783,7 +783,7 @@ let eq_filter f1 f2 = let closure_of_filter evd evk filter = let evi = Evd.find_undefined evd evk in - let vars = collect_vars (evar_concl evi) in + let vars = collect_vars (Evarutil.nf_evar evd (evar_concl evi)) in let ids = List.map pi1 (evar_context evi) in let test id b = b || Id.Set.mem id vars in let newfilter = List.map2 test ids filter in diff --git a/test-suite/bugs/closed/2830.v b/test-suite/bugs/closed/2830.v index 2daff6123c..876cad006e 100644 --- a/test-suite/bugs/closed/2830.v +++ b/test-suite/bugs/closed/2830.v @@ -1,3 +1,9 @@ +(* Bug report #2830 (evar defined twice) covers different bugs *) + +(* This was submitted by Anthony Crowley *) + +Module A. + Set Implicit Arguments. Inductive Bit := O | I. @@ -28,3 +34,80 @@ Fail Fixpoint StringOr (n m: nat) (a: BitString n) (b: BitString m) := | bitStr b' bT => bitStr (BitOr a' b') (StringOr aT bT) end end. + +End A. + +(* This was submitted by Andrew Appel *) + +Module B. + +Require Import Program Relations. + +Record ageable_facts (A:Type) (level: A -> nat) (age1:A -> option A) := +{ af_unage : forall x x' y', level x' = level y' -> age1 x = Some x' -> exists y, age1 y = Some y' +; af_level1 : forall x, age1 x = None <-> level x = 0 +; af_level2 : forall x y, age1 x = Some y -> level x = S (level y) +}. + +Implicit Arguments af_unage [[A] [level] [age1]]. +Implicit Arguments af_level1 [[A] [level] [age1]]. +Implicit Arguments af_level2 [[A] [level] [age1]]. + +Class ageable (A:Type) := mkAgeable +{ level : A -> nat +; age1 : A -> option A +; age_facts : ageable_facts A level age1 +}. +Definition age {A} `{ageable A} (x y:A) := age1 x = Some y. +Definition necR {A} `{ageable A} : relation A := clos_refl_trans A age. +Delimit Scope pred with pred. +Local Open Scope pred. + +Definition hereditary {A} (R:A->A->Prop) (p:A->Prop) := + forall a a':A, R a a' -> p a -> p a'. + +Definition pred (A:Type) {AG:ageable A} := + { p:A -> Prop | hereditary age p }. + +Bind Scope pred with pred. + +Definition app_pred {A} `{ageable A} (p:pred A) : A -> Prop := proj1_sig p. +Definition pred_hereditary `{ageable} (p:pred A) := proj2_sig p. +Coercion app_pred : pred >-> Funclass. +Global Opaque pred. + +Definition derives {A} `{ageable A} (P Q:pred A) := forall a:A, P a -> Q a. +Implicit Arguments derives. + +Program Definition andp {A} `{ageable A} (P Q:pred A) : pred A := + fun a:A => P a /\ Q a. +Next Obligation. + intros; intro; intuition; apply pred_hereditary with a; auto. +Qed. + +Program Definition imp {A} `{ageable A} (P Q:pred A) : pred A := + fun a:A => forall a':A, necR a a' -> P a' -> Q a'. +Next Obligation. + intros; intro; intuition. + apply H1; auto. + apply rt_trans with a'; auto. + apply rt_step; auto. +Qed. + +Program Definition allp {A} `{ageable A} {B: Type} (f: B -> pred A) : pred A + := fun a => forall b, f b a. +Next Obligation. + intros; intro; intuition. + apply pred_hereditary with a; auto. + apply H1. +Qed. + +Notation "P '<-->' Q" := (andp (imp P Q) (imp Q P)) (at level 57, no associativity) : pred. +Notation "P '|--' Q" := (derives P Q) (at level 80, no associativity). +Notation "'All' x ':' T ',' P " := (allp (fun x:T => P%pred)) (at level 65, x at level 99) : pred. + +Lemma forall_pred_ext {A} `{agA : ageable A}: forall B P Q, + (All x : B, (P x <--> Q x)) |-- (All x : B, P x) <--> (All x: B, Q x). +Abort. + +End B. |