From e03d1840a8e6eec927e7fbe006d59ab21b8d818f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 22 Oct 2008 11:21:45 +0000
Subject: Affichage des notations récursives: - Prise en compte des notations
 applicatives - Remplacement du codage des arguments liste des notations
 récursives   sous forme de terme par une représentation directe (permet
 notamment   de résoudre un problème de stack overflow de la fonction
 d'affichage) + Correction bug affichage Lemma dans ppvernac.ml + Divers
 util.ml

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

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 77cde062ff..561ed3d4c8 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -274,9 +274,11 @@ let rec xlate_match_pattern =
  	CT_coerce_NUM_to_MATCH_PATTERN
 	  (CT_int_encapsulator(Bigint.to_string n))
     | CPatPrim (_,String _) -> xlate_error "CPatPrim (String): TODO"
-    | CPatNotation(_, s, l) -> 
+    | CPatNotation(_, s, (l,[])) -> 
 	CT_pattern_notation(CT_string s,
 			    CT_match_pattern_list(List.map xlate_match_pattern l))
+    | CPatNotation(_, s, (l,_)) ->
+	 xlate_error "CPatNotation (recursive notation): TODO"
 ;;
 
 
@@ -392,7 +394,8 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 	  xlate_formula b1, xlate_formula b2)
 
    | CSort(_, s) -> CT_coerce_SORT_TYPE_to_FORMULA(xlate_sort s)
-   | CNotation(_, s, l) -> notation_to_formula s (List.map xlate_formula l)
+   | CNotation(_, s,(l,[])) -> notation_to_formula s (List.map xlate_formula l)
+   | CNotation(_, s,(l,_)) -> xlate_error "CNotation (recursive): TODO"
    | CPrim (_, Numeral i) -> 
        CT_coerce_NUM_to_FORMULA(CT_int_encapsulator(Bigint.to_string i))
    | CPrim (_, String _) -> xlate_error "CPrim (String): TODO"
-- 
cgit v1.2.3