diff options
Diffstat (limited to 'pretyping/detyping.mli')
| -rw-r--r-- | pretyping/detyping.mli | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 32b94e1b..8695d52b 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -14,7 +14,6 @@ open EConstr open Glob_term open Termops open Mod_subst -open Misctypes open Evd open Ltac_pretype @@ -56,6 +55,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 *) @@ -81,7 +87,7 @@ val subst_genarg_hook : module PrintingInductiveMake : functor (Test : sig - val encode : Libnames.reference -> Names.inductive + val encode : Libnames.qualid -> Names.inductive val member_message : Pp.t -> bool -> Pp.t val field : string val title : string @@ -89,7 +95,7 @@ module PrintingInductiveMake : sig type t = Names.inductive val compare : t -> t -> int - val encode : Libnames.reference -> Names.inductive + val encode : Libnames.qualid -> Names.inductive val subst : substitution -> t -> t val printer : t -> Pp.t val key : Goptions.option_name |