diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-28 17:24:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-28 20:58:05 +0200 |
| commit | 11371ee11cf22629aa931f69f14fff0cae0ce22a (patch) | |
| tree | 16392189caf095b29de02312ff06361f3e95ac76 /pretyping/detyping.mli | |
| parent | f1668e30eb4ad7787b3579f7265222d1db8ad973 (diff) | |
Detyping: Adding a variant of share_names for patterns.
Diffstat (limited to 'pretyping/detyping.mli')
| -rw-r--r-- | pretyping/detyping.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 32b94e1b0..817b8ba6e 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -56,6 +56,13 @@ val detype_sort : evar_map -> Sorts.t -> glob_sort val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.Set.t -> (names_context * env) -> evar_map -> rel_context -> 'a glob_decl_g list +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 -> + Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern -> + Pattern.constr_pattern -> + (Name.t * Decl_kinds.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 (** look for the index of a named var or a nondep var as it is renamed *) |