diff options
Diffstat (limited to 'parsing/prettyp.ml')
-rw-r--r-- | parsing/prettyp.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 98c93f897..882a94ffb 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -10,8 +10,6 @@ * on May-June 2006 for implementation of abstraction of pretty-printing of objects. *) -(* $Id$ *) - open Pp open Util open Names |