diff options
| author | barras | 2001-12-18 14:02:08 +0000 |
|---|---|---|
| committer | barras | 2001-12-18 14:02:08 +0000 |
| commit | 594bf5a8d753c0c93ed5f7fb4874675966d4d042 (patch) | |
| tree | 2c1072f53e587edae59f1fd05ae0dd2ed95bbf7c | |
| parent | 1a61af5ad0da102f6912ce3c7a18fe4770f23be4 (diff) | |
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
| -rw-r--r-- | parsing/prettyp.ml | 8 |
1 files 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) |