From c5fdfe6ffef15795ecfde8f18f332ddefd35605e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 12 May 2020 15:50:02 +0200
Subject: Remove a unused legacy tactic from Clenv.

---
 proofs/clenv.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'proofs/clenv.mli')

diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 1adfdb885a..4279ab4768 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -63,9 +63,6 @@ val clenv_unify :
   ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
 
 (** unifies the concl of the goal with the type of the clenv *)
-val old_clenv_unique_resolver :
-  ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
-
 val clenv_unique_resolver :
   ?flags:unify_flags -> clausenv -> Proofview.Goal.t -> clausenv
 
-- 
cgit v1.2.3