From 1e69c6a499757b05180205e84ed2bf6f1cbf7b2f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 3 Jul 2006 16:40:20 +0000
Subject: Extension des motifs disjonctifs au cas de disjonction de motifs
 multiples

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

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index e8fd52dba8..2a11f55c9c 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -336,8 +336,8 @@ and
   | a::l -> CT_match_pattern_ne_list(xlate_match_pattern a, 
                                      List.map xlate_match_pattern l)
 and  translate_one_equation = function
-    (_,lp, a) -> CT_eqn ( xlate_match_pattern_ne_list lp,
-	     xlate_formula a)
+    (_,[lp], a) -> CT_eqn (xlate_match_pattern_ne_list lp, xlate_formula a)
+  | _ -> xlate_error "TODO: disjunctive multiple patterns"
 and 
   xlate_binder_ne_list = function
     [] -> assert false
-- 
cgit v1.2.3