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 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'tactics')

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) =
-- 
cgit v1.2.3