diff options
Diffstat (limited to 'parsing/pattern.ml')
| -rw-r--r-- | parsing/pattern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/pattern.ml b/parsing/pattern.ml index 47c1d5716d..2d989fafc6 100644 --- a/parsing/pattern.ml +++ b/parsing/pattern.ml @@ -73,7 +73,7 @@ let head_of_constr_reference c = match kind_of_term c with (* Second part : Given a term with second-order variables in it, - represented by Meta's, and possibly applied using XTRA[$SOAPP] to + represented by Meta's, and possibly applied using [SOAPP] to terms, this function will perform second-order, binding-preserving, matching, in the case where the pattern is a pattern in the sense of Dale Miller. |