diff options
| author | herbelin | 2003-04-09 10:35:30 +0000 |
|---|---|---|
| committer | herbelin | 2003-04-09 10:35:30 +0000 |
| commit | d434ab34709e0ce40f049d709332800d9a96bcc5 (patch) | |
| tree | adc6e5ac006c3de8d9dbda1ad06905da31a5efdb /parsing | |
| parent | fa2571f711bf6ba6b99a04bf2cc10b68b37682f9 (diff) | |
Réorganisation de Impargs + mise en place d'une infrastructure
(notatemment des tables de parsing et d'affichage différenciées)
permettant au traducteur de changer les implicites
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3874 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/prettyp.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 648d4690de..7aa4359849 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -83,11 +83,11 @@ let implicit_args_id id l = let implicit_args_msg sp mipv = (prvecti (fun i mip -> - let imps = inductive_implicits_list (sp,i) in + let imps = implicits_of_global (IndRef (sp,i)) in ((implicit_args_id mip.mind_typename imps) ++ prvecti (fun j idc -> - let imps = constructor_implicits_list ((sp,i),succ j) in + let imps = implicits_of_global (ConstructRef ((sp,i),j+1)) in (implicit_args_id idc imps)) mip.mind_consnames )) @@ -153,7 +153,7 @@ let print_mutual sp = let print_section_variable sp = let d = get_variable sp in - let l = implicits_of_var sp in + let l = implicits_of_global (VarRef sp) in (print_named_decl d ++ print_impl_args l) let print_body = function @@ -167,7 +167,7 @@ let print_constant with_values sep sp = let cb = Global.lookup_constant sp in let val_0 = cb.const_body in let typ = cb.const_type in - let impls = constant_implicits_list sp in + let impls = implicits_of_global (ConstRef sp) in hov 0 ((match val_0 with | None -> (str"*** [ " ++ |