diff options
Diffstat (limited to 'pretyping/matching.ml')
| -rw-r--r-- | pretyping/matching.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 5460d8ba1..ab90b5601 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -16,6 +16,8 @@ open Nameops open Termops open Reductionops open Term +open Vars +open Context open Pattern open Patternops open Misctypes |