From 208eceab14148fa561c36f71e2e1485e73832616 Mon Sep 17 00:00:00 2001
From: gmelquio
Date: Wed, 4 Nov 2009 18:47:36 +0000
Subject: Fixed record syntax "{|x=...; y=...|}" so that it works with
 qualified names. Fixed pretty printing of record syntax. Allowed record
 syntax inside patterns. (Patch by Cedric Auger.)

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

(limited to 'plugins/interface')

diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index 261bb0029c..435130ae6f 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -273,6 +273,7 @@ let rec xlate_match_pattern =
      CT_pattern_as
       (xlate_match_pattern pattern, CT_coerce_ID_to_ID_OPT (xlate_ident id))
     | CPatOr (_,l) -> xlate_error "CPatOr: TODO"
+    | CPatRecord _ -> xlate_error "CPAtRecord: TODO"
     | CPatDelimiters(_, key, p) ->
 	CT_pattern_delimitors(CT_num_type key, xlate_match_pattern p)
     | CPatPrim (_,Numeral n) ->
-- 
cgit v1.2.3