diff options
| author | herbelin | 2006-01-28 22:03:33 +0000 |
|---|---|---|
| committer | herbelin | 2006-01-28 22:03:33 +0000 |
| commit | 383320a6a86d1023aa7304f697148375e076b114 (patch) | |
| tree | 28f0c43614b25328ef2c65c8d08ddb1acee0d7bb | |
| parent | 368ac3d3cf4d512e5d4ac7243a92e5d150c7670f (diff) | |
Correction bug Inspect introduit par le passage du discharge à une méthode associée aux objects
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7938 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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") -> |