diff options
| author | herbelin | 2001-09-24 12:51:11 +0000 |
|---|---|---|
| committer | herbelin | 2001-09-24 12:51:11 +0000 |
| commit | ee8e52f14194d3888dc6359ceb78abbcc98b0e7c (patch) | |
| tree | 6d4ea546795c47fb843840f81e84f32533b3a679 | |
| parent | cdc6f7c31c7dc8abc3f5fef03e5aa86c50f94643 (diff) | |
Marre des unrecognized objects
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2055 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/prettyp.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 7a8571fdcf..ab91537054 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -339,9 +339,13 @@ let print_leaf_entry with_values sep (sp,lobj) = [< >] | (_,"END-SECTION") -> [< >] | (_,"STRUCTURE") -> [< >] +(* To deal with forgotten cases... *) + | (_,s) -> [< >] +(* | (_,s) -> [< 'sTR(string_of_path sp); 'sTR" : "; 'sTR"Unrecognized object "; 'sTR s; 'fNL >] +*) let rec print_library_entry with_values ent = let sep = if with_values then " = " else " : " in |