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

(in case of side effects)

Also:
Fix #4781
Fix #4496

1 files changed, 0 insertions, 94 deletions

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 *)