From 3f5ce5cbf138435fcf7e50bf978192c9fdd7db05 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 9 Nov 2008 16:17:14 +0000
Subject: More factorization of inductive/record and typeclasses: move class
 declaration code to toplevel/record, including support for singleton classes
 as definitions. Parsing code also factorized. Arnaud: one more thing to think
 about when refactoring the definitions in vernacentries. Add support for
 specifying what to do with anonymous variables in contexts during
 internalisation (fixes bug #1982), current choice is to generate a name for
 typeclass bindings.

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

(limited to 'ide')

diff --git a/ide/coq.ml b/ide/coq.ml
index 2d8c2ff99a..2f496d99d8 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -238,7 +238,6 @@ let rec attribute_of_vernac_command = function
   | VernacIdentityCoercion _ -> []
 
   (* Type classes *)
-  | VernacClass _ -> []
   | VernacInstance _ -> []
   | VernacContext _ -> []
   | VernacDeclareInstance _ -> []
-- 
cgit v1.2.3