aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/rewrite.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/rewrite.mli')
-rw-r--r--plugins/ltac/rewrite.mli3
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 77286452b..d7f92fd6e 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -8,7 +8,6 @@
open API
open Names
-open Constr
open Environ
open EConstr
open Constrexpr
@@ -39,7 +38,7 @@ type ('constr,'redexpr) strategy_ast =
type rewrite_proof =
| RewPrf of constr * constr
- | RewCast of cast_kind
+ | RewCast of Term.cast_kind
type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)