Merge PR #13854: Normalize evars during bytecode compilation.

Reviewed-by: SkySkimmer
Ack-by: ppedrot
Ack-by: ejgallego

2 files changed, 17 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_13841.v b/test-suite/bugs/closed/bug_13841.v
new file mode 100644
index 0000000000..60fca8b49c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13841.v
@@ -0,0 +1,11 @@
+Goal True.
+evar (p : bool).
+unify ?p true.
+let v := eval vm_compute in (orb p false) in
+match v with true => idtac end.
+assert (orb p false = true).
+vm_compute.
+match goal with |- true = _ => idtac end.
+easy.
+easy.
+Qed.
diff --git a/test-suite/bugs/closed/bug_7631.v b/test-suite/bugs/closed/bug_7631.v
index 93aeb83e28..14ab4de9b7 100644
--- a/test-suite/bugs/closed/bug_7631.v
+++ b/test-suite/bugs/closed/bug_7631.v
@@ -21,3 +21,9 @@ Definition bar (x := foo) := Eval native_compute in x.
 Definition barvm (x := foo) := Eval vm_compute in x.
 
 End RelContext.
+
+Definition bar (t:=_) (x := true : t) := Eval native_compute in x.
+Definition barvm (t:=_) (x := true : t) := Eval vm_compute in x.
+
+Definition baz (z:nat) (t:=_ z) (x := true : t) := Eval native_compute in x.
+Definition bazvm (z:nat) (t:=_ z) (x := true : t) := Eval vm_compute in x.