From bf3c9136e51674282fe91c9de917ba7264bcd007 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 13 Dec 2002 21:25:07 +0000
Subject: Compensation de suppression betaiota de type_of (suite)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3433 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/clenv.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index fee6ce40f4..40060165e0 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -999,10 +999,9 @@ let clenv_match_args s clause =
                   errorlabstrm "clenv_match_args" (str "No such binder")
 	in
 	let k_typ = w_hnf_constr clause.hook (clenv_instance_type clause k)
-	and c_typ = w_hnf_constr clause.hook (w_type_of clause.hook c) in
+	and c_typ = w_hnf_constr clause.hook (nf_betaiota (w_type_of clause.hook c)) in
 	(* whd_betaiota was before in type_of - useful to reduce types like *)
 	(* (x:A)([x]P u) *)
-	let c_typ = nf_betaiota c_typ in
         matchrec 
        	    (clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)) t
   in 
-- 
cgit v1.2.3