diff options
| -rw-r--r-- | pretyping/detyping.ml | 23 | ||||
| -rw-r--r-- | pretyping/detyping.mli | 7 |
2 files changed, 30 insertions, 0 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 1d426e9ea..bb563220b 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -537,6 +537,29 @@ let rec share_names detype n l avoid env sigma c t = let t = detype avoid env sigma t in (List.rev l,c,t) +let rec share_pattern_names detype n l avoid env sigma c t = + let open Pattern in + if n = 0 then + let c = detype avoid env sigma c in + let t = detype avoid env sigma t in + (List.rev l,c,t) + else match c, t with + | PLambda (na,t,c), PProd (na',t',c') -> + let na = match (na,na') with + Name _, _ -> na + | _, Name _ -> na' + | _ -> na in + let t' = detype avoid env sigma t in + let id = next_name_away na avoid in + let avoid = Id.Set.add id avoid in + let env = Name id :: env in + share_pattern_names detype (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c' + | _ -> + if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough"); + let c = detype avoid env sigma c in + let t = detype avoid env sigma t in + (List.rev l,c,t) + let detype_fix detype avoid env sigma (vn,_ as nvn) (names,tys,bodies) = let def_avoid, def_env, lfi = Array.fold_left2 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 *) |