From 00608fac2d8e217232d5f2ddd28a43971bf259b7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 31 Mar 2003 21:18:53 +0000
Subject: Ajout d'un message à FailTac

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

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 3941d10c6f..8191a0978f 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -758,7 +758,8 @@ and xlate_tactic =
 		   (xlate_local_rec_tac f1, List.map xlate_local_rec_tac l) in
        CT_rec_tactic_in(tl, xlate_tactic t)
    | TacAtom (_, t) -> xlate_tac t 
-   | TacFail n -> CT_fail (CT_int n)
+   | TacFail (n,"") -> CT_fail (CT_int n)
+   | TacFail (n,s) -> xlate_error "TODO: Fail n message"
    | TacId -> CT_idtac
    | TacInfo t -> CT_info(xlate_tactic t)
    | TacArg a -> xlate_call_or_tacarg a
@@ -1656,6 +1657,7 @@ let xlate_vernac =
 	 match opt_positions with
 	     None -> CT_int_list[]
 	   | Some l -> CT_int_list(List.map (fun x -> CT_int x) l))
+  | VernacReserve _ -> xlate_error "TODO: Default Variable Type"
   | VernacLocate(LocateTerm id) -> CT_locate(reference_to_ct_ID id)
   | VernacLocate(LocateLibrary id) -> CT_locate_lib(reference_to_ct_ID id)
   | VernacLocate(LocateFile s) -> CT_locate_file(CT_string s)
-- 
cgit v1.2.3