From 6ff8870f57797f9bf7c340fb6a4b561e521a1325 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 19 Dec 2018 10:51:04 +0100
Subject: Fix #7904: update proofview env after ltac constr:()

(in case of side effects)

Also:
Fix #4781
Fix #4496
---
 plugins/ltac/tacinterp.ml         |  4 +-
 test-suite/bugs/closed/bug_4781.v | 96 +++++++++++++++++++++++++++++++++++++++
 test-suite/bugs/closed/bug_7904.v | 13 ++++++
 test-suite/bugs/opened/bug_4781.v | 94 --------------------------------------
 4 files changed, 112 insertions(+), 95 deletions(-)
 create mode 100644 test-suite/bugs/closed/bug_4781.v
 create mode 100644 test-suite/bugs/closed/bug_7904.v
 delete mode 100644 test-suite/bugs/opened/bug_4781.v

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 816741b894..5a9c8ff641 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1957,7 +1957,9 @@ let lifts f = (); fun ist x -> Ftactic.enter begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
   let (sigma, v) = f ist env sigma x in
   Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-  (Ftactic.return v)
+    (* FIXME once we don't need to catch side effects *)
+    (Proofview.tclTHEN (Proofview.Unsafe.tclSETENV (Global.env()))
+       (Ftactic.return v))
 end
 
 let interp_bindings' ist bl = Ftactic.return begin fun env sigma ->
diff --git a/test-suite/bugs/closed/bug_4781.v b/test-suite/bugs/closed/bug_4781.v
new file mode 100644
index 0000000000..464a3de1b3
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4781.v
@@ -0,0 +1,96 @@
+Ltac force_clear :=
+  clear;
+  repeat match goal with
+         | [ H : _ |- _ ] => clear H
+         | [ H := _ |- _ ] => clearbody H
+         end.
+
+Class abstract_term {T} (x : T) := by_abstract_term : T.
+Hint Extern 0 (@abstract_term ?T ?x) => force_clear; change T; abstract (exact x) : typeclass_instances.
+
+Goal True.
+(* These work: *)
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  pose x.
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := (eval cbv iota in (let v : T := x in v)) in
+  pose x.
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := match constr:(Set) with ?y => constr:(y) end in
+  pose x.
+(* This fails with an error: *)
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := match constr:(x) with ?y => constr:(y) end in
+  pose x. (* The command has indeed failed with message:
+Error: Variable y should be bound to a term. *)
+(* And the rest fail with Anomaly: Uncaught exception Not_found. Please report. *)
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := match constr:(x) with ?y => y end in
+  pose x.
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := (eval cbv iota in x) in
+  pose x.
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := type of x in
+  pose x. (* should succeed *)
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:(_ : abstract_term term) in
+  let x := type of x in
+  pose x. (* should succeed *)
+
+(*Apparently what [cbv iota] doesn't see can't hurt it, and [pose] is perfectly happy with abstracted lemmas only some of the time.
+
+Even stranger, consider:*)
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let y := (eval cbv iota in (let v : T := x in v)) in
+  pose y;
+    let x' := fresh "x'" in
+    pose x as x'.
+      let x := (eval cbv delta [x'] in x') in
+      pose x;
+      let z := (eval cbv iota in x) in
+      pose z.
+
+(*This works fine.  But if I change the period to a semicolon, I get:*)
+
+      let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let y := (eval cbv iota in (let v : T := x in v)) in
+  pose y;
+    let x' := fresh "x'" in
+    pose x as x';
+      let x := (eval cbv delta [x'] in x') in
+      pose x. (* Anomaly: Uncaught exception Not_found. Please report. *)
+ (* should succeed *)
+(*and if I use the second one instead of [pose x] (note that using [idtac] works fine), I get:*)
+
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let y := (eval cbv iota in (let v : T := x in v)) in
+  pose y;
+    let x' := fresh "x'" in
+    pose x as x';
+      let x := (eval cbv delta [x'] in x') in
+      let z := (eval cbv iota in x) in (* Error: Variable x should be bound to a term. *)
+      idtac. (* should succeed *)
+  exact I.
+Qed.
diff --git a/test-suite/bugs/closed/bug_7904.v b/test-suite/bugs/closed/bug_7904.v
new file mode 100644
index 0000000000..1e518e2adf
--- /dev/null
+++ b/test-suite/bugs/closed/bug_7904.v
@@ -0,0 +1,13 @@
+
+
+Class abstract_term {T} (x : T) := by_abstract_term : T.
+Hint Extern 0 (@abstract_term ?T ?x) => change T; abstract (exact x) : typeclass_instances.
+
+Goal True.
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := match constr:(x) with ?y => y end in
+  pose x as v. (* was Error: Variable x should be bound to a term but is bound to a constr. *)
+  exact v.
+Qed.
diff --git a/test-suite/bugs/opened/bug_4781.v b/test-suite/bugs/opened/bug_4781.v
deleted file mode 100644
index 8b651ac22e..0000000000
--- a/test-suite/bugs/opened/bug_4781.v
+++ /dev/null
@@ -1,94 +0,0 @@
-Ltac force_clear :=
-  clear;
-  repeat match goal with
-         | [ H : _ |- _ ] => clear H
-         | [ H := _ |- _ ] => clearbody H
-         end.
-
-Class abstract_term {T} (x : T) := by_abstract_term : T.
-Hint Extern 0 (@abstract_term ?T ?x) => force_clear; change T; abstract (exact x) : typeclass_instances.
-
-Goal True.
-(* These work: *)
-  let term := constr:(I) in
-  let T := type of term in
-  let x := constr:((_ : abstract_term term) : T) in
-  pose x.
-  let term := constr:(I) in
-  let T := type of term in
-  let x := constr:((_ : abstract_term term) : T) in
-  let x := (eval cbv iota in (let v : T := x in v)) in
-  pose x.
-  let term := constr:(I) in
-  let T := type of term in
-  let x := constr:((_ : abstract_term term) : T) in
-  let x := match constr:(Set) with ?y => constr:(y) end in
-  pose x.
-(* This fails with an error: *)
-  Fail let term := constr:(I) in
-  let T := type of term in
-  let x := constr:((_ : abstract_term term) : T) in
-  let x := match constr:(x) with ?y => constr:(y) end in
-  pose x. (* The command has indeed failed with message:
-Error: Variable y should be bound to a term. *)
-(* And the rest fail with Anomaly: Uncaught exception Not_found. Please report. *)
-  Fail let term := constr:(I) in
-  let T := type of term in
-  let x := constr:((_ : abstract_term term) : T) in
-  let x := match constr:(x) with ?y => y end in
-  pose x.
-  Fail let term := constr:(I) in
-  let T := type of term in
-  let x := constr:((_ : abstract_term term) : T) in
-  let x := (eval cbv iota in x) in
-  pose x.
-  Fail let term := constr:(I) in
-  let T := type of term in
-  let x := constr:((_ : abstract_term term) : T) in
-  let x := type of x in
-  pose x. (* should succeed *)
-  Fail let term := constr:(I) in
-  let T := type of term in
-  let x := constr:(_ : abstract_term term) in
-  let x := type of x in
-  pose x. (* should succeed *)
-
-(*Apparently what [cbv iota] doesn't see can't hurt it, and [pose] is perfectly happy with abstracted lemmas only some of the time.
-
-Even stranger, consider:*)
-  let term := constr:(I) in
-  let T := type of term in
-  let x := constr:((_ : abstract_term term) : T) in
-  let y := (eval cbv iota in (let v : T := x in v)) in
-  pose y;
-    let x' := fresh "x'" in
-    pose x as x'.
-      let x := (eval cbv delta [x'] in x') in
-      pose x;
-      let z := (eval cbv iota in x) in
-      pose z.
-
-(*This works fine.  But if I change the period to a semicolon, I get:*)
-
-      Fail let term := constr:(I) in
-  let T := type of term in
-  let x := constr:((_ : abstract_term term) : T) in
-  let y := (eval cbv iota in (let v : T := x in v)) in
-  pose y;
-    let x' := fresh "x'" in
-    pose x as x';
-      let x := (eval cbv delta [x'] in x') in
-      pose x. (* Anomaly: Uncaught exception Not_found. Please report. *)
- (* should succeed *)
-(*and if I use the second one instead of [pose x] (note that using [idtac] works fine), I get:*)
-
- Fail  let term := constr:(I) in
-  let T := type of term in
-  let x := constr:((_ : abstract_term term) : T) in
-  let y := (eval cbv iota in (let v : T := x in v)) in
-  pose y;
-    let x' := fresh "x'" in
-    pose x as x';
-      let x := (eval cbv delta [x'] in x') in
-      let z := (eval cbv iota in x) in (* Error: Variable x should be bound to a term. *)
-      idtac. (* should succeed *)
-- 
cgit v1.2.3