From b63cd131e8b4a5600973c860d2ccc6e3e5c8ce91 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 4 Jan 2010 17:50:38 +0000
Subject: Specific syntax for Instances in Module Type: Declare Instance

NB: the grammar entry is placed in vernac:command on purpose
 even if it should have gone into vernac:gallina_ext. Camlp4
 isn't factorising rules starting by "Declare" in a correct way
 otherwise...

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

(limited to 'plugins')

diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index b337d33520..0eba0f6336 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -169,8 +169,10 @@ let subtac (loc, command) =
   | VernacAssumption (stre,nl,l) ->
       vernac_assumption env isevars stre l nl
 
-  | VernacInstance (glob, sup, is, props, pri) ->
+  | VernacInstance (abst, glob, sup, is, props, pri) ->
       dump_constraint "inst" is;
+      if abst then
+	error "Declare Instance not supported here.";
       ignore(Subtac_classes.new_instance ~global:glob sup is props pri)
 
   | VernacCoFixpoint (l, b) ->
-- 
cgit v1.2.3