diff options
| author | herbelin | 2000-11-27 18:36:26 +0000 |
|---|---|---|
| committer | herbelin | 2000-11-27 18:36:26 +0000 |
| commit | c5c5381f410f0ca7505dd113884b210888310b8e (patch) | |
| tree | ea564d9c3d1cd9886ece6b18a79449cdcc55e6c9 | |
| parent | 4e990ab6bf33b5667930f7bcae970d5c3b29ef94 (diff) | |
Bug affichage inductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@996 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/pretty.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/parsing/pretty.ml b/parsing/pretty.ml index 152e2a50ac..22c735e474 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -81,9 +81,6 @@ let implicit_args_msg sp mipv = >]) mipv >] -let instance_of_named_context sign = - Array.of_list (List.map mkVar (ids_of_named_context sign)) - let print_mutual sp mib = let pk = kind_of_path sp in let env = Global.env () in @@ -113,7 +110,8 @@ let print_mutual sp mib = else [< 'sTR "["; pr_rel_context env lpars; 'sTR "]"; 'bRK(1,2) >] in let print_oneind tyi = - let mis = build_mis ((sp,tyi),instance_of_named_context mib.mind_hyps) mib in + let mis = + build_mis ((sp,tyi),Array.of_list (instance_from_named_context mib.mind_hyps)) mib in let (_,arity) = decomp_n_prod env evd nparams (body_of_type (mis_user_arity mis)) in (hOV 0 @@ -122,7 +120,8 @@ let print_mutual sp mib = 'sTR ": "; prterm_env env_ar arity; 'sTR " :=" >]); 'bRK(1,2); print_constructors mis >]) in - let mis0 = build_mis ((sp,0),instance_of_named_context mib.mind_hyps) mib in + let mis0 = + build_mis ((sp,0),Array.of_list (instance_from_named_context mib.mind_hyps)) mib in (* Case one [co]inductive *) if Array.length mipv = 1 then let (_,arity) = decomp_n_prod env evd nparams |