From 561a67ca1144b72a9e27e9ec1867b631665a6015 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 13 Jun 2003 14:08:46 +0000
Subject: Utilisation de intro_pattern dans NewDestruct/NewInduction

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

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 14caa9f98e..54f22c6460 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -512,6 +512,11 @@ let rec xlate_intro_pattern =
   | IntroWildcard -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" )
   | IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c)
 
+let xlate_newind_names = 
+  function
+    | IntroIdentifier id -> xlate_ident id
+    | _ -> xlate_error "TODO: intro_patterns for NewDestruct/NewInduction"
+
 let compute_INV_TYPE_from_string = function
    "InversionClear" -> CT_inv_clear
  | "SimpleInversion" -> CT_inv_simple
@@ -1005,12 +1010,12 @@ and xlate_tac =
 	CT_new_destruct
 	  (xlate_int_or_constr a, xlate_using b, 
 	   CT_id_list_list
-	     (List.map (fun l -> CT_id_list(List.map xlate_ident l)) c))
+	     (List.map (fun l -> CT_id_list(List.map xlate_newind_names l)) c))
     | TacNewInduction(a,b,c) ->
 	CT_new_induction
 	  (xlate_int_or_constr a, xlate_using b, 
 	   CT_id_list_list
-	     (List.map (fun l -> CT_id_list(List.map xlate_ident l)) c))
+	     (List.map (fun l -> CT_id_list(List.map xlate_newind_names l)) c))
     | TacInstantiate (a, b) -> 
 	CT_instantiate(CT_int a, xlate_formula b)
     | TacLetTac (id, c, cl) ->
-- 
cgit v1.2.3