diff options
author | 2009-04-16 17:33:38 +0000 | |
---|---|---|
committer | 2009-04-16 17:33:38 +0000 | |
commit | 491eb32c55c9b57a5a49ebbdc46f41ca5cb359c7 (patch) | |
tree | 9a74d9ea6a65a10d9a80fde72027f0f809a9af18 /tactics/rewrite.ml4 | |
parent | 665761c4e82504a579d335b529b2e61f0414665c (diff) |
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
Diffstat (limited to 'tactics/rewrite.ml4')
-rw-r--r-- | tactics/rewrite.ml4 | 11 |
1 files changed, 4 insertions, 7 deletions
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 |