diff options
Diffstat (limited to 'pretyping/constr_matching.mli')
| -rw-r--r-- | pretyping/constr_matching.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 32bb48c93..4734c90a8 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -64,7 +64,7 @@ val matches_conv : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map (whose hole is denoted here with [special_meta]) *) type matching_result = { m_sub : bound_ident_map * patvar_map; - m_ctx : Constr.t } + m_ctx : EConstr.t } (** [match_subterm n pat c] returns the substitution and the context corresponding to each **closed** subterm of [c] matching [pat]. *) |