aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/constr_matching.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/constr_matching.mli')
-rw-r--r--pretyping/constr_matching.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli
index 34c62043e..780ccc23d 100644
--- a/pretyping/constr_matching.mli
+++ b/pretyping/constr_matching.mli
@@ -9,7 +9,7 @@
(** This module implements pattern-matching on terms *)
open Names
-open Term
+open Constr
open EConstr
open Environ
open Pattern