diff options
| author | filliatr | 2001-04-04 14:13:24 +0000 |
|---|---|---|
| committer | filliatr | 2001-04-04 14:13:24 +0000 |
| commit | 0df14c3d0d2c71716bbed04451ad2e2541dcc6a3 (patch) | |
| tree | ec4918a0ef86b133860847f1b61e858b0920d6a1 /contrib/interface/parse.ml | |
| parent | 2def0e4f8e5d075d815df253d316a96dd7257423 (diff) | |
renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocamldep
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1547 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface/parse.ml')
| -rw-r--r-- | contrib/interface/parse.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml index f1f04a2df5..7648e79227 100644 --- a/contrib/interface/parse.ml +++ b/contrib/interface/parse.ml @@ -190,7 +190,7 @@ let parse_string_action reqid phylum char_stream string_list = P_c (xlate_vernac (execute_when_necessary - (Gram.Entry.parse Pcoq.Vernac.vernac_eoi (Gram.parsable char_stream)))) + (Gram.Entry.parse Pcoq.Vernac_.vernac_eoi (Gram.parsable char_stream)))) | "TACTIC_COM" -> P_t (xlate_tactic (Gram.Entry.parse Pcoq.Tactic.tactic_eoi @@ -223,9 +223,10 @@ 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; ();; |