From 5a419bafdb21fd61c4c5c0784c1a0156d5ec7005 Mon Sep 17 00:00:00 2001
From: jforest
Date: Tue, 2 Oct 2007 07:43:54 +0000
Subject: Correcting error message when adding Setoid, Relation or morphism
 (bug #1626)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10162 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/setoid_replace.ml | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 840cf979e4..176c9c4486 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -943,6 +943,7 @@ type morphism_signature =
  (bool option * Topconstr.constr_expr) list * Topconstr.constr_expr
 
 let new_named_morphism id m sign =
+  Coqlib.check_required_library ["Coq";"Setoids";"Setoid_tac"];
  let sign =
   match sign with
      None -> None
@@ -1130,21 +1131,23 @@ let int_add_relation id a aeq refl sym trans =
 
 (* The vernac command "Add Relation ..." *)
 let add_relation id a aeq refl sym trans =
- int_add_relation id (constr_of a) (constr_of aeq) (option_map constr_of refl)
-  (option_map constr_of sym) (option_map constr_of trans)
+  Coqlib.check_required_library ["Coq";"Setoids";"Setoid_tac"];
+  int_add_relation id (constr_of a) (constr_of aeq) (option_map constr_of refl)
+    (option_map constr_of sym) (option_map constr_of trans)
 
 (************************ Add Setoid ******************************************)
 
 (* The vernac command "Add Setoid" *)
 let add_setoid id a aeq th =
- let a = constr_of a in
- let aeq = constr_of aeq in
- let th = constr_of th in
- let env = Global.env () in
- let a_quantifiers_rev = check_a env a in
+  Coqlib.check_required_library ["Coq";"Setoids";"Setoid_tac"];
+  let a = constr_of a in
+  let aeq = constr_of aeq in
+  let th = constr_of th in
+  let env = Global.env () in
+  let a_quantifiers_rev = check_a env a in
   check_eq env a_quantifiers_rev a aeq  ;
   check_setoid_theory env a_quantifiers_rev a aeq  th ;
-   let a_instance = apply_to_rels a a_quantifiers_rev in
+  let a_instance = apply_to_rels a a_quantifiers_rev in
    let aeq_instance = apply_to_rels aeq a_quantifiers_rev in
    let th_instance = apply_to_rels th a_quantifiers_rev in
    let refl =
-- 
cgit v1.2.3