diff options
Diffstat (limited to 'pretyping/pattern.mli')
| -rw-r--r-- | pretyping/pattern.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index d69b5e7242..115e86d61e 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -11,6 +11,7 @@ open Environ type constr_pattern = | PRef of global_reference | PVar of identifier + | PEvar of existential_key | PRel of int | PApp of constr_pattern * constr_pattern array | PSoApp of int * constr_pattern list |