From 594bf5a8d753c0c93ed5f7fb4874675966d4d042 Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 18 Dec 2001 14:02:08 +0000
Subject: affichage correct du type des inductifs et constructeurs en presence
 de parametres

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2312 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/prettyp.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 41a4a6b5a4..867bcd3168 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -107,9 +107,11 @@ let build_inductive sp tyi =
   let (mib,mip) = Global.lookup_inductive (sp,tyi) in
   let params = mip.mind_params_ctxt in
   let args = extended_rel_list 0 params in
-  let indf = make_ind_family ((sp,tyi),args) in
-  let arity = mip.mind_user_arity in
-  let cstrtypes = arities_of_constructors (Global.env()) (sp,tyi) in
+  let env = Global.env() in
+  let arity = hnf_prod_applist env mip.mind_user_arity args in
+  let cstrtypes = arities_of_constructors env (sp,tyi) in
+  let cstrtypes =
+    Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
   let cstrnames = mip.mind_consnames in
   (IndRef (sp,tyi), params, arity, cstrnames, cstrtypes)
 
-- 
cgit v1.2.3