From e96be1390162ae3805e50b3d8305667c5f5c6a25 Mon Sep 17 00:00:00 2001
From: filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 11 Feb 2003 14:24:20 +0000
Subject: Undo dans Coq IDE

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3673 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernac.ml  | 6 ++++--
 toplevel/vernac.mli | 6 ++++++
 2 files changed, 10 insertions(+), 2 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a0b4271f6..5ccb9ad59 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -103,8 +103,7 @@ let pr_comments = function
   | None -> mt()
   | Some l -> h 0 (List.fold_left (++) (mt ()) (List.rev l))
 
-let rec vernac interpfun input =
-  let (loc,com) = parse_phrase input in
+let rec vernac_com interpfun (loc,com) =
   let rec interp = function
     | VernacLoad (verbosely, fname) ->
         read_vernac_file verbosely (make_suffix fname ".v")
@@ -138,6 +137,9 @@ let rec vernac interpfun input =
   with e -> 
     raise (DuringCommandInterp (loc, e))
 
+and vernac interpfun input =
+  vernac_com interpfun (parse_phrase input)
+
 and read_vernac_file verbosely s =
   let interpfun =
     if verbosely then 
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 5d53dab2a..ca96d9e49 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -39,3 +39,9 @@ val load_vernac : bool -> string -> unit
 (* Compile a vernac file, verbosely or not (f is assumed without .v suffix) *)
 
 val compile : bool -> string -> unit
+
+(* Interpret a vernac AST *)
+
+val vernac_com : 
+  (Vernacexpr.vernac_expr -> unit) ->
+  Util.loc * Vernacexpr.vernac_expr -> unit
-- 
cgit v1.2.3