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 /toplevel/classes.ml | |
| 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 'toplevel/classes.ml')
| -rw-r--r-- | toplevel/classes.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 4e8710918..4eca304c2 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -257,7 +257,9 @@ let new_class id par ar sup props = type binder_def_list = (identifier located * identifier located list * constr_expr) list let binders_of_lidents l = - List.map (fun (loc, id) -> LocalRawAssum ([loc, Name id], Default Rawterm.Implicit, CHole (loc, None))) l + List.map (fun (loc, id) -> + LocalRawAssum ([loc, Name id], Default Rawterm.Explicit, + CHole (loc, Some (BinderType (Name id))))) l let type_ctx_instance isevars env ctx inst subst = let (s, _) = @@ -312,7 +314,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) let tclass = match bk with | Implicit -> - Implicit_quantifiers.implicit_application Idset.empty + Implicit_quantifiers.implicit_application Idset.empty ~allow_partial:false (fun avoid (clname, (id, _, t)) -> match clname with | Some (cl, b) -> |