diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-23 16:22:18 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-23 16:22:18 +0000 |
| commit | 0b840f7aaece0c209850adb2a81904b54f410091 (patch) | |
| tree | 442e51c4aeea80184f77667f7abbd5a8d04e54b5 /interp/topconstr.mli | |
| parent | 57cb1648fcf7da18d74c28a4d63d59ea129ab136 (diff) | |
Open notation for declaring record instances.
It solves feature request 1852, makes me and Arnaud happy and
will permit to factor some more code in typeclasses.
- Records are introduced using the syntax "{| x := t; y := foo |}" and
"with" clauses are currently parsed but not yet supported in the
elaboration. You are invited to suggest other syntaxes :)
- Missing fields are turned into holes, extra fields cause an error
message. The current implementation finds the type of the record
at pretyping time, from the typing constraint alone (and just expects
an inductive with one constructor). It is then impossible to use
scope information to parse the bodies: that may be wrong. The other
solution I see is using the fields to detect the type earlier, before
internalisation of the bodies, but then we get in name clash hell.
- In funind/contrib/interface I mostly put [assert false] everywhere to
avoid warnings.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11496 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/topconstr.mli')
| -rw-r--r-- | interp/topconstr.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 0064d238d..b6e2927bb 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -33,6 +33,7 @@ type aconstr = | ALambda of name * aconstr * aconstr | AProd of name * aconstr * aconstr | ALetIn of name * aconstr * aconstr + | ARecord of aconstr option * (identifier * aconstr) list | ACases of case_style * aconstr option * (aconstr * (name * (inductive * int * name list) option)) list * (cases_pattern list * aconstr) list @@ -133,6 +134,7 @@ type constr_expr = | CAppExpl of loc * (proj_flag * reference) * constr_expr list | CApp of loc * (proj_flag * constr_expr) * (constr_expr * explicitation located option) list + | CRecord of loc * constr_expr option * (identifier located * constr_expr) list | CCases of loc * case_style * constr_expr option * (constr_expr * (name option * constr_expr option)) list * (loc * cases_pattern_expr list located list * constr_expr) list |