diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 7 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 44 |
2 files changed, 24 insertions, 27 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index ba3fa6fa0d..e5b032e638 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -693,12 +693,7 @@ let rewrite_except h = end -let refl_equal = - let coq_base_constant s = - Coqlib.gen_reference_in_modules "RecursiveDefinition" - (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s in - function () -> (coq_base_constant "eq_refl") - +let refl_equal () = Coqlib.lib_ref "core.eq.type" (* This is simply an implementation of the case_eq tactic. this code should be replaced by a call to the tactic but I don't know how to diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 5b8bd6d01a..9dd98a4ab7 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -56,12 +56,14 @@ let init_setoid () = if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then () else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"] +let find_reference dir s = + Coqlib.find_reference "generalized rewriting" dir s +[@@warning "-3"] + let lazy_find_reference dir s = - let gr = lazy (Coqlib.coq_reference "generalized rewriting" dir s) in + let gr = lazy (find_reference dir s) in fun () -> Lazy.force gr -let find_reference dir s = Coqlib.coq_reference "generalized rewriting" dir s - type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *) let find_global dir s = @@ -74,13 +76,13 @@ let find_global dir s = (** Global constants. *) -let coq_eq_ref = lazy_find_reference ["Init"; "Logic"] "eq" -let coq_eq = find_global ["Init"; "Logic"] "eq" -let coq_f_equal = find_global ["Init"; "Logic"] "f_equal" -let coq_all = find_global ["Init"; "Logic"] "all" -let impl = find_global ["Program"; "Basics"] "impl" +let coq_eq_ref () = Coqlib.lib_ref "core.eq.type" +let coq_eq = find_global ["Coq"; "Init"; "Logic"] "eq" +let coq_f_equal = find_global ["Coq"; "Init"; "Logic"] "f_equal" +let coq_all = find_global ["Coq"; "Init"; "Logic"] "all" +let impl = find_global ["Coq"; "Program"; "Basics"] "impl" -(** Bookkeeping which evars are constraints so that we can +(** Bookkeeping which evars are constraints so that we can remove them at the end of the tactic. *) let goalevars evars = fst evars @@ -154,7 +156,7 @@ end) = struct let respectful = find_global morphisms "respectful" let respectful_ref = lazy_find_reference morphisms "respectful" - let default_relation = find_global ["Classes"; "SetoidTactics"] "DefaultRelation" + let default_relation = find_global ["Coq"; "Classes"; "SetoidTactics"] "DefaultRelation" let coq_forall = find_global morphisms "forall_def" @@ -374,12 +376,12 @@ let type_app_poly env env evd f args = module PropGlobal = struct module Consts = struct - let relation_classes = ["Classes"; "RelationClasses"] - let morphisms = ["Classes"; "Morphisms"] - let relation = ["Relations";"Relation_Definitions"], "relation" + let relation_classes = ["Coq"; "Classes"; "RelationClasses"] + let morphisms = ["Coq"; "Classes"; "Morphisms"] + let relation = ["Coq"; "Relations";"Relation_Definitions"], "relation" let app_poly = app_poly_nocheck - let arrow = find_global ["Program"; "Basics"] "arrow" - let coq_inverse = find_global ["Program"; "Basics"] "flip" + let arrow = find_global ["Coq"; "Program"; "Basics"] "arrow" + let coq_inverse = find_global ["Coq"; "Program"; "Basics"] "flip" end module G = GlobalBindings(Consts) @@ -395,12 +397,12 @@ end module TypeGlobal = struct module Consts = struct - let relation_classes = ["Classes"; "CRelationClasses"] - let morphisms = ["Classes"; "CMorphisms"] + let relation_classes = ["Coq"; "Classes"; "CRelationClasses"] + let morphisms = ["Coq"; "Classes"; "CMorphisms"] let relation = relation_classes, "crelation" let app_poly = app_poly_check - let arrow = find_global ["Classes"; "CRelationClasses"] "arrow" - let coq_inverse = find_global ["Classes"; "CRelationClasses"] "flip" + let arrow = find_global ["Coq"; "Classes"; "CRelationClasses"] "arrow" + let coq_inverse = find_global ["Coq"; "Classes"; "CRelationClasses"] "flip" end module G = GlobalBindings(Consts) @@ -740,9 +742,9 @@ let new_global (evars, cstrs) gr = (sigma, cstrs), c let make_eq sigma = - new_global sigma (Coqlib.build_coq_eq ()) + new_global sigma Coqlib.(lib_ref "core.eq.type") let make_eq_refl sigma = - new_global sigma (Coqlib.build_coq_eq_refl ()) + new_global sigma Coqlib.(lib_ref "core.eq.refl") let get_rew_prf evars r = match r.rew_prf with | RewPrf (rel, prf) -> evars, (rel, prf) |