From 86935e33e8f5d4fcc4b5603086d594431a002d0b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 17 Aug 2016 17:52:12 +0200
Subject: Fixing #5001 (metas not cleaned properly in clenv_refine_in).

Fixing by copying what Matthieu did for Clenvtac.clenv_refine.
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e151a06583..54977dbce7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1095,7 +1095,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true)
   let naming = NamingMustBe (dloc,targetid) in
   let with_clear = do_replace (Some id) naming in
   Tacticals.New.tclTHEN
-    (Proofview.Unsafe.tclEVARS clenv.evd)
+    (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd))
     (if sidecond_first then
        Tacticals.New.tclTHENFIRST
          (assert_before_then_gen with_clear naming new_hyp_typ tac) exact_tac
-- 
cgit v1.2.3