From 9bf62aeb8f96c334783e4e46d4b5e0792299e9fa Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 14 Sep 2014 16:52:35 +0200
Subject: Rewrite.apply_strategy uses the same return type as strategies.

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

(limited to 'tactics/rewrite.mli')

diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli
index 614e89a27e..4944f6475d 100644
--- a/tactics/rewrite.mli
+++ b/tactics/rewrite.mli
@@ -116,6 +116,4 @@ val apply_strategy :
   Names.Id.t list ->
   Term.constr ->
   bool * Term.constr ->
-  evars ->
-  (rewrite_proof * evars * Term.constr * Term.constr * Term.constr)
-    option option
+  evars -> rewrite_result
-- 
cgit v1.2.3