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.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 37d54a4eea..08178052bf 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -321,10 +321,6 @@ let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl =
     clenv_unify CUMUL ~flags
       (meta_reducible_instance clenv.evd clenv.templtyp) concl clenv
 
-let old_clenv_unique_resolver ?flags clenv gl =
-  let concl = Goal.V82.concl clenv.evd (sig_it gl) in
-  clenv_unique_resolver_gen ?flags clenv concl
-
 let clenv_unique_resolver ?flags clenv gl =
   let concl = Proofview.Goal.concl gl in
   clenv_unique_resolver_gen ?flags clenv concl
-- 
cgit v1.2.3