From c74f11d65b693207cdfa6d02f697e76093021be7 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 14 Dec 2008 16:34:43 +0000
Subject: Generalized binding syntax overhaul: only two new binders: `() and
 `{}, guessing the binding name by default and making all generalized
 variables implicit. At the same time, continue refactoring of
 Record/Class/Inductive etc.., getting rid of [VernacRecord] definitively. The
 AST is not completely satisfying, but leaning towards Record/Class as
 restrictions of inductive (Arnaud, anyone ?). Now, [Class] declaration bodies
 are either of the form [meth : type] or [{ meth : type ; ... }],
 distinguishing singleton "definitional" classes and inductive classes based
 on records. The constructor syntax is accepted ([meth1 : type1 | meth1 :
 type2]) but raises an error immediately, as support for defining a class by a
 general inductive type is not there yet (this is a bugfix!).

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

(limited to 'ide')

diff --git a/ide/coq.ml b/ide/coq.ml
index 2f496d99d8..809c502e7e 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -230,7 +230,6 @@ let rec attribute_of_vernac_command = function
   (* Gallina extensions *)
   | VernacBeginSection _ -> []
   | VernacEndSegment _ -> []
-  | VernacRecord _ -> []
   | VernacRequire _ -> []
   | VernacImport _ -> []
   | VernacCanonical _ -> []
@@ -386,7 +385,7 @@ let compute_reset_info = function
 
   | VernacDefinition (_, (_,id), DefineBody _, _)
   | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_)
-  | VernacInductive (_, (((_,id),_,_,_),_) :: _) ->
+  | VernacInductive (_, (((_,(_,id)),_,_,_,_),_) :: _) ->
       ResetAtRegisteredObject (reset_mark id), undo_info(), ref true
 
   | com when is_vernac_proof_ending_command com -> NoReset, undo_info(), ref true
-- 
cgit v1.2.3