From 895fcffc774abada4677d52a7dbbb54a85cadec7 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 18 Jan 2009 17:36:51 +0000
Subject: Last changes in type class syntax: - curly braces mandatory for
 record class instances - no mention of the unique method for definitional
 class instances Turning a record or definition into a class is mostly a
 matter of changing the keywords to 'Class' and 'Instance' now. Documentation
 reflects these changes, and was checked once more along with setoid_rewrite's
 and Program's.

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

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3a88a09f81..2b99fee979 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -505,7 +505,8 @@ GEXTEND Gram
       | IDENT "Instance"; name = identref; sup = OPT binders_let; ":";
 	 expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
 	 pri = OPT [ "|"; i = natural -> i ] ; 
-	 props = [ ":="; decl = record_declaration -> decl | -> CRecord (loc, None, []) ] ->
+	 props = [ ":="; "{"; r = record_declaration; "}" -> r | 
+	     ":="; c = lconstr -> c | -> CRecord (loc, None, []) ] ->
 	   let sup =
 	     match sup with
 		 None -> []
@@ -695,7 +696,6 @@ GEXTEND Gram
       | IDENT "Hint"; "*" -> PrintHintDb
       | IDENT "HintDb"; s = IDENT -> PrintHintDbName s
       | "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s
-      | IDENT "Setoids" -> PrintSetoids
       | IDENT "Scopes" -> PrintScopes
       | IDENT "Scope"; s = IDENT -> PrintScope s
       | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
-- 
cgit v1.2.3