From 491eb32c55c9b57a5a49ebbdc46f41ca5cb359c7 Mon Sep 17 00:00:00 2001 From: msozeau Date: Thu, 16 Apr 2009 17:33:38 +0000 Subject: Better Requires in Classes. Fix bug #2093: the code does not require Program.Tactics anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12089 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/rewrite.ml4 | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) (limited to 'tactics/rewrite.ml4') diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 147e5384e..8efb0176e 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -42,18 +42,18 @@ open Evd (** Typeclass-based generalized rewriting. *) -let check_imported_library d = +let check_required_library d = let d' = List.map id_of_string d in let dir = make_dirpath (List.rev d') in if not (Library.library_is_loaded dir) then - error ("Library "^(list_last d)^" has to be imported first.") + error ("Library "^(list_last d)^" has to be required first.") let classes_dirpath = make_dirpath (List.map id_of_string ["Classes";"Coq"]) let init_setoid () = if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then () - else check_imported_library ["Coq";"Setoids";"Setoid"] + else check_required_library ["Coq";"Setoids";"Setoid"] let morphism_class = lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.Morphism")))) @@ -156,9 +156,6 @@ let is_applied_setoid_relation t = let _ = Equality.register_is_applied_setoid_relation is_applied_setoid_relation -exception Found of (constr * constr * (types * types) list * constr * constr array * - (constr * (constr * constr * constr * constr)) option array) - let split_head = function hd :: tl -> hd, tl | [] -> assert(false) @@ -1306,7 +1303,7 @@ let try_loaded f gl = let not_declared env ty rel = tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared " ++ - str ty ++ str" relation. Maybe you need to import the Setoid library") + str ty ++ str" relation. Maybe you need to require the Setoid library") let relation_of_constr env c = match kind_of_term c with -- cgit v1.2.3