From ca30a8be08beeae77d42b6cb5d9f219e3932a3f7 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 5 Nov 2015 17:12:39 -0500
Subject: Fix bug #3257, setoid_reflexivity should fail if not completing the
 goal.

---
 tactics/rewrite.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index e8a7c0f600..af6953bf85 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -2077,8 +2077,10 @@ let poly_proof getp gett env evm car rel =
 let setoid_reflexivity =
   setoid_proof "reflexive"
     (fun env evm car rel -> 
-      tac_open (poly_proof PropGlobal.get_reflexive_proof TypeGlobal.get_reflexive_proof
-		  env evm car rel) (fun c -> Proofview.V82.of_tactic (apply c)))
+     tac_open (poly_proof PropGlobal.get_reflexive_proof
+			  TypeGlobal.get_reflexive_proof
+			  env evm car rel)
+	      (fun c -> tclCOMPLETE (Proofview.V82.of_tactic (apply c))))
     (reflexivity_red true)
 
 let setoid_symmetry =
-- 
cgit v1.2.3