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

---
 tactics/tactics.ml            | 2 +-
 test-suite/bugs/closed/5671.v | 7 +++++++
 2 files changed, 8 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/5671.v

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8a95ad177d..057bc774ee 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 =
diff --git a/test-suite/bugs/closed/5671.v b/test-suite/bugs/closed/5671.v
new file mode 100644
index 0000000000..c9a085045a
--- /dev/null
+++ b/test-suite/bugs/closed/5671.v
@@ -0,0 +1,7 @@
+(* Fixing Meta-unclean specialize *)
+
+Require Import Setoid.
+Axiom a : forall x, x=0 -> True.
+Lemma lem (x y1 y2:nat) (H:x=0) (H0:eq y1 y2) : y1 = y2.
+specialize a with (1:=H). clear H x. intros _.
+setoid_rewrite H0.
-- 
cgit v1.2.3