From b818c00e3e895ea9b736ab968e3ba109b0fd67c1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 27 Sep 2017 00:09:59 +0200
Subject: Fixing an old bug in collecting evars with cleared context.

The function Proofview.undefined was collecting twice the evars that
had advanced. Consequently, the functions Proofview.unshelve and
Proofview.with_shelf were possibly doing the same.
---
 test-suite/success/unshelve.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/unshelve.v b/test-suite/success/unshelve.v
index 672222bdd6..a4fa544cd9 100644
--- a/test-suite/success/unshelve.v
+++ b/test-suite/success/unshelve.v
@@ -9,3 +9,11 @@ unshelve (refine (F _ _ _ _)).
 + exact (@eq_refl bool true).
 + exact (@eq_refl unit tt).
 Qed.
+
+(* This was failing in 8.6, because of ?a:nat being wrongly duplicated *)
+
+Goal (forall a : nat, a = 0 -> True) -> True.
+intros F.
+unshelve (eapply (F _);clear F).
+2:reflexivity.
+Qed.
-- 
cgit v1.2.3


From 05bd0ab1dd85764874ca077005dcaff5414589a5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 26 Sep 2017 16:37:26 +0200
Subject: Moving setting of "cleared" evar flag directly in Evd.restrict.

In particular, this fixes #5757 which used restrict_evar to refine the
information on the source of an evar, and which should have set the
"cleared" flag.

Also renaming flag "restricted" since it is not only about "clear".

I guess this is what we want in general, but I did not survey all uses
of restrict_evar so, maybe, this should be refined further.
---
 test-suite/bugs/closed/5757.v | 76 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 76 insertions(+)
 create mode 100644 test-suite/bugs/closed/5757.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5757.v b/test-suite/bugs/closed/5757.v
new file mode 100644
index 0000000000..0d0f2eed44
--- /dev/null
+++ b/test-suite/bugs/closed/5757.v
@@ -0,0 +1,76 @@
+(* Check that resolved status of evars follows "restrict" *)
+
+Axiom H : forall (v : nat), Some 0 = Some v -> True.
+Lemma L : True.
+eapply H with _;
+match goal with
+  | |- Some 0 = Some ?v => change (Some (0+0) = Some v)
+end.
+Abort.
+
+(* The original example *)
+
+Set Default Proof Using "Type".
+
+Module heap_lang.
+
+Inductive expr :=
+  | InjR (e : expr).
+
+Inductive val :=
+  | InjRV (v : val).
+
+Bind Scope val_scope with val.
+
+Fixpoint of_val (v : val) : expr :=
+  match v with
+  | InjRV v => InjR (of_val v)
+  end.
+
+Fixpoint to_val (e : expr) : option val := None.
+
+End heap_lang.
+Export heap_lang.
+
+Module W.
+Inductive expr :=
+  | Val (v : val)
+  (* Sums *)
+  | InjR (e : expr).
+
+Fixpoint to_expr (e : expr) : heap_lang.expr :=
+  match e with
+  | Val v => of_val v
+  | InjR e => heap_lang.InjR (to_expr e)
+  end.
+
+End W.
+
+
+
+Section Tests.
+
+  Context (iProp: Type).
+  Context (WPre: expr -> Prop).
+
+  Context (tac_wp_alloc :
+             forall (e : expr) (v : val),
+               to_val e = Some v -> WPre e).
+
+  Lemma push_atomic_spec (x: val) :
+    WPre (InjR (of_val x)).
+  Proof.
+(* This works. *)
+eapply tac_wp_alloc with _.
+match goal with
+  | |- to_val ?e = Some ?v =>
+    change (to_val (W.to_expr (W.InjR (W.Val x))) = Some v)
+end.
+Undo. Undo.
+(* This is fixed *)
+eapply tac_wp_alloc with _;
+match goal with
+  | |- to_val ?e = Some ?v =>
+    change (to_val (W.to_expr (W.InjR (W.Val x))) = Some v)
+end.
+Abort.
-- 
cgit v1.2.3