diff options
| author | Matthieu Sozeau | 2016-02-09 17:46:37 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-02-19 17:59:20 +0100 |
| commit | fd8038facfe10abb2c874ca4602b1d2ee0903056 (patch) | |
| tree | 13c4ddd1e78a1200e216bfb81973936822551d3f | |
| parent | 924d2833644735a9fa8289ffaa9bac9fbc43982c (diff) | |
Fix regression from 8.4 in reflexivity/...
reflexivity/symmetry/transitivity only need
RelationClasses to be loaded.
| -rw-r--r-- | tactics/rewrite.ml | 11 |
1 files 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 |