From b6feaafc7602917a8ef86fb8adc9651ff765e710 Mon Sep 17 00:00:00 2001
From: Matej Košík <matej.kosik@inria.fr>
Date: Mon, 29 May 2017 11:02:06 +0200
Subject: Remove (useless) aliases from the API.

---
 plugins/ltac/rewrite.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins/ltac/rewrite.mli')

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 *)
 
-- 
cgit v1.2.3