diff options
| author | msozeau | 2008-12-14 16:34:43 +0000 |
|---|---|---|
| committer | msozeau | 2008-12-14 16:34:43 +0000 |
| commit | c74f11d65b693207cdfa6d02f697e76093021be7 (patch) | |
| tree | b32866140d9f5ecde0bb719c234c6603d44037a8 /ide | |
| parent | 2f63108dccc104fe32344d88b35193d34a88f743 (diff) | |
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
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 3 |
1 files changed, 1 insertions, 2 deletions
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 |