From e79a1fdb9f7cd778aae3274b65b6b015bfc70277 Mon Sep 17 00:00:00 2001
From: bertot
Date: Fri, 24 Jan 2003 09:49:47 +0000
Subject: The data constructed when detecting an error in a list of commands
 must imperatively be called PARSING_ERROR and not PARSE_ERROR

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3608 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/parse.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'contrib/interface/parse.ml')

diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 854c76db49..b6a0ef659e 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -217,7 +217,7 @@ let parse_command_list reqid stream string_list =
                         (get_substring_list string_list this_pos
                             (Stream.count stream))))
 *)
-		ParseError ("PARSE_ERROR",
+		ParseError ("PARSING_ERROR",
                   get_substring_list string_list this_pos
 		    (Stream.count stream))
              with End_of_file -> ParseOK None
@@ -231,7 +231,7 @@ let parse_command_list reqid stream string_list =
 		   (get_substring_list string_list this_pos
                      (Stream.count stream))))
 *)
-	    ParseError ("PARSE_ERROR2",
+	    ParseError ("PARSING_ERROR2",
 	      get_substring_list string_list this_pos (Stream.count stream))
           end in
     match first_ast with
-- 
cgit v1.2.3