diff options
| author | coq | 2002-08-16 10:00:36 +0000 |
|---|---|---|
| committer | coq | 2002-08-16 10:00:36 +0000 |
| commit | b1eef69751a05eebdbdc9d3091e1dae3386218d0 (patch) | |
| tree | e7c3c7b3657f1d15e6931e71f77d1da4114d2b2c /parsing | |
| parent | a1858ecd34bd7946dab7e7fbf2413036f78f7109 (diff) | |
Strengthenning rules for modules + No modules in sections
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2969 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/prettyp.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 6554659f38..159b082f0f 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -293,10 +293,16 @@ let print_constant with_values sep sp = let print_inductive sp = (print_mutual sp ++ fnl ()) let print_syntactic_def sep kn = - let _,_,l = repr_kn kn in + let l = label kn in let c = Syntax_def.search_syntactic_definition kn in (str" Syntactic Definition " ++ pr_lab l ++ str sep ++ pr_rawterm c ++ fnl ()) +let print_module with_values kn = + str "Module " ++ pr_id (id_of_label (label kn)) ++ fnl () ++ fnl () + +let print_modtype kn = + str "Module Type " ++ pr_id (id_of_label (label kn)) ++ fnl () ++ fnl () + let print_leaf_entry with_values sep ((sp,kn as oname),lobj) = let tag = object_tag lobj in match (oname,tag) with @@ -306,6 +312,10 @@ let print_leaf_entry with_values sep ((sp,kn as oname),lobj) = print_constant with_values sep kn | (_,"INDUCTIVE") -> print_inductive kn + | (_,"MODULE") -> + print_module with_values kn + | (_,"MODULE TYPE") -> + print_modtype kn | (_,"AUTOHINT") -> (* (str" Hint Marker" ++ fnl ())*) (mt ()) |