From 630f565077fa8f9ce9fdd0535b61901c6c539e02 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Thu, 27 Jul 2017 22:46:58 +0200
Subject: Fixing bug #5671 (specialize unclean wrt Metas).

---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8a95ad177..057bc774e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2979,7 +2979,7 @@ let specialize (c,lbind) ipat =
           sigma,hd'
         | _ ,_ -> assert false in
       let sigma,hd = rebuild_lambdas sigma (List.rev lprod) [] c_hd tstack in
-      sigma, hd
+      Evd.clear_metas sigma, hd
   in
   let typ = Retyping.get_type_of env sigma term in
   let tac =
-- 
cgit v1.2.3