From fd8038facfe10abb2c874ca4602b1d2ee0903056 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 9 Feb 2016 17:46:37 +0100
Subject: Fix regression from 8.4 in reflexivity/...

reflexivity/symmetry/transitivity only need
RelationClasses to be loaded.
---
 tactics/rewrite.ml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index b04fb660d8..5ca74050a1 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -42,6 +42,10 @@ open Libnames
 let classes_dirpath =
   Names.DirPath.make (List.map Id.of_string ["Classes";"Coq"])
 
+let init_relation_classes () =
+  if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
+  else Coqlib.check_required_library ["Coq";"Classes";"RelationClasses"]
+
 let init_setoid () =
   if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
   else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"]
@@ -2041,8 +2045,9 @@ let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite_clause
 (** [setoid_]{reflexivity,symmetry,transitivity} tactics *)
 
 let not_declared env ty rel =
-  Tacticals.New.tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env Evd.empty rel ++ str" is not a declared " ++
-		str ty ++ str" relation. Maybe you need to require the Setoid library")
+  Tacticals.New.tclFAIL 0
+    (str" The relation " ++ Printer.pr_constr_env env Evd.empty rel ++ str" is not a declared " ++
+     str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library")
 
 let setoid_proof ty fn fallback =
   Proofview.Goal.nf_enter begin fun gl ->
@@ -2055,7 +2060,7 @@ let setoid_proof ty fn fallback =
           let rel, _, _ = decompose_app_rel env sigma concl in
           let (sigma, t) = Typing.type_of env sigma rel in
           let car = pi3 (List.hd (fst (Reduction.dest_prod env t))) in
-	    (try init_setoid () with _ -> raise Not_found);
+	    (try init_relation_classes () with _ -> raise Not_found);
             fn env sigma car rel
         with e -> Proofview.tclZERO e
       end
-- 
cgit v1.2.3