diff options
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 0d9a51ba37..ccba1d2cc1 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -32,6 +32,7 @@ type hole_kind = | TomatchTypeParameter of inductive * int | GoalEvar | ImpossibleCase + | MatchingVar of bool * identifier (* The type of mappings for existential variables *) |