diff options
| -rw-r--r-- | parsing/prettyp.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 1bd1109266..8d99ac1121 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -355,7 +355,9 @@ let print_leaf_entry with_values sep ((sp,kn as oname),lobj) = let tag = object_tag lobj in match (oname,tag) with | (_,"VARIABLE") -> - Some (print_section_variable (basename sp)) + (* Outside sections, VARIABLES still exist but only with universes + constraints *) + (try Some(print_section_variable (basename sp)) with Not_found -> None) | (_,"CONSTANT") -> Some (print_constant with_values sep (constant_of_kn kn)) | (_,"INDUCTIVE") -> |