From c5168ac18d40cf347da1a951d23f47777ae477e9 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 15 Jun 2009 01:37:39 +0000
Subject: Allow anonymous instances again, with syntax [Instance: T] where T
 may be a product.

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

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 56c00ca784..5b4e9ce04a 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -499,6 +499,13 @@ GEXTEND Gram
       | IDENT "Context"; c = binders_let -> 
 	  VernacContext c
 	    
+      | IDENT "Instance"; ":";
+	 expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
+	 pri = OPT [ "|"; i = natural -> i ] ; 
+	 props = [ ":="; "{"; r = record_declaration; "}" -> r | 
+	     ":="; c = lconstr -> c | -> CRecord (loc, None, []) ] ->
+	   VernacInstance (not (use_non_locality ()), [], ((loc,Anonymous), expl, t), props, pri)
+
       | IDENT "Instance"; name = identref; sup = OPT binders_let; ":";
 	 expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
 	 pri = OPT [ "|"; i = natural -> i ] ; 
-- 
cgit v1.2.3