diff options
| author | herbelin | 2000-12-21 20:58:56 +0000 |
|---|---|---|
| committer | herbelin | 2000-12-21 20:58:56 +0000 |
| commit | feebbe3d9d0c3046975f6f4f63758c6950949397 (patch) | |
| tree | 47c8ea51968a825d52b792f85dd32fd507ce5da2 | |
| parent | 6620fe95b23edc24356fac822e8f1cca7a8ee9a4 (diff) | |
Qualification des inductifs dans Print ind
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1181 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/pretty.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/pretty.ml b/parsing/pretty.ml index ba012d5202..ba2214ad62 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -118,7 +118,7 @@ let print_mutual sp mib = (body_of_type (mis_user_arity mis)) in (hOV 0 [< (hOV 0 - [< pr_id (mis_typename mis) ; 'bRK(1,2); params; + [< pr_global (IndRef (sp,tyi)) ; 'bRK(1,2); params; 'sTR ": "; prterm_env env_ar arity; 'sTR " :=" >]); 'bRK(1,2); print_constructors mis >]) in @@ -129,7 +129,7 @@ let print_mutual sp mib = let (_,arity) = decomp_n_prod env evd nparams (body_of_type (mis_user_arity mis0)) in let sfinite = if mis_finite mis0 then "Inductive " else "CoInductive " in - (hOV 0 [< 'sTR sfinite ; pr_id (mis_typename mis0); + (hOV 0 [< 'sTR sfinite ; pr_global (IndRef (sp,0)); if nparams = 0 then [<>] else |