aboutsummaryrefslogtreecommitdiff
path: root/library/impargs.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/impargs.ml')
-rw-r--r--library/impargs.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/library/impargs.ml b/library/impargs.ml
index d7d0d48796..707b2f4cbe 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -19,7 +19,7 @@ open Libobject
open Lib
open Nametab
open Pp
-open Topconstr
+open Constrexpr
open Termops
open Namegen
open Decl_kinds
@@ -614,7 +614,7 @@ let declare_mib_implicits kn =
(inImplicits (ImplMutualInductive (kn,flags),List.flatten imps))
(* Declare manual implicits *)
-type manual_explicitation = Topconstr.explicitation * (bool * bool * bool)
+type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool)
type manual_implicits = manual_explicitation list