From a008023cae4fdddffbbbfd8a455d7776200a9cfb Mon Sep 17 00:00:00 2001
From: corbinea
Date: Thu, 6 Nov 2003 14:35:25 +0000
Subject: Added Instantiate ... in

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

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 58eaf292a6..47370ef135 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1010,8 +1010,11 @@ and xlate_tac =
 	  (xlate_int_or_constr a, xlate_using b, 
 	   CT_id_list_list
 	     (List.map (fun l -> CT_id_list(List.map xlate_newind_names l)) c))
-    | TacInstantiate (a, b) -> 
+    | TacInstantiate (a, b, None) -> 
 	CT_instantiate(CT_int a, xlate_formula b)
+    | TacInstantiate (a, b, _) -> 
+	xlate_error "TODO: Instantiate ... in"
+
     | TacLetTac (id, c, cl) ->
         CT_lettac(xlate_ident id, xlate_formula c, 
 		  (* TODO LATER: This should be shared with Unfold,
-- 
cgit v1.2.3