From 110db6ddf023c98a76c719caf602559942ba089e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 29 Jun 2008 16:27:16 +0000
Subject: Correction bug "parser" suite changement syntaxe
 discriminate/injection/simplify_eq.

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

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 07cc101889..8b805cc26b 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -928,23 +928,26 @@ and xlate_tac =
     | TacExtend (_,"contradiction",[]) -> CT_contradiction
     | TacDoubleInduction (n1, n2) ->
 	CT_tac_double (xlate_quantified_hypothesis n1, xlate_quantified_hypothesis n2)
-    | TacExtend (_,"discriminate", [idopt]) ->
+    | TacExtend (_,"discriminate", []) ->
+     CT_discriminate_eq (CT_coerce_ID_OPT_to_ID_OR_INT_OPT ctv_ID_OPT_NONE)
+    | TacExtend (_,"discriminate", [id]) ->
      CT_discriminate_eq
          (xlate_quantified_hypothesis_opt
-	    (out_gen (wit_opt rawwit_quant_hyp) idopt))
-    | TacExtend (_,"simplify_eq", [idopt]) ->
-	let idopt1 = out_gen (wit_opt rawwit_quant_hyp) idopt in
-	let idopt2 = match idopt1 with
-	    None -> CT_coerce_ID_OPT_to_ID_OR_INT_OPT
-		(CT_coerce_NONE_to_ID_OPT CT_none)
-	  | Some v ->
-	      CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT
-	      	(xlate_quantified_hypothesis v) in
-	  CT_simplify_eq idopt2
-    | TacExtend (_,"injection", [idopt]) ->
+	    (Some (out_gen rawwit_quant_hyp id)))
+    | TacExtend (_,"simplify_eq", []) ->
+	  CT_simplify_eq (CT_coerce_ID_OPT_to_ID_OR_INT_OPT
+		(CT_coerce_NONE_to_ID_OPT CT_none))
+    | TacExtend (_,"simplify_eq", [id]) ->
+	let id1 = out_gen rawwit_quant_hyp id in
+	let id2 = CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT
+	      	(xlate_quantified_hypothesis id1) in
+	  CT_simplify_eq id2
+    | TacExtend (_,"injection", []) ->
+     CT_injection_eq (CT_coerce_ID_OPT_to_ID_OR_INT_OPT ctv_ID_OPT_NONE)
+    | TacExtend (_,"injection", [id]) ->
      CT_injection_eq
          (xlate_quantified_hypothesis_opt
-	    (out_gen (wit_opt rawwit_quant_hyp) idopt))
+	    (Some (out_gen rawwit_quant_hyp id)))
     | TacExtend (_,"injection_as", [idopt;ipat]) ->
 	xlate_error "TODO: injection as"
     | TacFix (idopt, n) ->
-- 
cgit v1.2.3