Merge PR #9248: Fix #7904: update proofview env after ltac constr:()

3 files changed, 25 insertions, 8 deletions

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index ae4cd06022..3e7479903a 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/opened/bug_4781.v b/test-suite/bugs/closed/bug_4781.v
index 8b651ac22e..464a3de1b3 100644
--- a/test-suite/bugs/opened/bug_4781.v
+++ b/test-suite/bugs/closed/bug_4781.v
@@ -25,29 +25,29 @@ Goal True.
   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 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 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 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 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 term := constr:(I) in
   let T := type of term in
   let x := constr:(_ : abstract_term term) in
   let x := type of x in
@@ -70,7 +70,7 @@ Even stranger, consider:*)
 
 (*This works fine.  But if I change the period to a semicolon, I get:*)
 
-      Fail let term := constr:(I) in
+      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
@@ -82,7 +82,7 @@ Even stranger, consider:*)
  (* 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 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
@@ -92,3 +92,5 @@ Even stranger, consider:*)
       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.