From 8c5bfa0f00b80979473bba26c1b9a1410667e032 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 12 Feb 2015 22:49:35 +0100
Subject: Univs: fix bug #4031: wrong folding of sigma in change.

---
 tactics/tactics.ml            |  8 ++++++--
 test-suite/bugs/closed/4031.v | 14 ++++++++++++++
 2 files changed, 20 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/bugs/closed/4031.v

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a298bba978..04df3b8cda 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -569,8 +569,12 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env
     let sigma',ty' = redfun false env sigma ty in
       sigma', (id,None,ty')
   | Some b ->
-      let sigma',b' = if where != InHypTypeOnly then redfun true env sigma b else sigma, b in
-      let sigma',ty' = if where != InHypValueOnly then redfun false env sigma ty else sigma', ty in
+      let sigma',b' = 
+	if where != InHypTypeOnly then redfun true env sigma b else sigma, b 
+      in
+      let sigma',ty' = 
+	if where != InHypValueOnly then redfun false env sigma' ty else sigma', ty 
+      in
 	sigma', (id,Some b',ty')
 
 let e_change_in_hyp redfun (id,where) =
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
-- 
cgit v1.2.3