diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/matching.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/matching.mli b/pretyping/matching.mli index 5ba68f26bf..3501584c06 100644 --- a/pretyping/matching.mli +++ b/pretyping/matching.mli @@ -33,7 +33,7 @@ type bound_ident_map = (Id.t * Id.t) list numbers given in the pattern *) val matches : constr_pattern -> constr -> patvar_map -(** [matches_head pat c] does the same as |matches pat c] but accepts +(** [matches_head pat c] does the same as [matches pat c] but accepts [pat] to match an applicative prefix of [c] *) val matches_head : constr_pattern -> constr -> patvar_map |