From 74ddca99c649f2f8c203582a9b82bddf64fb6b52 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 22 Apr 2014 15:31:12 +0200
Subject: Removing dead code, thanks to new OCaml warnings and a bit of
 scripting.

---
 proofs/clenvtac.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'proofs/clenvtac.ml')

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index c0036d192..7a1a14bde 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -79,9 +79,6 @@ let dft = default_unify_flags
 let res_pf clenv ?(with_evars=false) ?(flags=dft) gls =
   clenv_refine with_evars (clenv_unique_resolver ~flags clenv gls) gls
 
-let e_res_pf clenv = res_pf clenv ~with_evars:true ~flags:dft
-
-
 (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
    particulier ne semblent pas vérifier que des instances différentes
    d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas
-- 
cgit v1.2.3