diff options
| author | Emilio Jesus Gallego Arias | 2019-08-18 20:27:52 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-08-19 23:03:45 +0200 |
| commit | a74e055acf48583c6fece5d22c805736679376b2 (patch) | |
| tree | bc86b65608590013d7569b9585cd37029f2fa274 /pretyping/detyping.mli | |
| parent | 7f9a08b98b1637291dda687fce92198a21ffc395 (diff) | |
[api] Move handling of variable implicit data to impargs
We move `binder_kind` to the pretyping AST, removing the last data
type in the now orphaned file `Decl_kinds`.
This seems a better fit, as this data is not relevant to the lower
layers but only used in `Impargs`.
We also move state keeping to `Impargs`, so now implicit declaration
must include the type. We also remove a duplicated function.
Diffstat (limited to 'pretyping/detyping.mli')
| -rw-r--r-- | pretyping/detyping.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index cc9f520583..9eb014aa62 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -57,10 +57,10 @@ val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.Set.t -> ( val share_pattern_names : (Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern -> 'a) -> int -> - (Name.t * Decl_kinds.binding_kind * 'b option * 'a) list -> + (Name.t * binding_kind * 'b option * 'a) list -> Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern -> Pattern.constr_pattern -> - (Name.t * Decl_kinds.binding_kind * 'b option * 'a) list * 'a * 'a + (Name.t * binding_kind * 'b option * 'a) list * 'a * 'a val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> closed_glob_constr -> glob_constr |