aboutsummaryrefslogtreecommitdiff
path: root/tactics/hipattern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/hipattern.ml')
-rw-r--r--tactics/hipattern.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 53ffa7a350..c11fd1699b 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -21,6 +21,7 @@ open Environ
open Proof_trees
open Clenv
open Pattern
+open Matching
open Coqlib
open Declarations