diff options
Diffstat (limited to 'parsing/pretty.ml')
| -rw-r--r-- | parsing/pretty.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/parsing/pretty.ml b/parsing/pretty.ml index eb6b207192..2577ef9be2 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -329,7 +329,6 @@ let print_name qid = | IndRef (sp,_) -> print_inductive sp | ConstructRef ((sp,_),_) -> print_inductive sp | VarRef sp -> print_section_variable sp - | EvarRef n -> [< 'sTR "?"; 'iNT n; 'fNL >] with Not_found -> try (* Var locale de but, pas var de section... donc pas d'implicits *) let dir,str = repr_qualid qid in |