diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-27 17:29:10 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-01-27 17:29:10 +0000 |
| commit | 546150e4873c9e004d832d0ab4e92ad952aeb11f (patch) | |
| tree | 7791518ee3d6f2513153a36725f6ebef4a3ec779 /parsing | |
| parent | 9a6180a0fb03bc452414f0327ce375733c223f5d (diff) | |
Simplification Impargs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1284 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pretty.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/parsing/pretty.ml b/parsing/pretty.ml index 007a2e4ab..d7d092685 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -71,12 +71,12 @@ let implicit_args_id id l = let implicit_args_msg sp mipv = [< prvecti (fun i mip -> - let imps = inductive_implicits (sp,i) in - [< (implicit_args_id mip.mind_typename (list_of_implicits imps)); + let imps = inductive_implicits_list (sp,i) in + [< (implicit_args_id mip.mind_typename imps); prvecti (fun j idc -> - let imps = constructor_implicits ((sp,i),succ j) in - (implicit_args_id idc (list_of_implicits imps))) + let imps = constructor_implicits_list ((sp,i),succ j) in + (implicit_args_id idc imps)) mip.mind_consnames >]) mipv >] @@ -183,7 +183,7 @@ let print_constant with_values sep sp = if kind_of_path sp = CCI then let val_0 = cb.const_body in let typ = cb.const_type in - let l = constant_implicits sp in + let impls = constant_implicits_list sp in hOV 0 [< (match val_0 with | None -> [< 'sTR"*** [ "; @@ -196,7 +196,7 @@ let print_constant with_values sep sp = print_typed_body (val_0,typ) else [< prtype typ ; 'fNL >] >]); - print_impl_args (list_of_implicits l); 'fNL >] + print_impl_args impls; 'fNL >] else hOV 0 [< 'sTR"Fw constant " ; print_basename sp ; 'fNL>] |