From 3d519597dc4a8f86995297c5b013f1b4f87c73e2 Mon Sep 17 00:00:00 2001
From: msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 1 Feb 2007 12:00:51 +0000
Subject: Abbreviation of order notation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9576 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_constr.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'parsing/g_constr.ml4')

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 9a50eb897..b29b82607 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -231,8 +231,8 @@ GEXTEND Gram
   ;
   fixannot:
     [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec)
-      | "{"; IDENT "wf"; rel=constr; id=name; "}" -> (Some id, CWfRec rel)
-      | "{"; IDENT "measure"; rel=constr; id=name; "}" -> (Some id, CMeasureRec rel)
+      | "{"; IDENT "wf"; rel=constr; id=OPT name; "}" -> (id, CWfRec rel)
+      | "{"; IDENT "measure"; rel=constr; id=OPT name; "}" -> (id, CMeasureRec rel)
       | ->  (None, CStructRec)
       ] ]
   ;
-- 
cgit v1.2.3