From 4db867c45dafc7ed7b524a8d089cd57b7944feca Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 27 Jun 2014 12:45:11 +0200
Subject: Add an init_setoid check in rewrite to avoid trying to get undefined
 references. Fixes the behavior of reflexivity/symmetry etc... when Setoid is
 not loaded.

---
 tactics/rewrite.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 06d0a04cc2..7b8b0cc55c 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1967,7 +1967,8 @@ let setoid_proof ty fn fallback =
           let rel, args = decompose_app_rel env sigma concl in
           let evm = sigma in
           let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in
-          fn env sigma car rel
+	    (try init_setoid () with _ -> raise Not_found);
+            fn env sigma car rel
         with e -> Proofview.tclZERO e
       end
       begin function
-- 
cgit v1.2.3