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 /contrib/subtac | |
| 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 'contrib/subtac')
| -rw-r--r-- | contrib/subtac/subtac_classes.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml index a240744bfc..510229ae6f 100644 --- a/contrib/subtac/subtac_classes.ml +++ b/contrib/subtac/subtac_classes.ml @@ -137,7 +137,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p let sigma = Evd.evars_of !isevars in let subst = List.map (Evarutil.nf_evar sigma) subst in let subst = - let props = match props with CRecord (loc, _, fs) -> fs | _ -> assert false in + let props = match props with CRecord (loc, _, fs) -> fs + | _ -> errorlabstrm "new_instance" (Pp.str "Expected a record declaration for the instance body") + in if List.length props > List.length k.cl_props then Classes.mismatched_props env' (List.map snd props) k.cl_props; match k.cl_props with |