From 6ebd2316e5acf10e0d505804fdd7001edc5575fa Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 May 2015 11:54:49 +0200
Subject: Making the strategy type in Rewrite opaque.

---
 tactics/rewrite.mli | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli
index cae00f5a86..40a18ac458 100644
--- a/tactics/rewrite.mli
+++ b/tactics/rewrite.mli
@@ -55,10 +55,7 @@ type rewrite_result =
 | Identity
 | Success of rewrite_result_info
 
-type 'a pure_strategy = 'a -> Environ.env -> Id.t list -> constr -> types ->
-  (bool (* prop *) * constr option) -> evars -> 'a * rewrite_result
-
-type strategy = unit pure_strategy
+type strategy
 
 val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strategy
 
-- 
cgit v1.2.3