From b9d7d302a186e2bb6766708a9802f058724ea0fb Mon Sep 17 00:00:00 2001
From: bertot
Date: Wed, 18 Apr 2001 07:03:26 +0000
Subject: Adding files for the production of textual explanations as used in
 pcoq.

dependence files are updated accordingly.

Modifications in other files to cope with a few errors in the translation for
the parser (mostly around records, coercions, and the search-pattern command).


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

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

diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 7648e79227..bdda47e38f 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -223,10 +223,9 @@ let parse_string_action reqid phylum char_stream string_list =
 
 
 let quiet_parse_string_action char_stream =
- try 
-   let _ = 
-     Gram.Entry.parse Pcoq.Vernac_.vernac_eoi (Gram.parsable char_stream) in
-   ()
+ try let _ = 
+         Gram.Entry.parse Pcoq.Vernac_.vernac_eoi (Gram.parsable char_stream) in
+     ()
  with
  | _ -> flush_until_end_of_stream char_stream; ();;
 
-- 
cgit v1.2.3