From 141dcba78c1c8cc1ef158554a391efa1032d4b5f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 11 Dec 2002 10:46:16 +0000
Subject: Compensation de suppression betaiota de type_of

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

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 66e3181a3c..ebb4ab684f 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -1000,6 +1000,9 @@ let clenv_match_args s clause =
 	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
+	(* whd_betaiota was before in type_of - useful to reduce types like *)
+	(* (x:A)([x]P u) *)
+	let c_typ = whd_betaiota c_typ in
         matchrec 
        	    (clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)) t
   in 
-- 
cgit v1.2.3