aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tactics/hipattern.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index fd871349c7..7bf9fa0e1b 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -15,7 +15,7 @@ open Names
open Term
open Termops
open Inductiveops
-open ConstrMatching
+open Constr_matching
open Coqlib
open Declarations
open Tacmach.New