From bac2937c74053b526dd0b848b490ef5fac05a1ca Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 25 Apr 2012 15:12:47 +0000
Subject: Do not delta-head-normalize the proposition argument of sigma types
 during coercion.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15245 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/coercion.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 560b615467..d74584d896 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -104,11 +104,11 @@ let lift_args n sign =
 
 let rec mu env isevars t =
   let rec aux v =
-    let v = hnf env !isevars v in
-      match disc_subset v with
+    let v' = hnf env !isevars v in
+      match disc_subset v' with
       Some (u, p) ->
 	let f, ct = aux u in
-	let p = hnf env !isevars p in
+	let p = hnf_nodelta env !isevars p in
 	  (Some (fun x ->
 		   app_opt env isevars 
 		     f (mkApp (delayed_force sig_proj1,
-- 
cgit v1.2.3