diff options
Diffstat (limited to 'parsing/syntaxerr.ml')
| -rw-r--r-- | parsing/syntaxerr.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/parsing/syntaxerr.ml b/parsing/syntaxerr.ml index f18e3281d..bd5fafb25 100644 --- a/parsing/syntaxerr.ml +++ b/parsing/syntaxerr.ml @@ -10,8 +10,6 @@ (* *) (***********************************************************************) -(* $Id$ *) - (* Auxiliary type for reporting syntax errors *) open Format |