diff options
| author | msozeau | 2008-10-23 16:22:18 +0000 |
|---|---|---|
| committer | msozeau | 2008-10-23 16:22:18 +0000 |
| commit | 0b840f7aaece0c209850adb2a81904b54f410091 (patch) | |
| tree | 442e51c4aeea80184f77667f7abbd5a8d04e54b5 /interp/implicit_quantifiers.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/implicit_quantifiers.mli')
| -rw-r--r-- | interp/implicit_quantifiers.mli | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 5934272091..dc83e2135c 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -28,19 +28,20 @@ val ids_of_list : identifier list -> Idset.t val destClassApp : constr_expr -> loc * reference * constr_expr list val destClassAppExpl : constr_expr -> loc * reference * (constr_expr * explicitation located option) list -val free_vars_of_constr_expr : Topconstr.constr_expr -> - ?bound:Idset.t -> - Names.identifier list -> Names.identifier list +(* Fragile, should be used only for construction a set of identifiers to avoid *) -val free_vars_of_rawconstr : ?bound:Idset.t -> rawconstr -> (Names.identifier * loc) list - -val binder_list_of_ids : identifier list -> local_binder list - -val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier +val free_vars_of_constr_expr : constr_expr -> ?bound:Idset.t -> + identifier list -> identifier list val free_vars_of_binders : ?bound:Idset.t -> Names.identifier list -> local_binder list -> Idset.t * Names.identifier list +(* Returns the free ids in left-to-right order with the location of their first occurence *) + +val free_vars_of_rawconstr : ?bound:Idset.t -> rawconstr -> (Names.identifier * loc) list + +val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier + val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list val combine_params_freevar : |