Univs: fix bug #4031: wrong folding of sigma in change.

1 files changed, 14 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4031.v b/test-suite/bugs/closed/4031.v
new file mode 100644
index 0000000000..2b8641ebb0
--- /dev/null
+++ b/test-suite/bugs/closed/4031.v
@@ -0,0 +1,14 @@
+Definition something (P:Type) (e:P) := e.
+
+Inductive myunit : Set := mytt.
+  (* Proof below works when definition is in Type,
+     however builtin types such as unit are in Set. *)
+
+Lemma demo_hide_generic : 
+   let x := mytt in x = x.
+Proof.
+  intros.
+  change mytt with (@something _ mytt) in x.
+  subst x. (* Proof works if this line is removed *)
+  reflexivity.
+Qed.
\ No newline at end of file