aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tactics/leminv.ml2
-rw-r--r--tactics/tacticals.ml2
2 files changed, 2 insertions, 2 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 273633975a..76db1a0b73 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -10,7 +10,7 @@ open Sign
open Evd
open Printer
open Reduction
-open Constant
+open Declarations
open Inductive
open Environ
open Tacmach
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 6f8d55ef6f..2bd7df631f 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -7,7 +7,7 @@ open Names
open Generic
open Term
open Sign
-open Constant
+open Declarations
open Inductive
open Reduction
open Environ