From cb84fd65bcc043e685ab83ae9dc7222a5b49263b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 11 Aug 2009 10:00:59 +0000
Subject: Infix (r12268 continued)

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

(limited to 'plugins')

diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index 9629fa923c..f60a9ee0bd 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -2104,7 +2104,7 @@ let rec xlate_vernac =
 	 CT_local_reserve_notation(translated_s, translated_modif_list)
        else
 	 CT_reserve_notation(translated_s, translated_modif_list)
-   | VernacInfix (b,(str,modl),id, opt_scope) ->
+   | VernacInfix (b,(str,modl),CRef id, opt_scope) ->
        let id1 = loc_qualid_to_ct_ID id in
        let modl1 = CT_modifier_list(List.map xlate_syntax_modifier modl) in
        let s = CT_string str in
@@ -2115,6 +2115,8 @@ let rec xlate_vernac =
 	   CT_local_infix(s, id1,modl1, translated_scope)
 	 else
 	   CT_infix(s, id1,modl1, translated_scope)
+   | VernacInfix (b,(str,modl),_ , opt_scope) -> 
+       xlate_error "TODO: Infix not ref"
    | VernacCoercion (s, id1, id2, id3) ->
       let id_opt = CT_coerce_NONE_to_IDENTITY_OPT CT_none in
       let local_opt =
-- 
cgit v1.2.3