From cedcfc9bc386456f3fdd225f739706e4f7a2902c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 15 Dec 2015 10:51:08 +0100
Subject: Refine tactic now shelves unifiable holes.

The unshelve tactical can be used to get the shelved holes. This changes the
proper ordering of holes though, so expect some broken scripts. Also, the
test-suite is not fixed yet.
---
 tactics/extratactics.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 35efb0b65..ca65f08ec 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -357,7 +357,7 @@ let refine_tac {Glob_term.closure=closure;term=term} =
       Pretyping.ltac_idents = closure.Glob_term.idents;
     } in
     let update evd = Pretyping.understand_ltac flags env evd lvar tycon term in
-    Tactics.New.refine ~unsafe:false update
+    Tactics.New.refine ~unsafe:false update <*> Proofview.shelve_unifiable
   end
 
 TACTIC EXTEND refine
-- 
cgit v1.2.3