diff options
Diffstat (limited to 'pretyping/pattern.mli')
| -rw-r--r-- | pretyping/pattern.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index ee0eefade..b0229ab61 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -72,7 +72,7 @@ val pattern_of_constr : constr -> constr_pattern a pattern; variables bound in [l] are replaced by the pattern to which they are bound *) -val pattern_of_rawconstr : rawconstr -> +val pattern_of_rawconstr : rawconstr -> patvar list * constr_pattern val instantiate_pattern : |