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
---
 contrib/correctness/pextract.ml | 3 ++-
 contrib/correctness/pmlize.ml   | 2 +-
 proofs/clenv.ml                 | 3 +++
 3 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/contrib/correctness/pextract.ml b/contrib/correctness/pextract.ml
index cd5badbed6..3e42ba6367 100644
--- a/contrib/correctness/pextract.ml
+++ b/contrib/correctness/pextract.ml
@@ -439,7 +439,8 @@ let pp_ocaml file prm =
 let initialize id com =
   let loc = Ast.loc com in
   let c = constr_of_com (Evd.mt_evd()) (initial_sign()) com in
-  let ty = type_of (Evd.mt_evd()) (initial_sign()) c in
+  let ty = 
+    Reductionops.nf_betaiota (type_of (Evd.mt_evd()) (initial_sign()) c) in
   try
     let v = lookup_global id in
     let ety = match v with 
diff --git a/contrib/correctness/pmlize.ml b/contrib/correctness/pmlize.ml
index aa81310030..ed2896ec90 100644
--- a/contrib/correctness/pmlize.ml
+++ b/contrib/correctness/pmlize.ml
@@ -29,7 +29,7 @@ open Pmonad
 let has_proof_part ren env c =
   let sign = Pcicenv.trad_sign_of ren env in
   let ty = Typing.type_of (Global.env_of_context sign) Evd.empty c in
-  is_matching (Coqlib.build_coq_sig_pattern ()) ty
+  is_matching (Coqlib.build_coq_sig_pattern ()) (Reductionops.nf_betaiota ty)
 
 (* main part: translation of imperative programs into functional ones.
  * 
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