diff options
| author | Emilio Jesus Gallego Arias | 2017-10-02 12:22:32 +0200 |
|---|---|---|
| committer | Vincent Laporte | 2018-10-10 15:19:07 +0000 |
| commit | 8ac6145d5cc14823df48698a755d8adf048f026c (patch) | |
| tree | fa8bf650d111b828958ad7468fd0ec3b445d2305 | |
| parent | ea38cc10b1b3d81e2346de6b95076733ef4fd7bb (diff) | |
[coqlib] Rebindable Coqlib namespace.
We refactor the `Coqlib` API to locate objects over a namespace
`module.object.property`.
This introduces the vernacular command `Register g as n` to expose the
Coq constant `g` under the name `n` (through the `register_ref`
function). The constant can then be dynamically located using the
`lib_ref` function.
Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org>
Co-authored-by: Maxime Dénès <mail@maximedenes.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
76 files changed, 1180 insertions, 842 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 7e64f80ac5..32d457c6dd 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -19,6 +19,14 @@ Names Constant.make3 has been removed, use Constant.make2 Constant.repr3 has been removed, use Constant.repr2 +Coqlib: + +- Most functions from the `Coqlib` module have been deprecated in favor of + `register_ref` and `lib_ref`. The first one is available through the + vernacular `Register` command; it binds a name to a constant. The second + command then enables to locate the registered constant through its name. The + name resolution is dynamic. + ## Changes between Coq 8.8 and Coq 8.9 ### ML API diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index be65ff7570..125c4c25a3 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1200,3 +1200,18 @@ scope of their effect. There are four kinds of commands: modifier extends the effect outside the module even when the command occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this category. + +.. _exposing-constants-to-ocaml-libraries: + +Exposing constants to OCaml libraries +---------------------------------------------------------------- + +.. cmd:: Register @qualid__1 as @qualid__2 + + This command exposes the constant :n:`@qualid__1` to OCaml libraries under + the name :n:`@qualid__2`. This constant can then be dynamically located + calling :n:`Coqlib.lib_ref "@qualid__2"`; i.e., there is no need to known + where is the constant defined (file, module, library, etc.). + + Due to its internal nature, this command is not for general use. It is meant + to appear only in standard libraries and in support libraries of plug-ins. diff --git a/library/coqlib.ml b/library/coqlib.ml index e71de4d77e..677515981a 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -16,29 +16,68 @@ open Libnames open Globnames open Nametab -let coq = Libnames.coq_string (* "Coq" *) +let make_dir l = DirPath.make (List.rev_map Id.of_string l) (************************************************************************) -(* Generic functions to find Coq objects *) +(* Coq reference API *) +(************************************************************************) +let coq = Libnames.coq_string (* "Coq" *) -type message = string +let init_dir = [ coq; "Init"] -let make_dir l = DirPath.make (List.rev_map Id.of_string l) +let jmeq_module_name = [coq;"Logic";"JMeq"] +let jmeq_library_path = make_dir jmeq_module_name +let jmeq_module = MPfile jmeq_library_path let find_reference locstr dir s = let dp = make_dir dir in let sp = Libnames.make_path dp (Id.of_string s) in - try Nametab.global_of_path sp - with Not_found -> - (* Following bug 5066 we are more permissive with the handling - of not found errors here *) - user_err ~hdr:locstr - Pp.(str "cannot find " ++ Libnames.pr_path sp ++ - str "; maybe library " ++ DirPath.print dp ++ - str " has to be required first.") + Nametab.global_of_path sp let coq_reference locstr dir s = find_reference locstr (coq::dir) s +let table : GlobRef.t CString.Map.t ref = + let name = "coqlib_registered" in + Summary.ref ~name CString.Map.empty + +let get_lib_refs () = + CString.Map.bindings !table + +let has_ref s = CString.Map.mem s !table + +let check_ind_ref s ind = + match CString.Map.find s !table with + | IndRef r -> eq_ind r ind + | _ -> false + | exception Not_found -> false + +let lib_ref s = + try CString.Map.find s !table + with Not_found -> + user_err Pp.(str "not found in table: " ++ str s) + +let add_ref s c = + table := CString.Map.add s c !table + +let cache_ref (_,(s,c)) = + add_ref s c + +let (inCoqlibRef : string * GlobRef.t -> Libobject.obj) = + let open Libobject in + declare_object { (default_object "COQLIBREF") with + cache_function = cache_ref; + load_function = (fun _ x -> cache_ref x); + classify_function = (fun o -> Substitute o); + subst_function = ident_subst_function; + discharge_function = fun (_, sc) -> Some sc } + +(** Replaces a binding ! *) +let register_ref s c = + Lib.add_anonymous_leaf @@ inCoqlibRef (s,c) + +(************************************************************************) +(* Generic functions to find Coq objects *) + let has_suffix_in_dirs dirs ref = let dir = dirpath (path_of_global ref) in List.exists (fun d -> is_dirpath_prefix_of d dir) dirs @@ -74,25 +113,12 @@ let check_required_library d = | _ -> false in if not in_current_dir then -(* Loading silently ... - let m, prefix = List.sep_last d' in - read_library - (Loc.ghost,make_qualid (DirPath.make (List.rev prefix)) m) -*) -(* or failing ...*) user_err ~hdr:"Coqlib.check_required_library" (str "Library " ++ DirPath.print dir ++ str " has to be required first.") (************************************************************************) -(* Specific Coq objects *) - -let init_reference dir s = - let d = coq::"Init"::dir in - check_required_library d; find_reference "Coqlib" d s - -let logic_reference dir s = - let d = coq::"Logic"::dir in - check_required_library d; find_reference "Coqlib" d s +(* Specific Coq objects *) +(************************************************************************) let arith_dir = [coq;"Arith"] let arith_modules = [arith_dir] @@ -104,7 +130,6 @@ let zarith_dir = [coq;"ZArith"] let zarith_base_modules = [numbers_dir;parith_dir;narith_dir;zarith_dir] -let init_dir = [coq;"Init"] let init_modules = [ init_dir@["Datatypes"]; init_dir@["Logic"]; @@ -115,9 +140,6 @@ let init_modules = [ init_dir@["Wf"] ] -let prelude_module_name = init_dir@["Prelude"] -let prelude_module = make_dir prelude_module_name - let logic_module_name = init_dir@["Logic"] let logic_module = MPfile (make_dir logic_module_name) @@ -127,10 +149,6 @@ let logic_type_module = make_dir logic_type_module_name let datatypes_module_name = init_dir@["Datatypes"] let datatypes_module = MPfile (make_dir datatypes_module_name) -let jmeq_module_name = [coq;"Logic";"JMeq"] -let jmeq_library_path = make_dir jmeq_module_name -let jmeq_module = MPfile jmeq_library_path - (** Identity *) let id = Constant.make2 datatypes_module @@ Label.make "idProp" @@ -167,6 +185,7 @@ let glob_identity = IndRef (identity_kn,0) let jmeq_kn = MutInd.make2 jmeq_module @@ Label.make "JMeq" let glob_jmeq = IndRef (jmeq_kn,0) +(* Sigma data *) type coq_sigma_data = { proj1 : GlobRef.t; proj2 : GlobRef.t; @@ -174,39 +193,29 @@ type coq_sigma_data = { intro : GlobRef.t; typ : GlobRef.t } +let build_sigma_gen str = + { typ = lib_ref ("core." ^ str ^ ".type"); + elim = lib_ref ("core." ^ str ^ ".rect"); + intro = lib_ref ("core." ^ str ^ ".intro"); + proj1 = lib_ref ("core." ^ str ^ ".proj1"); + proj2 = lib_ref ("core." ^ str ^ ".proj2"); + } + +let build_prod () = build_sigma_gen "prod" +let build_sigma () = build_sigma_gen "sig" +let build_sigma_type () = build_sigma_gen "sigT" + +(* Booleans *) + type coq_bool_data = { andb : GlobRef.t; andb_prop : GlobRef.t; andb_true_intro : GlobRef.t} let build_bool_type () = - { andb = init_reference ["Datatypes"] "andb"; - andb_prop = init_reference ["Datatypes"] "andb_prop"; - andb_true_intro = init_reference ["Datatypes"] "andb_true_intro" } - -let build_sigma_set () = anomaly (Pp.str "Use build_sigma_type.") - -let build_sigma_type () = - { proj1 = init_reference ["Specif"] "projT1"; - proj2 = init_reference ["Specif"] "projT2"; - elim = init_reference ["Specif"] "sigT_rect"; - intro = init_reference ["Specif"] "existT"; - typ = init_reference ["Specif"] "sigT" } - -let build_sigma () = - { proj1 = init_reference ["Specif"] "proj1_sig"; - proj2 = init_reference ["Specif"] "proj2_sig"; - elim = init_reference ["Specif"] "sig_rect"; - intro = init_reference ["Specif"] "exist"; - typ = init_reference ["Specif"] "sig" } - - -let build_prod () = - { proj1 = init_reference ["Datatypes"] "fst"; - proj2 = init_reference ["Datatypes"] "snd"; - elim = init_reference ["Datatypes"] "prod_rec"; - intro = init_reference ["Datatypes"] "pair"; - typ = init_reference ["Datatypes"] "prod" } + { andb = lib_ref "core.bool.andb"; + andb_prop = lib_ref "core.bool.andb_prop"; + andb_true_intro = lib_ref "core.bool.andb_true_intro"; } (* Equalities *) type coq_eq_data = { @@ -217,6 +226,24 @@ type coq_eq_data = { trans: GlobRef.t; congr: GlobRef.t } +(* Leibniz equality on Type *) + +let build_eqdata_gen lib str = + let _ = check_required_library lib in { + eq = lib_ref ("core." ^ str ^ ".type"); + ind = lib_ref ("core." ^ str ^ ".ind"); + refl = lib_ref ("core." ^ str ^ ".refl"); + sym = lib_ref ("core." ^ str ^ ".sym"); + trans = lib_ref ("core." ^ str ^ ".trans"); + congr = lib_ref ("core." ^ str ^ ".congr"); + } + +let build_coq_eq_data () = build_eqdata_gen logic_module_name "eq" +let build_coq_jmeq_data () = build_eqdata_gen jmeq_module_name "JMeq" +let build_coq_identity_data () = build_eqdata_gen datatypes_module_name "identity" + +(* Inversion data... *) + (* Data needed for discriminate and injection *) type coq_inversion_data = { inv_eq : GlobRef.t; (* : forall params, t -> Prop *) @@ -224,161 +251,75 @@ type coq_inversion_data = { inv_congr: GlobRef.t (* : forall params B (f:t->B) y, eq params y -> f c=f y *) } -let lazy_init_reference dir id = lazy (init_reference dir id) -let lazy_logic_reference dir id = lazy (logic_reference dir id) - -(* Leibniz equality on Type *) - -let coq_eq_eq = lazy_init_reference ["Logic"] "eq" -let coq_eq_refl = lazy_init_reference ["Logic"] "eq_refl" -let coq_eq_ind = lazy_init_reference ["Logic"] "eq_ind" -let coq_eq_congr = lazy_init_reference ["Logic"] "f_equal" -let coq_eq_sym = lazy_init_reference ["Logic"] "eq_sym" -let coq_eq_trans = lazy_init_reference ["Logic"] "eq_trans" -let coq_f_equal2 = lazy_init_reference ["Logic"] "f_equal2" -let coq_eq_congr_canonical = - lazy_init_reference ["Logic"] "f_equal_canonical_form" - -let build_coq_eq_data () = - let _ = check_required_library logic_module_name in { - eq = Lazy.force coq_eq_eq; - ind = Lazy.force coq_eq_ind; - refl = Lazy.force coq_eq_refl; - sym = Lazy.force coq_eq_sym; - trans = Lazy.force coq_eq_trans; - congr = Lazy.force coq_eq_congr } - -let build_coq_eq () = Lazy.force coq_eq_eq -let build_coq_eq_refl () = Lazy.force coq_eq_refl -let build_coq_eq_sym () = Lazy.force coq_eq_sym -let build_coq_f_equal2 () = Lazy.force coq_f_equal2 +let build_coq_inversion_gen l str = + List.iter check_required_library l; { + inv_eq = lib_ref ("core." ^ str ^ ".type"); + inv_ind = lib_ref ("core." ^ str ^ ".ind"); + inv_congr = lib_ref ("core." ^ str ^ ".congr_canonical"); + } let build_coq_inversion_eq_data () = - let _ = check_required_library logic_module_name in { - inv_eq = Lazy.force coq_eq_eq; - inv_ind = Lazy.force coq_eq_ind; - inv_congr = Lazy.force coq_eq_congr_canonical } - -(* Heterogenous equality on Type *) - -let coq_jmeq_eq = lazy_logic_reference ["JMeq"] "JMeq" -let coq_jmeq_hom = lazy_logic_reference ["JMeq"] "JMeq_hom" -let coq_jmeq_refl = lazy_logic_reference ["JMeq"] "JMeq_refl" -let coq_jmeq_ind = lazy_logic_reference ["JMeq"] "JMeq_ind" -let coq_jmeq_sym = lazy_logic_reference ["JMeq"] "JMeq_sym" -let coq_jmeq_congr = lazy_logic_reference ["JMeq"] "JMeq_congr" -let coq_jmeq_trans = lazy_logic_reference ["JMeq"] "JMeq_trans" -let coq_jmeq_congr_canonical = - lazy_logic_reference ["JMeq"] "JMeq_congr_canonical_form" - -let build_coq_jmeq_data () = - let _ = check_required_library jmeq_module_name in { - eq = Lazy.force coq_jmeq_eq; - ind = Lazy.force coq_jmeq_ind; - refl = Lazy.force coq_jmeq_refl; - sym = Lazy.force coq_jmeq_sym; - trans = Lazy.force coq_jmeq_trans; - congr = Lazy.force coq_jmeq_congr } - -let build_coq_inversion_jmeq_data () = - let _ = check_required_library logic_module_name in { - inv_eq = Lazy.force coq_jmeq_hom; - inv_ind = Lazy.force coq_jmeq_ind; - inv_congr = Lazy.force coq_jmeq_congr_canonical } - -(* Specif *) -let coq_sumbool = lazy_init_reference ["Specif"] "sumbool" - -let build_coq_sumbool () = Lazy.force coq_sumbool - -(* Equality on Type as a Type *) -let coq_identity_eq = lazy_init_reference ["Datatypes"] "identity" -let coq_identity_refl = lazy_init_reference ["Datatypes"] "identity_refl" -let coq_identity_ind = lazy_init_reference ["Datatypes"] "identity_ind" -let coq_identity_congr = lazy_init_reference ["Logic_Type"] "identity_congr" -let coq_identity_sym = lazy_init_reference ["Logic_Type"] "identity_sym" -let coq_identity_trans = lazy_init_reference ["Logic_Type"] "identity_trans" -let coq_identity_congr_canonical = lazy_init_reference ["Logic_Type"] "identity_congr_canonical_form" - -let build_coq_identity_data () = - let _ = check_required_library datatypes_module_name in { - eq = Lazy.force coq_identity_eq; - ind = Lazy.force coq_identity_ind; - refl = Lazy.force coq_identity_refl; - sym = Lazy.force coq_identity_sym; - trans = Lazy.force coq_identity_trans; - congr = Lazy.force coq_identity_congr } - -let build_coq_inversion_identity_data () = - let _ = check_required_library datatypes_module_name in - let _ = check_required_library logic_type_module_name in { - inv_eq = Lazy.force coq_identity_eq; - inv_ind = Lazy.force coq_identity_ind; - inv_congr = Lazy.force coq_identity_congr_canonical } - -(* Equality to true *) -let coq_eq_true_eq = lazy_init_reference ["Datatypes"] "eq_true" -let coq_eq_true_ind = lazy_init_reference ["Datatypes"] "eq_true_ind" -let coq_eq_true_congr = lazy_init_reference ["Logic"] "eq_true_congr" + build_coq_inversion_gen [logic_module_name] "eq" let build_coq_inversion_eq_true_data () = - let _ = check_required_library datatypes_module_name in - let _ = check_required_library logic_module_name in { - inv_eq = Lazy.force coq_eq_true_eq; - inv_ind = Lazy.force coq_eq_true_ind; - inv_congr = Lazy.force coq_eq_true_congr } + build_coq_inversion_gen [logic_module_name] "True" -(* The False proposition *) -let coq_False = lazy_init_reference ["Logic"] "False" - -(* The True proposition and its unique proof *) -let coq_True = lazy_init_reference ["Logic"] "True" -let coq_I = lazy_init_reference ["Logic"] "I" +let build_coq_inversion_identity_data () = + build_coq_inversion_gen [logic_module_name] "identity" -(* Connectives *) -let coq_not = lazy_init_reference ["Logic"] "not" -let coq_and = lazy_init_reference ["Logic"] "and" -let coq_conj = lazy_init_reference ["Logic"] "conj" -let coq_or = lazy_init_reference ["Logic"] "or" -let coq_ex = lazy_init_reference ["Logic"] "ex" -let coq_iff = lazy_init_reference ["Logic"] "iff" +(* This needs a special case *) +let build_coq_inversion_jmeq_data () = { + inv_eq = lib_ref "core.JMeq.hom"; + inv_ind = lib_ref "core.JMeq.ind"; + inv_congr = lib_ref "core.JMeq.congr_canonical"; +} -let coq_iff_left_proj = lazy_init_reference ["Logic"] "proj1" -let coq_iff_right_proj = lazy_init_reference ["Logic"] "proj2" +(* Specif *) +let build_coq_sumbool () = lib_ref "core.sumbool.type" -let coq_prod = lazy_init_reference ["Datatypes"] "prod" -let coq_pair = lazy_init_reference ["Datatypes"] "pair" +let build_coq_eq () = lib_ref "core.eq.type" +let build_coq_eq_refl () = lib_ref "core.eq.refl" +let build_coq_eq_sym () = lib_ref "core.eq.sym" +let build_coq_f_equal2 () = lib_ref "core.eq.congr2" (* Runtime part *) -let build_coq_True () = Lazy.force coq_True -let build_coq_I () = Lazy.force coq_I +let build_coq_True () = lib_ref "core.True.type" +let build_coq_I () = lib_ref "core.True.I" +let build_coq_identity () = lib_ref "core.identity.type" -let build_coq_False () = Lazy.force coq_False -let build_coq_not () = Lazy.force coq_not -let build_coq_and () = Lazy.force coq_and -let build_coq_conj () = Lazy.force coq_conj -let build_coq_or () = Lazy.force coq_or -let build_coq_ex () = Lazy.force coq_ex -let build_coq_iff () = Lazy.force coq_iff +let build_coq_eq_true () = lib_ref "core.eq_true.type" +let build_coq_jmeq () = lib_ref "core.JMeq.type" -let build_coq_iff_left_proj () = Lazy.force coq_iff_left_proj -let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj +let build_coq_prod () = lib_ref "core.prod.type" +let build_coq_pair () = lib_ref "core.prod.intro" -let build_coq_prod () = Lazy.force coq_prod -let build_coq_pair () = Lazy.force coq_pair +let build_coq_False () = lib_ref "core.False.type" +let build_coq_not () = lib_ref "core.not.type" +let build_coq_and () = lib_ref "core.and.type" +let build_coq_conj () = lib_ref "core.and.conj" +let build_coq_or () = lib_ref "core.or.type" +let build_coq_ex () = lib_ref "core.ex.type" +let build_coq_sig () = lib_ref "core.sig.type" +let build_coq_existT () = lib_ref "core.sigT.existT" +let build_coq_iff () = lib_ref "core.iff.type" +let build_coq_iff_left_proj () = lib_ref "core.iff.proj1" +let build_coq_iff_right_proj () = lib_ref "core.iff.proj2" (* The following is less readable but does not depend on parsing *) -let coq_eq_ref = lazy (init_reference ["Logic"] "eq") -let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity") -let coq_jmeq_ref = lazy (find_reference "Coqlib" [coq;"Logic";"JMeq"] "JMeq") -let coq_eq_true_ref = lazy (find_reference "Coqlib" [coq;"Init";"Datatypes"] "eq_true") -let coq_existS_ref = lazy (anomaly (Pp.str "use coq_existT_ref.")) -let coq_existT_ref = lazy (init_reference ["Specif"] "existT") -let coq_exist_ref = lazy (init_reference ["Specif"] "exist") -let coq_not_ref = lazy (init_reference ["Logic"] "not") -let coq_False_ref = lazy (init_reference ["Logic"] "False") -let coq_sumbool_ref = lazy (init_reference ["Specif"] "sumbool") -let coq_sig_ref = lazy (init_reference ["Specif"] "sig") -let coq_or_ref = lazy (init_reference ["Logic"] "or") -let coq_iff_ref = lazy (init_reference ["Logic"] "iff") +let coq_eq_ref = Lazy.from_fun build_coq_eq +let coq_identity_ref = Lazy.from_fun build_coq_identity +let coq_jmeq_ref = Lazy.from_fun build_coq_jmeq +let coq_eq_true_ref = Lazy.from_fun build_coq_eq_true +let coq_existS_ref = Lazy.from_fun build_coq_existT +let coq_existT_ref = Lazy.from_fun build_coq_existT +let coq_exist_ref = Lazy.from_fun build_coq_ex +let coq_not_ref = Lazy.from_fun build_coq_not +let coq_False_ref = Lazy.from_fun build_coq_False +let coq_sumbool_ref = Lazy.from_fun build_coq_sumbool +let coq_sig_ref = Lazy.from_fun build_coq_sig +let coq_or_ref = Lazy.from_fun build_coq_or +let coq_iff_ref = Lazy.from_fun build_coq_iff + +(** Deprecated functions that search by library name. *) +let build_sigma_set () = anomaly (Pp.str "Use build_sigma_type.") diff --git a/library/coqlib.mli b/library/coqlib.mli index 6a3d0953cd..351a0a7e84 100644 --- a/library/coqlib.mli +++ b/library/coqlib.mli @@ -10,92 +10,164 @@ open Util open Names -open Libnames -(** This module collects the global references, constructions and - patterns of the standard library used in ocaml files *) +(** Indirection between logical names and global references. -(** The idea is to migrate to rebindable name-based approach, thus the - only function this FILE will provide will be: + This module provides a mechanism to bind “names” to constants and to look up + these constants using their names. - [find_reference : string -> global_reference] + The two main functions are [register_ref n r] which binds the name [n] to + the reference [r] and [lib_ref n] which returns the previously registered + reference under name [n]. - such that [find_reference "core.eq.type"] returns the proper [global_reference] + The first function is meant to be available through the vernacular command + [Register r as n], so that plug-ins can refer to a constant without knowing + its user-facing name, the precise module path in which it is defined, etc. - [bind_reference : string -> global_reference -> unit] + For instance, [lib_ref "core.eq.type"] returns the proper [GlobRef.t] for + the type of the core equality type. +*) - will bind a reference. +(** Registers a global reference under the given name. *) +val register_ref : string -> GlobRef.t -> unit - A feature based approach would be possible too. +(** Retrieves the reference bound to the given name (by a previous call to {!register_ref}). + Raises an error if no reference is bound to this name. *) +val lib_ref : string -> GlobRef.t - Contrary to the old approach of raising an anomaly, we expect - tactics to gracefully fail in the absence of some primitive. +(** Checks whether a name refers to a registered constant. + For any name [n], if [has_ref n] returns [true], [lib_ref n] will succeed. *) +val has_ref : string -> bool - This is work in progress, see below. -*) +(** Checks whether a name is bound to a known inductive. *) +val check_ind_ref : string -> inductive -> bool + +(** List of all currently bound names. *) +val get_lib_refs : unit -> (string * GlobRef.t) list + +(* Exceptions to deprecation *) + +(** {2 For Equality tactics} *) + +type coq_sigma_data = { + proj1 : GlobRef.t; + proj2 : GlobRef.t; + elim : GlobRef.t; + intro : GlobRef.t; + typ : GlobRef.t } + +val build_sigma_set : coq_sigma_data delayed +val build_sigma_type : coq_sigma_data delayed +val build_sigma : coq_sigma_data delayed + +type coq_eq_data = { + eq : GlobRef.t; + ind : GlobRef.t; + refl : GlobRef.t; + sym : GlobRef.t; + trans: GlobRef.t; + congr: GlobRef.t } + +val build_coq_eq_data : coq_eq_data delayed +val build_coq_identity_data : coq_eq_data delayed +val build_coq_jmeq_data : coq_eq_data delayed + +(* XXX: Some tactics special case JMeq, they should instead check for + the constant, not the module *) +(** For tactics/commands requiring vernacular libraries *) +val check_required_library : string list -> unit + +(* Used by obligations *) +val datatypes_module_name : string list + +(* Used by ind_schemes *) +val logic_module_name : string list + +(* Used by tactics *) +val jmeq_module_name : string list + + +(*************************************************************************) +(** {2 DEPRECATED} *) +(*************************************************************************) + +(** All the functions below are deprecated and should go away in the + next coq version ... *) -(** {6 ... } *) (** [find_reference caller_message [dir;subdir;...] s] returns a global reference to the name dir.subdir.(...).s; the corresponding module must have been required or in the process of being compiled so that it must be used lazily; it raises an anomaly with the given message if not found *) +val find_reference : string -> string list -> string -> GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] -type message = string - -val find_reference : message -> string list -> string -> GlobRef.t -val coq_reference : message -> string list -> string -> GlobRef.t - -(** For tactics/commands requiring vernacular libraries *) -val check_required_library : string list -> unit +(** This just prefixes find_reference with Coq... *) +val coq_reference : string -> string list -> string -> GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Search in several modules (not prefixed by "Coq") *) val gen_reference_in_modules : string->string list list-> string -> GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val arith_modules : string list list +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val zarith_base_modules : string list list +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val init_modules : string list list +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** {6 Global references } *) (** Modules *) -val prelude_module : DirPath.t - val logic_module : ModPath.t -val logic_module_name : string list +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val logic_type_module : DirPath.t - -val jmeq_module : ModPath.t -val jmeq_library_path : DirPath.t -val jmeq_module_name : string list - -val datatypes_module_name : string list +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Identity *) val id : Constant.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val type_of_id : Constant.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Natural numbers *) -val nat_path : full_path + +val nat_path : Libnames.full_path +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + val glob_nat : GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val path_of_O : constructor +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val path_of_S : constructor +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val glob_O : GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val glob_S : GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Booleans *) val glob_bool : GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] + val path_of_true : constructor +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val path_of_false : constructor +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val glob_true : GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val glob_false : GlobRef.t - +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Equality *) val glob_eq : GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val glob_identity : GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val glob_jmeq : GlobRef.t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** {6 ... } *) (** Constructions and patterns related to Coq initial state are unknown @@ -108,46 +180,24 @@ val glob_jmeq : GlobRef.t type coq_bool_data = { andb : GlobRef.t; andb_prop : GlobRef.t; - andb_true_intro : GlobRef.t} -val build_bool_type : coq_bool_data delayed - -(** {6 For Equality tactics } *) -type coq_sigma_data = { - proj1 : GlobRef.t; - proj2 : GlobRef.t; - elim : GlobRef.t; - intro : GlobRef.t; - typ : GlobRef.t } - -val build_sigma_set : coq_sigma_data delayed -val build_sigma_type : coq_sigma_data delayed -val build_sigma : coq_sigma_data delayed + andb_true_intro : GlobRef.t +} -(* val build_sigma_type_in : Environ.env -> coq_sigma_data Univ.in_universe_context_set *) -(* val build_sigma_in : Environ.env -> coq_sigma_data Univ.in_universe_context_set *) -(* val build_prod_in : Environ.env -> coq_sigma_data Univ.in_universe_context_set *) -(* val build_coq_eq_data_in : Environ.env -> coq_eq_data Univ.in_universe_context_set *) +val build_bool_type : coq_bool_data delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Non-dependent pairs in Set from Datatypes *) val build_prod : coq_sigma_data delayed - -type coq_eq_data = { - eq : GlobRef.t; - ind : GlobRef.t; - refl : GlobRef.t; - sym : GlobRef.t; - trans: GlobRef.t; - congr: GlobRef.t } - -val build_coq_eq_data : coq_eq_data delayed - -val build_coq_identity_data : coq_eq_data delayed -val build_coq_jmeq_data : coq_eq_data delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_eq : GlobRef.t delayed (** = [(build_coq_eq_data()).eq] *) +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_eq_refl : GlobRef.t delayed (** = [(build_coq_eq_data()).refl] *) +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_eq_sym : GlobRef.t delayed (** = [(build_coq_eq_data()).sym] *) +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_f_equal2 : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Data needed for discriminate and injection *) @@ -160,54 +210,85 @@ type coq_inversion_data = { } val build_coq_inversion_eq_data : coq_inversion_data delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_inversion_identity_data : coq_inversion_data delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_inversion_jmeq_data : coq_inversion_data delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_inversion_eq_true_data : coq_inversion_data delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Specif *) val build_coq_sumbool : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** {6 ... } *) (** Connectives The False proposition *) val build_coq_False : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** The True proposition and its unique proof *) val build_coq_True : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_I : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Negation *) val build_coq_not : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Conjunction *) val build_coq_and : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_conj : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_iff : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_iff_left_proj : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_iff_right_proj : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Pairs *) val build_coq_prod : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val build_coq_pair : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Disjunction *) val build_coq_or : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] (** Existential quantifier *) val build_coq_ex : GlobRef.t delayed +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_eq_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_identity_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_jmeq_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_eq_true_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_existS_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_existT_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_exist_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_not_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_False_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_sumbool_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_sig_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_or_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] val coq_iff_ref : GlobRef.t lazy_t +[@@ocaml.deprecated "Please use Coqlib.lib_ref"] diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v index d82e8ae8ad..4cde08872f 100644 --- a/plugins/btauto/Reflect.v +++ b/plugins/btauto/Reflect.v @@ -396,3 +396,16 @@ lazymatch goal with end | _ => fail "Cannot recognize a boolean equality" end. *) + +Register formula_var as plugins.btauto.f_var. +Register formula_btm as plugins.btauto.f_btm. +Register formula_top as plugins.btauto.f_top. +Register formula_cnj as plugins.btauto.f_cnj. +Register formula_dsj as plugins.btauto.f_dsj. +Register formula_neg as plugins.btauto.f_neg. +Register formula_xor as plugins.btauto.f_xor. +Register formula_ifb as plugins.btauto.f_ifb. + +Register formula_eval as plugins.btauto.eval. +Register boolean_witness as plugins.btauto.witness. +Register reduce_poly_of_formula_sound_alt as plugins.btauto.soundness. diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index b0f97c59b8..ac0a875229 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -12,17 +12,7 @@ open Constr let contrib_name = "btauto" -let init_constant dir s = - let find_constant contrib dir s = - UnivGen.constr_of_global (Coqlib.find_reference contrib dir s) - in - find_constant contrib_name dir s - -let get_constant dir s = lazy (UnivGen.constr_of_global @@ Coqlib.coq_reference contrib_name dir s) - -let get_inductive dir s = - let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in - Lazy.from_fun (fun () -> Globnames.destIndRef (glob_ref ())) +let bt_lib_constr n = lazy (UnivGen.constr_of_global @@ Coqlib.lib_ref n) let decomp_term sigma (c : Constr.t) = Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c))) @@ -31,11 +21,11 @@ let lapp c v = Constr.mkApp (Lazy.force c, v) let (===) = Constr.equal + module CoqList = struct - let path = ["Init"; "Datatypes"] - let typ = get_constant path "list" - let _nil = get_constant path "nil" - let _cons = get_constant path "cons" + let typ = bt_lib_constr "core.list.type" + let _nil = bt_lib_constr "core.list.nil" + let _cons = bt_lib_constr "core.list.cons" let cons ty h t = lapp _cons [|ty; h ; t|] let nil ty = lapp _nil [|ty|] @@ -47,11 +37,10 @@ module CoqList = struct end module CoqPositive = struct - let path = ["Numbers"; "BinNums"] - let typ = get_constant path "positive" - let _xH = get_constant path "xH" - let _xO = get_constant path "xO" - let _xI = get_constant path "xI" + let typ = bt_lib_constr "num.pos.type" + let _xH = bt_lib_constr "num.pos.xH" + let _xO = bt_lib_constr "num.pos.xO" + let _xI = bt_lib_constr "num.pos.xI" (* A coq nat from an int *) let rec of_int n = @@ -91,14 +80,14 @@ end module Bool = struct - let typ = get_constant ["Init"; "Datatypes"] "bool" - let ind = get_inductive ["Init"; "Datatypes"] "bool" - let trueb = get_constant ["Init"; "Datatypes"] "true" - let falseb = get_constant ["Init"; "Datatypes"] "false" - let andb = get_constant ["Init"; "Datatypes"] "andb" - let orb = get_constant ["Init"; "Datatypes"] "orb" - let xorb = get_constant ["Init"; "Datatypes"] "xorb" - let negb = get_constant ["Init"; "Datatypes"] "negb" + let ind = lazy (Globnames.destIndRef (Coqlib.lib_ref "core.bool.type")) + let typ = bt_lib_constr "core.bool.type" + let trueb = bt_lib_constr "core.bool.true" + let falseb = bt_lib_constr "core.bool.false" + let andb = bt_lib_constr "core.bool.andb" + let orb = bt_lib_constr "core.bool.orb" + let xorb = bt_lib_constr "core.bool.xorb" + let negb = bt_lib_constr "core.bool.negb" type t = | Var of int @@ -150,21 +139,20 @@ module Btauto = struct open Pp - let eq = get_constant ["Init"; "Logic"] "eq" - - let f_var = get_constant ["btauto"; "Reflect"] "formula_var" - let f_btm = get_constant ["btauto"; "Reflect"] "formula_btm" - let f_top = get_constant ["btauto"; "Reflect"] "formula_top" - let f_cnj = get_constant ["btauto"; "Reflect"] "formula_cnj" - let f_dsj = get_constant ["btauto"; "Reflect"] "formula_dsj" - let f_neg = get_constant ["btauto"; "Reflect"] "formula_neg" - let f_xor = get_constant ["btauto"; "Reflect"] "formula_xor" - let f_ifb = get_constant ["btauto"; "Reflect"] "formula_ifb" + let eq = bt_lib_constr "core.eq.type" - let eval = get_constant ["btauto"; "Reflect"] "formula_eval" - let witness = get_constant ["btauto"; "Reflect"] "boolean_witness" + let f_var = bt_lib_constr "plugins.btauto.f_var" + let f_btm = bt_lib_constr "plugins.btauto.f_btm" + let f_top = bt_lib_constr "plugins.btauto.f_top" + let f_cnj = bt_lib_constr "plugins.btauto.f_cnj" + let f_dsj = bt_lib_constr "plugins.btauto.f_dsj" + let f_neg = bt_lib_constr "plugins.btauto.f_neg" + let f_xor = bt_lib_constr "plugins.btauto.f_xor" + let f_ifb = bt_lib_constr "plugins.btauto.f_ifb" - let soundness = get_constant ["btauto"; "Reflect"] "reduce_poly_of_formula_sound_alt" + let eval = bt_lib_constr "plugins.btauto.eval" + let witness = bt_lib_constr "plugins.btauto.witness" + let soundness = bt_lib_constr "plugins.btauto.soundness" let rec convert = function | Bool.Var n -> lapp f_var [|CoqPositive.of_int n|] diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 2eaa6146e1..055d36747d 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -28,17 +28,13 @@ open Proofview.Notations module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -let reference dir s = lazy (Coqlib.coq_reference "CC" dir s) - -let _f_equal = reference ["Init";"Logic"] "f_equal" -let _eq_rect = reference ["Init";"Logic"] "eq_rect" -let _refl_equal = reference ["Init";"Logic"] "eq_refl" -let _sym_eq = reference ["Init";"Logic"] "eq_sym" -let _trans_eq = reference ["Init";"Logic"] "eq_trans" -let _eq = reference ["Init";"Logic"] "eq" -let _False = reference ["Init";"Logic"] "False" -let _True = reference ["Init";"Logic"] "True" -let _I = reference ["Init";"Logic"] "I" +let _f_equal = lazy (Coqlib.lib_ref "core.eq.congr") +let _eq_rect = lazy (Coqlib.lib_ref "core.eq.rect") +let _refl_equal = lazy (Coqlib.lib_ref "core.eq.refl") +let _sym_eq = lazy (Coqlib.lib_ref "core.eq.sym") +let _trans_eq = lazy (Coqlib.lib_ref "core.eq.trans") +let _eq = lazy (Coqlib.lib_ref "core.eq.type") +let _False = lazy (Coqlib.lib_ref "core.False.type") let whd env sigma t = Reductionops.clos_whd_flags CClosure.betaiotazeta env sigma t @@ -423,7 +419,7 @@ let build_term_to_complete uf pac = let cc_tactic depth additionnal_terms = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in - Coqlib.check_required_library Coqlib.logic_module_name; + Coqlib.(check_required_library logic_module_name); let _ = debug (fun () -> Pp.str "Reading subgoal ...") in let state = make_prb gl depth additionnal_terms in let _ = debug (fun () -> Pp.str "Problem built, solving ...") in diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 7e54bc8adb..fdeef5f0ac 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -109,11 +109,11 @@ let gen_ground_tac flag taco ids bases = (* special for compatibility with Intuition -let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str +let constant str = Coqlib.get_constr str let defined_connectives=lazy - [[],EvalConstRef (destConst (constant "not")); - [],EvalConstRef (destConst (constant "iff"))] + [[],EvalConstRef (destConst (constant "core.not.type")); + [],EvalConstRef (destConst (constant "core.iff.type"))] let normalize_evaluables= onAllHypsAndConcl diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 3ae777cc9a..8fa676de44 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -234,11 +234,11 @@ let ll_forall_tac prod backtrack id continue seq= (* special for compatibility with old Intuition *) let constant str = UnivGen.constr_of_global - @@ Coqlib.coq_reference "User" ["Init";"Logic"] str + @@ Coqlib.lib_ref str -let defined_connectives=lazy - [AllOccurrences,EvalConstRef (fst (Constr.destConst (constant "not"))); - AllOccurrences,EvalConstRef (fst (Constr.destConst (constant "iff")))] +let defined_connectives = lazy + [AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.not.type"))); + AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.iff.type")))] let normalize_evaluables= Proofview.Goal.enter begin fun gl -> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 5336948642..b12364d04a 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -414,9 +414,9 @@ let rewrite_until_var arg_num eq_ids : tactic = let rec_pte_id = Id.of_string "Hrec" let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = - let coq_False = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_False ()) in - let coq_True = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_True ()) in - let coq_I = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_I ()) in + let coq_False = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type") in + let coq_True = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.type") in + let coq_I = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I") in let rec scan_type context type_of_hyp : tactic = if isLetIn sigma type_of_hyp then let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in @@ -1605,7 +1605,7 @@ let prove_principle_for_gen match !tcc_lemma_ref with | Undefined -> user_err Pp.(str "No tcc proof !!") | Value lemma -> EConstr.of_constr lemma - | Not_needed -> EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_I ()) + | Not_needed -> EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I") in (* let rec list_diff del_list check_list = *) (* match del_list with *) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 0c45de4dc4..7c80b776a4 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -259,11 +259,8 @@ let mk_result ctxt value avoid = Some functions to deal with overlapping patterns **************************************************) -let coq_True_ref = - lazy (Coqlib.coq_reference "" ["Init";"Logic"] "True") - -let coq_False_ref = - lazy (Coqlib.coq_reference "" ["Init";"Logic"] "False") +let coq_True_ref = lazy (Coqlib.lib_ref "core.True.type") +let coq_False_ref = lazy (Coqlib.lib_ref "core.False.type") (* [make_discr_match_el \[e1,...en\]] builds match e1,...,en with @@ -957,7 +954,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = assert false end | GApp(eq_as_ref,[ty; id ;rt]) - when is_gvar id && is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous + when is_gvar id && is_gr eq_as_ref Coqlib.(lib_ref "core.eq.type") && n == Anonymous -> let loc1 = rt.CAst.loc in let loc2 = eq_as_ref.CAst.loc in @@ -1078,7 +1075,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = else new_b, Id.Set.add id id_to_exclude *) | GApp(eq_as_ref,[ty;rt1;rt2]) - when is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous + when is_gr eq_as_ref Coqlib.(lib_ref "core.eq.type") && n == Anonymous -> begin try @@ -1089,7 +1086,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = List.fold_left (fun acc (lhs,rhs) -> mkGProd(Anonymous, - mkGApp(mkGRef(Lazy.force Coqlib.coq_eq_ref),[mkGHole ();lhs;rhs]),acc) + mkGApp(mkGRef Coqlib.(lib_ref "core.eq.type"),[mkGHole ();lhs;rhs]),acc) ) b l diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index f81de82d5e..5b45a8dbed 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -38,11 +38,11 @@ let glob_decompose_app = (* [glob_make_eq t1 t2] build the glob_constr corresponding to [t2 = t1] *) let glob_make_eq ?(typ= mkGHole ()) t1 t2 = - mkGApp(mkGRef (Lazy.force Coqlib.coq_eq_ref),[typ;t2;t1]) + mkGApp(mkGRef (Coqlib.lib_ref "core.eq.type"),[typ;t2;t1]) (* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *) let glob_make_neq t1 t2 = - mkGApp(mkGRef (Lazy.force Coqlib.coq_not_ref),[glob_make_eq t1 t2]) + mkGApp(mkGRef (Coqlib.lib_ref "core.not.type"),[glob_make_eq t1 t2]) let remove_name_from_mapping mapping na = match na with diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 6ed382ca1c..03a64988e4 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -114,6 +114,7 @@ let def_of_const t = with Not_found -> assert false) |_ -> assert false +[@@@ocaml.warning "-3"] let coq_constant s = UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" @@ -441,7 +442,7 @@ let jmeq () = Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ UnivGen.constr_of_global @@ - Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq" + Coqlib.lib_ref "core.JMeq.type" with e when CErrors.noncritical e -> raise (ToShow e) let jmeq_refl () = @@ -449,7 +450,7 @@ let jmeq_refl () = Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ UnivGen.constr_of_global @@ - Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq_refl" + Coqlib.lib_ref "core.JMeq.refl" with e when CErrors.noncritical e -> raise (ToShow e) let h_intros l = @@ -461,8 +462,10 @@ let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded" let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc") let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv") +[@@@ocaml.warning "-3"] let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_global @@ - Coqlib.coq_reference "" ["Arith";"Wf_nat"] "well_founded_ltof" + Coqlib.find_reference "IndFun" ["Coq"; "Arith";"Wf_nat"] "well_founded_ltof" +[@@@ocaml.warning "+3"] let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof") diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 56fe430077..b8973a18dc 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -81,10 +81,9 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl let make_eq () = try - EConstr.of_constr (UnivGen.constr_of_global (Coqlib.build_coq_eq ())) - with _ -> assert false + EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref "core.eq.type")) + with _ -> assert false - (* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true] (resp. g_to_f = false) where [graph] is the graph of [f] and is the [i]th function in the block. @@ -512,7 +511,7 @@ and intros_with_rewrite_aux : Tacmach.tactic = intros_with_rewrite ] g end - | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_False ())) -> + | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type")) -> Proofview.V82.of_tactic tauto g | Case(_,_,v,_) -> tclTHENLIST[ diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 633d98a585..89dfb58017 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -49,11 +49,12 @@ open Context.Rel.Declaration (* Ugly things which should not be here *) +[@@@ocaml.warning "-3"] let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_global @@ - Coqlib.coq_reference "RecursiveDefinition" m s + Coqlib.find_reference "RecursiveDefinition" m s -let arith_Nat = ["Arith";"PeanoNat";"Nat"] -let arith_Lt = ["Arith";"Lt"] +let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"] +let arith_Lt = ["Coq"; "Arith";"Lt"] let pr_leconstr_rd = let sigma, env = Pfedit.get_current_context () in @@ -63,6 +64,7 @@ let coq_init_constant s = EConstr.of_constr ( UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) +[@@@ocaml.warning "+3"] let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in @@ -143,6 +145,7 @@ let def_id = Id.of_string "def" let p_id = Id.of_string "p" let rec_res_id = Id.of_string "rec_res";; let lt = function () -> (coq_init_constant "lt") +[@@@ocaml.warning "-3"] let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le") let ex = function () -> (coq_init_constant "ex") let nat = function () -> (coq_init_constant "nat") @@ -163,7 +166,6 @@ let coq_S = function () -> (coq_init_constant "S") let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r") let max_ref = function () -> (find_reference ["Recdef"] "max") let max_constr = function () -> EConstr.of_constr (constr_of_global (delayed_force max_ref)) -let coq_conj = function () -> find_reference Coqlib.logic_module_name "conj" let f_S t = mkApp(delayed_force coq_S, [|t|]);; @@ -1241,8 +1243,8 @@ let get_current_subgoals_types () = exception EmptySubgoals let build_and_l sigma l = - let and_constr = UnivGen.constr_of_global @@ Coqlib.build_coq_and () in - let conj_constr = coq_conj () in + let and_constr = UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type" in + let conj_constr = Coqlib.build_coq_conj () in let mk_and p1 p2 = mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in let rec is_well_founded t = 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) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index ec080edbdb..402e8b91e6 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -357,6 +357,8 @@ struct ["Coq";"Reals" ; "Rpow_def"]; ["LRing_normalise"]] +[@@@ocaml.warning "-3"] + let coq_modules = Coqlib.(init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules @ mic_modules) @@ -379,6 +381,8 @@ struct let gen_constant_in_modules s m n = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules s m n) let init_constant = gen_constant_in_modules "ZMicromega" Coqlib.init_modules + [@@@ocaml.warning "+3"] + let constant = gen_constant_in_modules "ZMicromega" coq_modules let bin_constant = gen_constant_in_modules "ZMicromega" bin_module let r_constant = gen_constant_in_modules "ZMicromega" r_modules diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index d2d4639d2b..11d0a4a44d 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -12,7 +12,6 @@ open CErrors open Util open Constr open Tactics -open Coqlib open Num open Utile @@ -136,36 +135,32 @@ let mul = function | (Const n,q) when eq_num n num_1 -> q | (p,q) -> Mul(p,q) -let gen_constant msg path s = UnivGen.constr_of_global @@ - coq_reference msg path s +let gen_constant n = lazy (UnivGen.constr_of_global (Coqlib.lib_ref n)) -let tpexpr = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PExpr") -let ttconst = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEc") -let ttvar = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEX") -let ttadd = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEadd") -let ttsub = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEsub") -let ttmul = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEmul") -let ttopp = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEopp") -let ttpow = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEpow") +let tpexpr = gen_constant "plugins.setoid_ring.pexpr" +let ttconst = gen_constant "plugins.setoid_ring.const" +let ttvar = gen_constant "plugins.setoid_ring.var" +let ttadd = gen_constant "plugins.setoid_ring.add" +let ttsub = gen_constant "plugins.setoid_ring.sub" +let ttmul = gen_constant "plugins.setoid_ring.mul" +let ttopp = gen_constant "plugins.setoid_ring.opp" +let ttpow = gen_constant "plugins.setoid_ring.pow" -let datatypes = ["Init";"Datatypes"] -let binnums = ["Numbers";"BinNums"] +let tlist = gen_constant "core.list.type" +let lnil = gen_constant "core.list.nil" +let lcons = gen_constant "core.list.cons" -let tlist = lazy (gen_constant "CC" datatypes "list") -let lnil = lazy (gen_constant "CC" datatypes "nil") -let lcons = lazy (gen_constant "CC" datatypes "cons") +let tz = gen_constant "num.Z.type" +let z0 = gen_constant "num.Z.Z0" +let zpos = gen_constant "num.Z.Zpos" +let zneg = gen_constant "num.Z.Zneg" -let tz = lazy (gen_constant "CC" binnums "Z") -let z0 = lazy (gen_constant "CC" binnums "Z0") -let zpos = lazy (gen_constant "CC" binnums "Zpos") -let zneg = lazy(gen_constant "CC" binnums "Zneg") +let pxI = gen_constant "num.pos.xI" +let pxO = gen_constant "num.pos.xO" +let pxH = gen_constant "num.pos.xH" -let pxI = lazy(gen_constant "CC" binnums "xI") -let pxO = lazy(gen_constant "CC" binnums "xO") -let pxH = lazy(gen_constant "CC" binnums "xH") - -let nN0 = lazy (gen_constant "CC" binnums "N0") -let nNpos = lazy(gen_constant "CC" binnums "Npos") +let nN0 = gen_constant "num.N.N0" +let nNpos = gen_constant "num.N.Npos" let mkt_app name l = mkApp (Lazy.force name, Array.of_list l) @@ -545,7 +540,7 @@ let nsatz lpol = let return_term t = let a = - mkApp(gen_constant "CC" ["Init";"Logic"] "eq_refl",[|tllp ();t|]) in + mkApp (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.eq.refl",[|tllp ();t|]) in let a = EConstr.of_constr a in generalize [a] diff --git a/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v index dc86a98998..9593e1225c 100644 --- a/plugins/omega/OmegaLemmas.v +++ b/plugins/omega/OmegaLemmas.v @@ -267,3 +267,49 @@ Proof. intros n; exists (Z.of_nat n); split; trivial. rewrite Z.mul_1_r, Z.add_0_r. apply Nat2Z.is_nonneg. Qed. + +Register fast_Zplus_assoc_reverse as plugins.omega.fast_Zplus_assoc_reverse. +Register fast_Zplus_assoc as plugins.omega.fast_Zplus_assoc. +Register fast_Zmult_assoc_reverse as plugins.omega.fast_Zmult_assoc_reverse. +Register fast_Zplus_permute as plugins.omega.fast_Zplus_permute. +Register fast_Zplus_comm as plugins.omega.fast_Zplus_comm. +Register fast_Zmult_comm as plugins.omega.fast_Zmult_comm. + +Register OMEGA1 as plugins.omega.OMEGA1. +Register OMEGA2 as plugins.omega.OMEGA2. +Register OMEGA3 as plugins.omega.OMEGA3. +Register OMEGA4 as plugins.omega.OMEGA4. +Register OMEGA5 as plugins.omega.OMEGA5. +Register OMEGA6 as plugins.omega.OMEGA6. +Register OMEGA7 as plugins.omega.OMEGA7. +Register OMEGA8 as plugins.omega.OMEGA8. +Register OMEGA9 as plugins.omega.OMEGA9. +Register fast_OMEGA10 as plugins.omega.fast_OMEGA10. +Register fast_OMEGA11 as plugins.omega.fast_OMEGA11. +Register fast_OMEGA12 as plugins.omega.fast_OMEGA12. +Register fast_OMEGA13 as plugins.omega.fast_OMEGA13. +Register fast_OMEGA14 as plugins.omega.fast_OMEGA14. +Register fast_OMEGA15 as plugins.omega.fast_OMEGA15. +Register fast_OMEGA16 as plugins.omega.fast_OMEGA16. +Register OMEGA17 as plugins.omega.OMEGA17. +Register OMEGA18 as plugins.omega.OMEGA18. +Register OMEGA19 as plugins.omega.OMEGA19. +Register OMEGA20 as plugins.omega.OMEGA20. + +Register fast_Zred_factor0 as plugins.omega.fast_Zred_factor0. +Register fast_Zred_factor1 as plugins.omega.fast_Zred_factor1. +Register fast_Zred_factor2 as plugins.omega.fast_Zred_factor2. +Register fast_Zred_factor3 as plugins.omega.fast_Zred_factor3. +Register fast_Zred_factor4 as plugins.omega.fast_Zred_factor4. +Register fast_Zred_factor5 as plugins.omega.fast_Zred_factor5. +Register fast_Zred_factor6 as plugins.omega.fast_Zred_factor6. + +Register fast_Zmult_plus_distr_l as plugins.omega.fast_Zmult_plus_distr_l. +Register fast_Zmult_opp_comm as plugins.omega.fast_Zmult_opp_comm. +Register fast_Zopp_plus_distr as plugins.omega.fast_Zopp_plus_distr. +Register fast_Zopp_mult_distr_r as plugins.omega.fast_Zopp_mult_distr_r. +Register fast_Zopp_eq_mult_neg_1 as plugins.omega.fast_Zopp_eq_mult_neg_1. +Register fast_Zopp_involutive as plugins.omega.fast_Zopp_involutive. + +Register new_var as plugins.omega.new_var. +Register intro_Z as plugins.omega.intro_Z. diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index abae6940fa..f55458de8d 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -193,172 +193,159 @@ let reset_all () = To use the constant Zplus, one must type "Lazy.force coq_Zplus" This is the right way to access to Coq constants in tactics ML code *) -open Coqlib - -let logic_dir = ["Coq";"Logic";"Decidable"] -let coq_modules = - init_modules @arith_modules @ [logic_dir] @ zarith_base_modules - @ [["Coq"; "omega"; "OmegaLemmas"]] - -let gen_constant_in_modules n m s = EConstr.of_constr (UnivGen.constr_of_global @@ gen_reference_in_modules n m s) -let init_constant = gen_constant_in_modules "Omega" init_modules -let constant = gen_constant_in_modules "Omega" coq_modules - -let z_constant = gen_constant_in_modules "Omega" [["Coq";"ZArith"]] -let zbase_constant = - gen_constant_in_modules "Omega" [["Coq";"ZArith";"BinInt"]] +let gen_constant k = lazy (k |> Coqlib.lib_ref |> UnivGen.constr_of_global |> EConstr.of_constr) (* Zarith *) -let coq_xH = lazy (constant "xH") -let coq_xO = lazy (constant "xO") -let coq_xI = lazy (constant "xI") -let coq_Z0 = lazy (constant "Z0") -let coq_Zpos = lazy (constant "Zpos") -let coq_Zneg = lazy (constant "Zneg") -let coq_Z = lazy (constant "Z") -let coq_comparison = lazy (constant "comparison") -let coq_Gt = lazy (constant "Gt") -let coq_Zplus = lazy (zbase_constant "Z.add") -let coq_Zmult = lazy (zbase_constant "Z.mul") -let coq_Zopp = lazy (zbase_constant "Z.opp") -let coq_Zminus = lazy (zbase_constant "Z.sub") -let coq_Zsucc = lazy (zbase_constant "Z.succ") -let coq_Zpred = lazy (zbase_constant "Z.pred") -let coq_Z_of_nat = lazy (zbase_constant "Z.of_nat") -let coq_inj_plus = lazy (z_constant "Nat2Z.inj_add") -let coq_inj_mult = lazy (z_constant "Nat2Z.inj_mul") -let coq_inj_minus1 = lazy (z_constant "Nat2Z.inj_sub") -let coq_inj_minus2 = lazy (constant "inj_minus2") -let coq_inj_S = lazy (z_constant "Nat2Z.inj_succ") -let coq_inj_le = lazy (z_constant "Znat.inj_le") -let coq_inj_lt = lazy (z_constant "Znat.inj_lt") -let coq_inj_ge = lazy (z_constant "Znat.inj_ge") -let coq_inj_gt = lazy (z_constant "Znat.inj_gt") -let coq_inj_neq = lazy (z_constant "inj_neq") -let coq_inj_eq = lazy (z_constant "inj_eq") -let coq_fast_Zplus_assoc_reverse = lazy (constant "fast_Zplus_assoc_reverse") -let coq_fast_Zplus_assoc = lazy (constant "fast_Zplus_assoc") -let coq_fast_Zmult_assoc_reverse = lazy (constant "fast_Zmult_assoc_reverse") -let coq_fast_Zplus_permute = lazy (constant "fast_Zplus_permute") -let coq_fast_Zplus_comm = lazy (constant "fast_Zplus_comm") -let coq_fast_Zmult_comm = lazy (constant "fast_Zmult_comm") -let coq_Zmult_le_approx = lazy (constant "Zmult_le_approx") -let coq_OMEGA1 = lazy (constant "OMEGA1") -let coq_OMEGA2 = lazy (constant "OMEGA2") -let coq_OMEGA3 = lazy (constant "OMEGA3") -let coq_OMEGA4 = lazy (constant "OMEGA4") -let coq_OMEGA5 = lazy (constant "OMEGA5") -let coq_OMEGA6 = lazy (constant "OMEGA6") -let coq_OMEGA7 = lazy (constant "OMEGA7") -let coq_OMEGA8 = lazy (constant "OMEGA8") -let coq_OMEGA9 = lazy (constant "OMEGA9") -let coq_fast_OMEGA10 = lazy (constant "fast_OMEGA10") -let coq_fast_OMEGA11 = lazy (constant "fast_OMEGA11") -let coq_fast_OMEGA12 = lazy (constant "fast_OMEGA12") -let coq_fast_OMEGA13 = lazy (constant "fast_OMEGA13") -let coq_fast_OMEGA14 = lazy (constant "fast_OMEGA14") -let coq_fast_OMEGA15 = lazy (constant "fast_OMEGA15") -let coq_fast_OMEGA16 = lazy (constant "fast_OMEGA16") -let coq_OMEGA17 = lazy (constant "OMEGA17") -let coq_OMEGA18 = lazy (constant "OMEGA18") -let coq_OMEGA19 = lazy (constant "OMEGA19") -let coq_OMEGA20 = lazy (constant "OMEGA20") -let coq_fast_Zred_factor0 = lazy (constant "fast_Zred_factor0") -let coq_fast_Zred_factor1 = lazy (constant "fast_Zred_factor1") -let coq_fast_Zred_factor2 = lazy (constant "fast_Zred_factor2") -let coq_fast_Zred_factor3 = lazy (constant "fast_Zred_factor3") -let coq_fast_Zred_factor4 = lazy (constant "fast_Zred_factor4") -let coq_fast_Zred_factor5 = lazy (constant "fast_Zred_factor5") -let coq_fast_Zred_factor6 = lazy (constant "fast_Zred_factor6") -let coq_fast_Zmult_plus_distr_l = lazy (constant "fast_Zmult_plus_distr_l") -let coq_fast_Zmult_opp_comm = lazy (constant "fast_Zmult_opp_comm") -let coq_fast_Zopp_plus_distr = lazy (constant "fast_Zopp_plus_distr") -let coq_fast_Zopp_mult_distr_r = lazy (constant "fast_Zopp_mult_distr_r") -let coq_fast_Zopp_eq_mult_neg_1 = lazy (constant "fast_Zopp_eq_mult_neg_1") -let coq_fast_Zopp_involutive = lazy (constant "fast_Zopp_involutive") -let coq_Zegal_left = lazy (constant "Zegal_left") -let coq_Zne_left = lazy (constant "Zne_left") -let coq_Zlt_left = lazy (constant "Zlt_left") -let coq_Zge_left = lazy (constant "Zge_left") -let coq_Zgt_left = lazy (constant "Zgt_left") -let coq_Zle_left = lazy (constant "Zle_left") -let coq_new_var = lazy (constant "new_var") -let coq_intro_Z = lazy (constant "intro_Z") - -let coq_dec_eq = lazy (zbase_constant "Z.eq_decidable") -let coq_dec_Zne = lazy (constant "dec_Zne") -let coq_dec_Zle = lazy (zbase_constant "Z.le_decidable") -let coq_dec_Zlt = lazy (zbase_constant "Z.lt_decidable") -let coq_dec_Zgt = lazy (constant "dec_Zgt") -let coq_dec_Zge = lazy (constant "dec_Zge") - -let coq_not_Zeq = lazy (constant "not_Zeq") -let coq_not_Zne = lazy (constant "not_Zne") -let coq_Znot_le_gt = lazy (constant "Znot_le_gt") -let coq_Znot_lt_ge = lazy (constant "Znot_lt_ge") -let coq_Znot_ge_lt = lazy (constant "Znot_ge_lt") -let coq_Znot_gt_le = lazy (constant "Znot_gt_le") -let coq_neq = lazy (constant "neq") -let coq_Zne = lazy (constant "Zne") -let coq_Zle = lazy (zbase_constant "Z.le") -let coq_Zgt = lazy (zbase_constant "Z.gt") -let coq_Zge = lazy (zbase_constant "Z.ge") -let coq_Zlt = lazy (zbase_constant "Z.lt") +let coq_xH = gen_constant "num.pos.xH" +let coq_xO = gen_constant "num.pos.xO" +let coq_xI = gen_constant "num.pos.xI" +let coq_Z0 = gen_constant "num.Z.Z0" +let coq_Zpos = gen_constant "num.Z.Zpos" +let coq_Zneg = gen_constant "num.Z.Zneg" +let coq_Z = gen_constant "num.Z.type" +let coq_comparison = gen_constant "core.comparison.type" +let coq_Gt = gen_constant "core.comparison.Gt" +let coq_Zplus = gen_constant "num.Z.add" +let coq_Zmult = gen_constant "num.Z.mul" +let coq_Zopp = gen_constant "num.Z.opp" +let coq_Zminus = gen_constant "num.Z.sub" +let coq_Zsucc = gen_constant "num.Z.succ" +let coq_Zpred = gen_constant "num.Z.pred" +let coq_Z_of_nat = gen_constant "num.Z.of_nat" +let coq_inj_plus = gen_constant "num.Nat2Z.inj_add" +let coq_inj_mult = gen_constant "num.Nat2Z.inj_mul" +let coq_inj_minus1 = gen_constant "num.Nat2Z.inj_sub" +let coq_inj_minus2 = gen_constant "plugins.omega.inj_minus2" +let coq_inj_S = gen_constant "num.Nat2Z.inj_succ" +let coq_inj_eq = gen_constant "plugins.omega.inj_eq" +let coq_inj_neq = gen_constant "plugins.omega.inj_neq" +let coq_inj_le = gen_constant "plugins.omega.inj_le" +let coq_inj_lt = gen_constant "plugins.omega.inj_lt" +let coq_inj_ge = gen_constant "plugins.omega.inj_ge" +let coq_inj_gt = gen_constant "plugins.omega.inj_gt" +let coq_fast_Zplus_assoc_reverse = gen_constant "plugins.omega.fast_Zplus_assoc_reverse" +let coq_fast_Zplus_assoc = gen_constant "plugins.omega.fast_Zplus_assoc" +let coq_fast_Zmult_assoc_reverse = gen_constant "plugins.omega.fast_Zmult_assoc_reverse" +let coq_fast_Zplus_permute = gen_constant "plugins.omega.fast_Zplus_permute" +let coq_fast_Zplus_comm = gen_constant "plugins.omega.fast_Zplus_comm" +let coq_fast_Zmult_comm = gen_constant "plugins.omega.fast_Zmult_comm" +let coq_Zmult_le_approx = gen_constant "plugins.omega.Zmult_le_approx" +let coq_OMEGA1 = gen_constant "plugins.omega.OMEGA1" +let coq_OMEGA2 = gen_constant "plugins.omega.OMEGA2" +let coq_OMEGA3 = gen_constant "plugins.omega.OMEGA3" +let coq_OMEGA4 = gen_constant "plugins.omega.OMEGA4" +let coq_OMEGA5 = gen_constant "plugins.omega.OMEGA5" +let coq_OMEGA6 = gen_constant "plugins.omega.OMEGA6" +let coq_OMEGA7 = gen_constant "plugins.omega.OMEGA7" +let coq_OMEGA8 = gen_constant "plugins.omega.OMEGA8" +let coq_OMEGA9 = gen_constant "plugins.omega.OMEGA9" +let coq_fast_OMEGA10 = gen_constant "plugins.omega.fast_OMEGA10" +let coq_fast_OMEGA11 = gen_constant "plugins.omega.fast_OMEGA11" +let coq_fast_OMEGA12 = gen_constant "plugins.omega.fast_OMEGA12" +let coq_fast_OMEGA13 = gen_constant "plugins.omega.fast_OMEGA13" +let coq_fast_OMEGA14 = gen_constant "plugins.omega.fast_OMEGA14" +let coq_fast_OMEGA15 = gen_constant "plugins.omega.fast_OMEGA15" +let coq_fast_OMEGA16 = gen_constant "plugins.omega.fast_OMEGA16" +let coq_OMEGA17 = gen_constant "plugins.omega.OMEGA17" +let coq_OMEGA18 = gen_constant "plugins.omega.OMEGA18" +let coq_OMEGA19 = gen_constant "plugins.omega.OMEGA19" +let coq_OMEGA20 = gen_constant "plugins.omega.OMEGA20" +let coq_fast_Zred_factor0 = gen_constant "plugins.omega.fast_Zred_factor0" +let coq_fast_Zred_factor1 = gen_constant "plugins.omega.fast_Zred_factor1" +let coq_fast_Zred_factor2 = gen_constant "plugins.omega.fast_Zred_factor2" +let coq_fast_Zred_factor3 = gen_constant "plugins.omega.fast_Zred_factor3" +let coq_fast_Zred_factor4 = gen_constant "plugins.omega.fast_Zred_factor4" +let coq_fast_Zred_factor5 = gen_constant "plugins.omega.fast_Zred_factor5" +let coq_fast_Zred_factor6 = gen_constant "plugins.omega.fast_Zred_factor6" +let coq_fast_Zmult_plus_distr_l = gen_constant "plugins.omega.fast_Zmult_plus_distr_l" +let coq_fast_Zmult_opp_comm = gen_constant "plugins.omega.fast_Zmult_opp_comm" +let coq_fast_Zopp_plus_distr = gen_constant "plugins.omega.fast_Zopp_plus_distr" +let coq_fast_Zopp_mult_distr_r = gen_constant "plugins.omega.fast_Zopp_mult_distr_r" +let coq_fast_Zopp_eq_mult_neg_1 = gen_constant "plugins.omega.fast_Zopp_eq_mult_neg_1" +let coq_fast_Zopp_involutive = gen_constant "plugins.omega.fast_Zopp_involutive" +let coq_Zegal_left = gen_constant "plugins.omega.Zegal_left" +let coq_Zne_left = gen_constant "plugins.omega.Zne_left" +let coq_Zlt_left = gen_constant "plugins.omega.Zlt_left" +let coq_Zge_left = gen_constant "plugins.omega.Zge_left" +let coq_Zgt_left = gen_constant "plugins.omega.Zgt_left" +let coq_Zle_left = gen_constant "plugins.omega.Zle_left" +let coq_new_var = gen_constant "plugins.omega.new_var" +let coq_intro_Z = gen_constant "plugins.omega.intro_Z" + +let coq_dec_eq = gen_constant "num.Z.eq_decidable" +let coq_dec_Zne = gen_constant "plugins.omega.dec_Zne" +let coq_dec_Zle = gen_constant "num.Z.le_decidable" +let coq_dec_Zlt = gen_constant "num.Z.lt_decidable" +let coq_dec_Zgt = gen_constant "plugins.omega.dec_Zgt" +let coq_dec_Zge = gen_constant "plugins.omega.dec_Zge" + +let coq_not_Zeq = gen_constant "plugins.omega.not_Zeq" +let coq_not_Zne = gen_constant "plugins.omega.not_Zne" +let coq_Znot_le_gt = gen_constant "plugins.omega.Znot_le_gt" +let coq_Znot_lt_ge = gen_constant "plugins.omega.Znot_lt_ge" +let coq_Znot_ge_lt = gen_constant "plugins.omega.Znot_ge_lt" +let coq_Znot_gt_le = gen_constant "plugins.omega.Znot_gt_le" +let coq_neq = gen_constant "plugins.omega.neq" +let coq_Zne = gen_constant "plugins.omega.Zne" +let coq_Zle = gen_constant "num.Z.le" +let coq_Zlt = gen_constant "num.Z.lt" +let coq_Zge = gen_constant "num.Z.ge" +let coq_Zgt = gen_constant "num.Z.gt" (* Peano/Datatypes *) -let coq_le = lazy (init_constant "le") -let coq_lt = lazy (init_constant "lt") -let coq_ge = lazy (init_constant "ge") -let coq_gt = lazy (init_constant "gt") -let coq_minus = lazy (init_constant "Nat.sub") -let coq_plus = lazy (init_constant "Nat.add") -let coq_mult = lazy (init_constant "Nat.mul") -let coq_pred = lazy (init_constant "Nat.pred") -let coq_nat = lazy (init_constant "nat") -let coq_S = lazy (init_constant "S") -let coq_O = lazy (init_constant "O") +let coq_nat = gen_constant "num.nat.type" +let coq_O = gen_constant "num.nat.O" +let coq_S = gen_constant "num.nat.S" +let coq_le = gen_constant "num.nat.le" +let coq_lt = gen_constant "num.nat.lt" +let coq_ge = gen_constant "num.nat.ge" +let coq_gt = gen_constant "num.nat.gt" +let coq_plus = gen_constant "num.nat.add" +let coq_minus = gen_constant "num.nat.sub" +let coq_mult = gen_constant "num.nat.mul" +let coq_pred = gen_constant "num.nat.pred" (* Compare_dec/Peano_dec/Minus *) -let coq_pred_of_minus = lazy (constant "pred_of_minus") -let coq_le_gt_dec = lazy (constant "le_gt_dec") -let coq_dec_eq_nat = lazy (constant "dec_eq_nat") -let coq_dec_le = lazy (constant "dec_le") -let coq_dec_lt = lazy (constant "dec_lt") -let coq_dec_ge = lazy (constant "dec_ge") -let coq_dec_gt = lazy (constant "dec_gt") -let coq_not_eq = lazy (constant "not_eq") -let coq_not_le = lazy (constant "not_le") -let coq_not_lt = lazy (constant "not_lt") -let coq_not_ge = lazy (constant "not_ge") -let coq_not_gt = lazy (constant "not_gt") +let coq_pred_of_minus = gen_constant "num.nat.pred_of_minus" +let coq_le_gt_dec = gen_constant "num.nat.le_gt_dec" +let coq_dec_eq_nat = gen_constant "num.nat.eq_dec" +let coq_dec_le = gen_constant "num.nat.dec_le" +let coq_dec_lt = gen_constant "num.nat.dec_lt" +let coq_dec_ge = gen_constant "num.nat.dec_ge" +let coq_dec_gt = gen_constant "num.nat.dec_gt" +let coq_not_eq = gen_constant "num.nat.not_eq" +let coq_not_le = gen_constant "num.nat.not_le" +let coq_not_lt = gen_constant "num.nat.not_lt" +let coq_not_ge = gen_constant "num.nat.not_ge" +let coq_not_gt = gen_constant "num.nat.not_gt" (* Logic/Decidable *) -let coq_eq_ind_r = lazy (constant "eq_ind_r") - -let coq_dec_or = lazy (constant "dec_or") -let coq_dec_and = lazy (constant "dec_and") -let coq_dec_imp = lazy (constant "dec_imp") -let coq_dec_iff = lazy (constant "dec_iff") -let coq_dec_not = lazy (constant "dec_not") -let coq_dec_False = lazy (constant "dec_False") -let coq_dec_not_not = lazy (constant "dec_not_not") -let coq_dec_True = lazy (constant "dec_True") - -let coq_not_or = lazy (constant "not_or") -let coq_not_and = lazy (constant "not_and") -let coq_not_imp = lazy (constant "not_imp") -let coq_not_iff = lazy (constant "not_iff") -let coq_not_not = lazy (constant "not_not") -let coq_imp_simp = lazy (constant "imp_simp") -let coq_iff = lazy (constant "iff") -let coq_not = lazy (init_constant "not") -let coq_and = lazy (init_constant "and") -let coq_or = lazy (init_constant "or") -let coq_eq = lazy (init_constant "eq") -let coq_ex = lazy (init_constant "ex") -let coq_False = lazy (init_constant "False") -let coq_True = lazy (init_constant "True") +let coq_eq_ind_r = gen_constant "core.eq.ind_r" + +let coq_dec_or = gen_constant "core.dec.or" +let coq_dec_and = gen_constant "core.dec.and" +let coq_dec_imp = gen_constant "core.dec.imp" +let coq_dec_iff = gen_constant "core.dec.iff" +let coq_dec_not = gen_constant "core.dec.not" +let coq_dec_False = gen_constant "core.dec.False" +let coq_dec_not_not = gen_constant "core.dec.not_not" +let coq_dec_True = gen_constant "core.dec.True" + +let coq_not_or = gen_constant "core.dec.not_or" +let coq_not_and = gen_constant "core.dec.not_and" +let coq_not_imp = gen_constant "core.dec.not_imp" +let coq_not_iff = gen_constant "core.dec.not_iff" +let coq_not_not = gen_constant "core.dec.dec_not_not" +let coq_imp_simp = gen_constant "core.dec.imp_simp" +let coq_iff = gen_constant "core.iff.type" +let coq_not = gen_constant "core.not.type" +let coq_and = gen_constant "core.and.type" +let coq_or = gen_constant "core.or.type" +let coq_eq = gen_constant "core.eq.type" +let coq_ex = gen_constant "core.ex.type" +let coq_False = gen_constant "core.False.type" +let coq_True = gen_constant "core.True.type" (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *) diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index 600e8993b4..99c02995fb 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -319,6 +319,9 @@ Arguments F_empty [A]. Arguments F_push [A] a S _. Arguments In [A] x S F. +Register empty as plugins.rtauto.empty. +Register push as plugins.rtauto.push. + Section Map. Variables A B:Set. diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v index 06cdf76b4e..f027a4a46e 100644 --- a/plugins/rtauto/Rtauto.v +++ b/plugins/rtauto/Rtauto.v @@ -387,3 +387,24 @@ exact (Reflect (empty \ A \ B \ C) Qed. Print toto. *) + +Register Reflect as plugins.rtauto.Reflect. + +Register Atom as plugins.rtauto.Atom. +Register Arrow as plugins.rtauto.Arrow. +Register Bot as plugins.rtauto.Bot. +Register Conjunct as plugins.rtauto.Conjunct. +Register Disjunct as plugins.rtauto.Disjunct. + +Register Ax as plugins.rtauto.Ax. +Register I_Arrow as plugins.rtauto.I_Arrow. +Register E_Arrow as plugins.rtauto.E_Arrow. +Register D_Arrow as plugins.rtauto.D_Arrow. +Register E_False as plugins.rtauto.E_False. +Register I_And as plugins.rtauto.I_And. +Register E_And as plugins.rtauto.E_And. +Register D_And as plugins.rtauto.D_And. +Register I_Or_l as plugins.rtauto.I_Or_l. +Register I_Or_r as plugins.rtauto.I_Or_r. +Register E_Or as plugins.rtauto.E_Or. +Register D_Or as plugins.rtauto.D_Or. diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 8a0f48dc4d..79418da27c 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -26,49 +26,39 @@ let step_count = ref 0 let node_count = ref 0 -let logic_constant s = UnivGen.constr_of_global @@ - Coqlib.coq_reference "refl_tauto" ["Init";"Logic"] s - -let li_False = lazy (destInd (logic_constant "False")) -let li_and = lazy (destInd (logic_constant "and")) -let li_or = lazy (destInd (logic_constant "or")) - -let pos_constant s = UnivGen.constr_of_global @@ - Coqlib.coq_reference "refl_tauto" ["Numbers";"BinNums"] s - -let l_xI = lazy (pos_constant "xI") -let l_xO = lazy (pos_constant "xO") -let l_xH = lazy (pos_constant "xH") - -let store_constant s = UnivGen.constr_of_global @@ - Coqlib.coq_reference "refl_tauto" ["rtauto";"Bintree"] s - -let l_empty = lazy (store_constant "empty") -let l_push = lazy (store_constant "push") - -let constant s = UnivGen.constr_of_global @@ - Coqlib.coq_reference "refl_tauto" ["rtauto";"Rtauto"] s - -let l_Reflect = lazy (constant "Reflect") - -let l_Atom = lazy (constant "Atom") -let l_Arrow = lazy (constant "Arrow") -let l_Bot = lazy (constant "Bot") -let l_Conjunct = lazy (constant "Conjunct") -let l_Disjunct = lazy (constant "Disjunct") - -let l_Ax = lazy (constant "Ax") -let l_I_Arrow = lazy (constant "I_Arrow") -let l_E_Arrow = lazy (constant "E_Arrow") -let l_D_Arrow = lazy (constant "D_Arrow") -let l_E_False = lazy (constant "E_False") -let l_I_And = lazy (constant "I_And") -let l_E_And = lazy (constant "E_And") -let l_D_And = lazy (constant "D_And") -let l_I_Or_l = lazy (constant "I_Or_l") -let l_I_Or_r = lazy (constant "I_Or_r") -let l_E_Or = lazy (constant "E_Or") -let l_D_Or = lazy (constant "D_Or") +let li_False = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type")) +let li_and = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type")) +let li_or = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.or.type")) + +let gen_constant n = lazy (UnivGen.constr_of_global (Coqlib.lib_ref n)) + +let l_xI = gen_constant "num.pos.xI" +let l_xO = gen_constant "num.pos.xO" +let l_xH = gen_constant "num.pos.xH" + +let l_empty = gen_constant "plugins.rtauto.empty" +let l_push = gen_constant "plugins.rtauto.push" + +let l_Reflect = gen_constant "plugins.rtauto.Reflect" + +let l_Atom = gen_constant "plugins.rtauto.Atom" +let l_Arrow = gen_constant "plugins.rtauto.Arrow" +let l_Bot = gen_constant "plugins.rtauto.Bot" +let l_Conjunct = gen_constant "plugins.rtauto.Conjunct" +let l_Disjunct = gen_constant "plugins.rtauto.Disjunct" + +let l_Ax = gen_constant "plugins.rtauto.Ax" +let l_I_Arrow = gen_constant "plugins.rtauto.I_Arrow" +let l_E_Arrow = gen_constant "plugins.rtauto.E_Arrow" +let l_D_Arrow = gen_constant "plugins.rtauto.D_Arrow" +let l_E_False = gen_constant "plugins.rtauto.E_False" +let l_I_And = gen_constant "plugins.rtauto.I_And" +let l_E_And = gen_constant "plugins.rtauto.E_And" +let l_D_And = gen_constant "plugins.rtauto.D_And" +let l_I_Or_l = gen_constant "plugins.rtauto.I_Or_l" +let l_I_Or_r = gen_constant "plugins.rtauto.I_Or_r" +let l_E_Or = gen_constant "plugins.rtauto.E_Or" +let l_D_Or = gen_constant "plugins.rtauto.D_Or" let special_whd gl c = diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index 33df36d847..ccd82eabcd 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -919,6 +919,14 @@ Section MakeRingPol. | PEopp : PExpr -> PExpr | PEpow : PExpr -> N -> PExpr. + Register PExpr as plugins.setoid_ring.pexpr. + Register PEc as plugins.setoid_ring.const. + Register PEX as plugins.setoid_ring.var. + Register PEadd as plugins.setoid_ring.add. + Register PEsub as plugins.setoid_ring.sub. + Register PEmul as plugins.setoid_ring.mul. + Register PEopp as plugins.setoid_ring.opp. + Register PEpow as plugins.setoid_ring.pow. (** evaluation of polynomial expressions towards R *) Definition mk_X j := mkPinj_pred j mkX. diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 0734654abf..85e759d152 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -205,25 +205,16 @@ let exec_tactic env evd n f args = let nf c = constr_of evd c in Array.map nf !tactic_res, Evd.universe_context_set evd -let stdlib_modules = - [["Coq";"Setoids";"Setoid"]; - ["Coq";"Lists";"List"]; - ["Coq";"Init";"Datatypes"]; - ["Coq";"Init";"Logic"]; - ] - -let coq_constant c = - lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" stdlib_modules c)) -let coq_reference c = - lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c) - -let coq_mk_Setoid = coq_constant "Build_Setoid_Theory" -let coq_None = coq_reference "None" -let coq_Some = coq_reference "Some" -let coq_eq = coq_constant "eq" - -let coq_cons = coq_reference "cons" -let coq_nil = coq_reference "nil" +let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref n))) +let gen_reference n = lazy (Coqlib.lib_ref n) + +let coq_mk_Setoid = gen_constant "plugins.setoid_ring.Build_Setoid_Theory" +let coq_None = gen_reference "core.option.None" +let coq_Some = gen_reference "core.option.Some" +let coq_eq = gen_constant "core.eq.type" + +let coq_cons = gen_reference "core.list.cons" +let coq_nil = gen_reference "core.list.nil" let lapp f args = mkApp(Lazy.force f,args) @@ -260,16 +251,18 @@ let plugin_modules = let my_constant c = lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c)) + [@@ocaml.warning "-3"] let my_reference c = lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c) + [@@ocaml.warning "-3"] let znew_ring_path = DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"]) let zltac s = lazy(KerName.make (ModPath.MPfile znew_ring_path) (Label.make s)) -let mk_cst l s = lazy (Coqlib.coq_reference "newring" l s);; -let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;; +let mk_cst l s = lazy (Coqlib.coq_reference "newring" l s) [@@ocaml.warning "-3"] +let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s (* Ring theory *) @@ -907,7 +900,7 @@ let ftheory_to_obj : field_info -> obj = let field_equality evd r inv req = match EConstr.kind !evd req with | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) -> - let c = UnivGen.constr_of_global (Coqlib.build_coq_eq_data()).congr in + let c = UnivGen.constr_of_global Coqlib.(lib_ref "core.eq.congr") in let c = EConstr.of_constr c in mkApp(c,[|r;r;inv|]) | _ -> diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index f2f236f448..1492cfb4e4 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -201,8 +201,8 @@ let mkRInd mind = DAst.make @@ GRef (IndRef mind,None) let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t) let rec mkRnat n = - if n <= 0 then DAst.make @@ GRef (Coqlib.glob_O, None) else - mkRApp (DAst.make @@ GRef (Coqlib.glob_S, None)) [mkRnat (n - 1)] + if n <= 0 then DAst.make @@ GRef (Coqlib.lib_ref "num.nat.O", None) else + mkRApp (DAst.make @@ GRef (Coqlib.lib_ref "num.nat.S", None)) [mkRnat (n - 1)] let glob_constr ist genv = function | _, Some ce -> @@ -763,7 +763,7 @@ let mkEtaApp c n imin = let mkRefl t c gl = let sigma = project gl in - let (sigma, refl) = EConstr.fresh_global (pf_env gl) sigma Coqlib.((build_coq_eq_data()).refl) in + let (sigma, refl) = EConstr.fresh_global (pf_env gl) sigma Coqlib.(lib_ref "core.eq.refl") in EConstr.mkApp (refl, [|t; c|]), { gl with sigma } let discharge_hyp (id', (id, mode)) gl = @@ -1220,7 +1220,7 @@ let genclrtac cl cs clr = (fun type_err gl -> tclTHEN (tclTHEN (Proofview.V82.of_tactic (Tactics.elim_type (EConstr.of_constr - (UnivGen.constr_of_global @@ Coqlib.build_coq_False ())))) (old_cleartac clr)) + (UnivGen.constr_of_global @@ Coqlib.(lib_ref "core.False.type"))))) (old_cleartac clr)) (fun gl -> raise type_err) gl)) (old_cleartac clr) @@ -1504,7 +1504,7 @@ let tclOPTION o d = let tacIS_INJECTION_CASE ?ty t = begin tclOPTION ty (tacTYPEOF t) >>= fun ty -> tacREDUCE_TO_QUANTIFIED_IND ty >>= fun ((mind,_),_) -> - tclUNIT (GlobRef.equal (GlobRef.IndRef mind) (Coqlib.build_coq_eq ())) + tclUNIT (Coqlib.check_ind_ref "core.eq.type" mind) end let tclWITHTOP tac = Goal.enter begin fun gl -> diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 602fcfcab5..7f9a9e125e 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -115,7 +115,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let orig_gl, concl, env = gl, pf_concl gl, pf_env gl in ppdebug(lazy(Pp.str(if is_case then "==CASE==" else "==ELIM=="))); let fire_subst gl t = Reductionops.nf_evar (project gl) t in - let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in + let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in let eq = EConstr.of_constr eq in let is_undef_pat = function | sigma, T t -> EConstr.isEvar sigma (EConstr.of_constr t) @@ -421,7 +421,7 @@ let injectl2rtac sigma c = match EConstr.kind sigma c with let is_injection_case c gl = let gl, cty = pfe_type_of gl c in let (mind,_), _ = pf_reduce_to_quantified_ind gl cty in - GlobRef.equal (IndRef mind) (Coqlib.build_coq_eq ()) + GlobRef.equal (IndRef mind) Coqlib.(lib_ref "core.eq.type") let perform_injection c gl = let gl, cty = pfe_type_of gl c in diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 2af917b939..c04ced4ab4 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -130,7 +130,7 @@ let newssrcongrtac arg ist gl = let ssr_congr lr = EConstr.mkApp (arr, lr) in (* here thw two cases: simple equality or arrow *) let equality, _, eq_args, gl' = - let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in + let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in pf_saturate gl (EConstr.of_constr eq) 3 in tclMATCH_GOAL (equality, gl') (fun gl' -> fs gl' (List.assoc 0 eq_args)) (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) ty) ist) @@ -386,7 +386,7 @@ let rwcltac cl rdx dir sr gl = ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env (pf_env gl) (project gl) (snd sr))); let cvtac, rwtac, gl = if EConstr.Vars.closed0 (project gl) r' then - let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, Coqlib.build_coq_eq () in + let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, Coqlib.(lib_ref "core.eq.type") in let sigma, c_ty = Typing.type_of env sigma c in ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty)); match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with @@ -427,6 +427,7 @@ let rwcltac cl rdx dir sr gl = ;; +[@@@ocaml.warning "-3"] let lz_coq_prod = let prod = lazy (Coqlib.build_prod ()) in fun () -> Lazy.force prod @@ -438,7 +439,7 @@ let lz_setoid_relation = | _ -> let srel = try Some (UnivGen.constr_of_global @@ - Coqlib.coq_reference "Class_setoid" sdir "RewriteRelation") + Coqlib.find_reference "Class_setoid" ("Coq"::sdir) "RewriteRelation" [@ocaml.warning "-3"]) with _ -> None in last_srel := (env, srel); srel @@ -484,7 +485,7 @@ let rwprocess_rule dir rule gl = | _ -> let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in EConstr.mkApp (pi2, ra), sigma in - if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_True ())) then + if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.(lib_ref "core.True.type"))) then let s, sigma = sr sigma 2 in loop (converse_dir d) sigma s a.(1) rs 0 else diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 1dbacf0ff7..ce439d0497 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -149,6 +149,7 @@ let tac_case t = end (** [=> [: id]] ************************************************************) +[@@@ocaml.warning "-3"] let mk_abstract_id = let open Coqlib in let ssr_abstract_id = Summary.ref ~name:"SSR:abstractid" 0 in @@ -375,7 +376,7 @@ let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr = let rec gen_eq_tac () = Goal.enter begin fun g -> let sigma, env, concl = Goal.(sigma g, env g, concl g) in let sigma, eq = - EConstr.fresh_global env sigma (Coqlib.build_coq_eq ()) in + EConstr.fresh_global env sigma (Coqlib.lib_ref "core.eq.type") in let ctx, last = EConstr.decompose_prod_assum sigma concl in let args = match EConstr.kind_of_type sigma last with | Term.AtomicType (hd, args) -> diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 8ee6fbf036..94255bab6c 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -40,8 +40,7 @@ let ascii_kn = MutInd.make2 ascii_modpath ascii_label let path_of_Ascii = ((ascii_kn,0),1) let static_glob_Ascii = ConstructRef path_of_Ascii -let make_reference id = find_reference "Ascii interpretation" ascii_module id -let glob_Ascii = lazy (make_reference "Ascii") +let glob_Ascii = lazy (lib_ref "plugins.syntax.Ascii") open Lazy @@ -49,7 +48,7 @@ let interp_ascii ?loc p = let rec aux n p = if Int.equal n 0 then [] else let mp = p mod 2 in - (DAst.make ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None)) + (DAst.make ?loc @@ GRef (lib_ref (if Int.equal mp 0 then "core.bool.false" else "core.bool.true"),None)) :: (aux (n-1) (p/2)) in DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p) @@ -67,8 +66,8 @@ let interp_ascii_string ?loc s = let uninterp_ascii r = let rec uninterp_bool_list n = function | [] when Int.equal n 0 -> 0 - | r::l when is_gr r glob_true -> 1+2*(uninterp_bool_list (n-1) l) - | r::l when is_gr r glob_false -> 2*(uninterp_bool_list (n-1) l) + | r::l when is_gr r (lib_ref "core.bool.true") -> 1+2*(uninterp_bool_list (n-1) l) + | r::l when is_gr r (lib_ref "core.bool.false") -> 2*(uninterp_bool_list (n-1) l) | _ -> raise Non_closed_ascii in try let aux c = match DAst.get c with diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index 703b40dd3e..59e65a0672 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -31,9 +31,8 @@ let string_kn = MutInd.make2 string_modpath @@ Label.make "string" let static_glob_EmptyString = ConstructRef ((string_kn,0),1) let static_glob_String = ConstructRef ((string_kn,0),2) -let make_reference id = find_reference "String interpretation" string_module id -let glob_String = lazy (make_reference "String") -let glob_EmptyString = lazy (make_reference "EmptyString") +let glob_String = lazy (lib_ref "plugins.syntax.String") +let glob_EmptyString = lazy (lib_ref "plugins.syntax.EmptyString") let is_gr c gr = match DAst.get c with | GRef (r, _) -> GlobRef.equal r gr diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index bae13dbba1..72d95f7eb1 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -46,12 +46,16 @@ let _ = Goptions.declare_bool_option { (*******************************************) (* Functions to deal with impossible cases *) (*******************************************) -(* XXX: we would like to search for this with late binding - "data.id.type" etc... *) let impossible_default_case () = - let c, ctx = UnivGen.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in + let type_of_id = + let open Names.GlobRef in + match Coqlib.lib_ref "core.IDProp.type" with + | ConstRef c -> c + | VarRef _ | IndRef _ | ConstructRef _ -> assert false + in + let c, ctx = UnivGen.fresh_global_instance (Global.env()) (Coqlib.(lib_ref "core.IDProp.idProp")) in let (_, u) = Constr.destConst c in - Some (c, Constr.mkConstU (Coqlib.type_of_id, u), ctx) + Some (c, Constr.mkConstU (type_of_id, u), ctx) let coq_unit_judge = let open Environ in diff --git a/pretyping/program.ml b/pretyping/program.ml index 8cfb7966cb..bbabbefdc3 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -11,8 +11,6 @@ open CErrors open Util -let init_reference dir s () = Coqlib.coq_reference "Program" dir s - let papp evdref r args = let open EConstr in let gr = delayed_force r in @@ -20,44 +18,48 @@ let papp evdref r args = evdref := evd; mkApp (hd, args) -let sig_typ = init_reference ["Init"; "Specif"] "sig" -let sig_intro = init_reference ["Init"; "Specif"] "exist" -let sig_proj1 = init_reference ["Init"; "Specif"] "proj1_sig" - -let sigT_typ = init_reference ["Init"; "Specif"] "sigT" -let sigT_intro = init_reference ["Init"; "Specif"] "existT" -let sigT_proj1 = init_reference ["Init"; "Specif"] "projT1" -let sigT_proj2 = init_reference ["Init"; "Specif"] "projT2" - -let prod_typ = init_reference ["Init"; "Datatypes"] "prod" -let prod_intro = init_reference ["Init"; "Datatypes"] "pair" -let prod_proj1 = init_reference ["Init"; "Datatypes"] "fst" -let prod_proj2 = init_reference ["Init"; "Datatypes"] "snd" +let sig_typ () = Coqlib.lib_ref "core.sig.type" +let sig_intro () = Coqlib.lib_ref "core.sig.intro" +let sig_proj1 () = Coqlib.lib_ref "core.sig.proj1" +(* let sig_proj2 () = Coqlib.lib_ref "core.sig.proj2" *) -let coq_eq_ind = init_reference ["Init"; "Logic"] "eq" -let coq_eq_refl = init_reference ["Init"; "Logic"] "eq_refl" -let coq_eq_refl_ref = init_reference ["Init"; "Logic"] "eq_refl" -let coq_eq_rect = init_reference ["Init"; "Logic"] "eq_rect" +let sigT_typ () = Coqlib.lib_ref "core.sigT.type" +let sigT_intro () = Coqlib.lib_ref "core.sigT.intro" +let sigT_proj1 () = Coqlib.lib_ref "core.sigT.proj1" +let sigT_proj2 () = Coqlib.lib_ref "core.sigT.proj2" -let coq_JMeq_ind = init_reference ["Logic";"JMeq"] "JMeq" -let coq_JMeq_refl = init_reference ["Logic";"JMeq"] "JMeq_refl" +let prod_typ () = Coqlib.lib_ref "core.prod.type" +let prod_intro () = Coqlib.lib_ref "core.prod.intro" +let prod_proj1 () = Coqlib.lib_ref "core.prod.proj1" +let prod_proj2 () = Coqlib.lib_ref "core.prod.proj2" -let coq_not = init_reference ["Init";"Logic"] "not" -let coq_and = init_reference ["Init";"Logic"] "and" +let coq_eq_ind () = Coqlib.lib_ref "core.eq.type" +let coq_eq_refl () = Coqlib.lib_ref "core.eq.refl" +let coq_eq_refl_ref () = Coqlib.lib_ref "core.eq.refl" +let coq_eq_rect () = Coqlib.lib_ref "core.eq.rect" let mk_coq_not sigma x = - let sigma, notc = Evarutil.new_global sigma (coq_not ()) in + let sigma, notc = Evarutil.new_global sigma Coqlib.(lib_ref "core.not.type") in sigma, EConstr.mkApp (notc, [| x |]) +let coq_JMeq_ind () = + try Coqlib.lib_ref "core.JMeq.type" + with Not_found -> + user_err (Pp.str "cannot find Coq.Logic.JMeq.JMeq; maybe library Coq.Logic.JMeq has to be required first.") +let coq_JMeq_refl () = Coqlib.lib_ref "core.JMeq.refl" + +(* let coq_not () = Universes.constr_of_global @@ Coqlib.lib_ref "core.not.type" *) +(* let coq_and () = Universes.constr_of_global @@ Coqlib.lib_ref "core.and.type" *) + let unsafe_fold_right f = function hd :: tl -> List.fold_right f tl hd | [] -> invalid_arg "unsafe_fold_right" let mk_coq_and sigma l = - let sigma, and_typ = Evarutil.new_global sigma (coq_and ()) in + let sigma, and_typ = Evarutil.new_global sigma Coqlib.(lib_ref "core.and.type") in sigma, unsafe_fold_right (fun c conj -> - EConstr.mkApp (and_typ, [| c ; conj |])) + EConstr.(mkApp (and_typ, [| c ; conj |]))) l (* true = transparent by default, false = opaque if possible *) diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index e12063fd44..bd95a62532 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -12,7 +12,6 @@ open Constr open EConstr open Hipattern open Tactics -open Coqlib open Reductionops open Proofview.Notations @@ -33,8 +32,8 @@ let absurd c = let sigma, j = Coercion.inh_coerce_to_sort env sigma j in let t = j.Environ.utj_val in Proofview.Unsafe.tclEVARS sigma <*> - Tacticals.New.pf_constr_of_global (build_coq_not ()) >>= fun coqnot -> - Tacticals.New.pf_constr_of_global (build_coq_False ()) >>= fun coqfalse -> + Tacticals.New.pf_constr_of_global (Coqlib.(lib_ref "core.not.type")) >>= fun coqnot -> + Tacticals.New.pf_constr_of_global (Coqlib.(lib_ref "core.False.type")) >>= fun coqfalse -> Tacticals.New.tclTHENLIST [ elim_type coqfalse; Simple.apply (mk_absurd_proof coqnot t) diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 832014a610..f2bc679aac 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -27,7 +27,6 @@ open Constr_matching open Hipattern open Proofview.Notations open Tacmach.New -open Coqlib open Tactypes (* This file containts the implementation of the tactics ``Decide @@ -269,9 +268,10 @@ let decideEquality rectype ops = (* The tactic Compare *) let compare c1 c2 = - pf_constr_of_global (build_coq_sumbool ()) >>= fun opc -> - pf_constr_of_global (Coqlib.build_coq_eq ()) >>= fun eqc -> - pf_constr_of_global (build_coq_not ()) >>= fun notc -> + let open Coqlib in + pf_constr_of_global (lib_ref "core.sumbool.type") >>= fun opc -> + pf_constr_of_global (lib_ref "core.eq.type") >>= fun eqc -> + pf_constr_of_global (lib_ref "core.not.type") >>= fun notc -> Proofview.Goal.enter begin fun gl -> let rectype = pf_unsafe_type_of gl c1 in let ops = (opc,eqc,notc) in diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index ea5ff4a6cb..16b94cd154 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -99,7 +99,7 @@ let my_it_mkLambda_or_LetIn_name s c = let get_coq_eq ctx = try - let eq = Globnames.destIndRef Coqlib.glob_eq in + let eq = Globnames.destIndRef (Coqlib.lib_ref "core.eq.type") in (* Do not force the lazy if they are not defined *) let eq, ctx = with_context_set ctx (UnivGen.fresh_inductive_instance (Global.env ()) eq) in diff --git a/tactics/equality.ml b/tactics/equality.ml index 510f119229..3e3ef78c5d 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -339,12 +339,17 @@ let jmeq_same_dom env sigma = function let find_elim hdcncl lft2rgt dep cls ot = Proofview.Goal.enter_one begin fun gl -> let sigma = project gl in - let is_global gr c = Termops.is_global sigma gr c in + let is_global_exists gr c = + Coqlib.has_ref gr && Termops.is_global sigma (Coqlib.lib_ref gr) c + in let inccl = Option.is_empty cls in let env = Proofview.Goal.env gl in - if (is_global Coqlib.glob_eq hdcncl || - (is_global Coqlib.glob_jmeq hdcncl && - jmeq_same_dom env sigma ot)) && not dep + (* if (is_global Coqlib.glob_eq hdcncl || *) + (* (is_global Coqlib.glob_jmeq hdcncl && *) + (* jmeq_same_dom env sigma ot)) && not dep *) + if (is_global_exists "core.eq.type" hdcncl || + (is_global_exists "core.JMeq.type" hdcncl + && jmeq_same_dom env sigma ot)) && not dep then let c = match EConstr.kind sigma hdcncl with @@ -588,7 +593,7 @@ let classes_dirpath = let init_setoid () = if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then () - else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"] + else check_required_library ["Coq";"Setoids";"Setoid"] let check_setoid cl = Option.fold_left @@ -637,8 +642,8 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = | None -> tclFAIL 0 (str"Terms do not have convertible types") | Some evd -> - let e = build_coq_eq () in - let sym = build_coq_eq_sym () in + let e = lib_ref "core.eq.type" in + let sym = lib_ref "core.eq.sym" in Tacticals.New.pf_constr_of_global sym >>= fun sym -> Tacticals.New.pf_constr_of_global e >>= fun e -> let eq = applist (e, [t1;c1;c2]) in @@ -930,9 +935,9 @@ let build_selector env sigma dirn c ind special default = let ans = Inductiveops.make_case_or_project env sigma indf ci p c (Array.of_list brl) in ans -let build_coq_False () = pf_constr_of_global (build_coq_False ()) -let build_coq_True () = pf_constr_of_global (build_coq_True ()) -let build_coq_I () = pf_constr_of_global (build_coq_I ()) +let build_coq_False () = pf_constr_of_global (lib_ref "core.False.type") +let build_coq_True () = pf_constr_of_global (lib_ref "core.True.type") +let build_coq_I () = pf_constr_of_global (lib_ref "core.True.I") let rec build_discriminator env sigma true_0 false_0 dirn c = function | [] -> @@ -1320,15 +1325,15 @@ let inject_if_homogenous_dependent_pair ty = let sigma = Tacmach.New.project gl in let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in (* fetch the informations of the pair *) - let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in - let existTconstr () = (Coqlib.build_sigma_type()).Coqlib.intro in + let sigTconstr = Coqlib.(lib_ref "core.sigT.type") in + let existTconstr = Coqlib.lib_ref "core.sigT.intro" in (* check whether the equality deals with dep pairs or not *) let eqTypeDest = fst (decompose_app sigma t) in - if not (Termops.is_global sigma (sigTconstr()) eqTypeDest) then raise Exit; + if not (Termops.is_global sigma sigTconstr eqTypeDest) then raise Exit; let hd1,ar1 = decompose_app_vect sigma t1 and hd2,ar2 = decompose_app_vect sigma t2 in - if not (Termops.is_global sigma (existTconstr()) hd1) then raise Exit; - if not (Termops.is_global sigma (existTconstr()) hd2) then raise Exit; + if not (Termops.is_global sigma existTconstr hd1) then raise Exit; + if not (Termops.is_global sigma existTconstr hd2) then raise Exit; let (ind, _), _ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in (* check if the user has declared the dec principle *) (* and compare the fst arguments of the dep pair *) @@ -1336,17 +1341,16 @@ let inject_if_homogenous_dependent_pair ty = (* knows inductive types *) if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) ind && pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit; - Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"]; + check_required_library ["Coq";"Logic";"Eqdep_dec"]; let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in - let inj2 = Coqlib.coq_reference "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"] - "inj_pair2_eq_dec" in + let inj2 = lib_ref "core.eqdep_dec.inj_pair2" in let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in (* cut with the good equality and prove the requested goal *) tclTHENLIST [Proofview.tclEFFECTS eff; intro; onLastHyp (fun hyp -> - Tacticals.New.pf_constr_of_global Coqlib.glob_eq >>= fun ceq -> + Tacticals.New.pf_constr_of_global Coqlib.(lib_ref "core.eq.type") >>= fun ceq -> tclTHENS (cut (mkApp (ceq,new_eq_args))) [clear [destVar sigma hyp]; Tacticals.New.pf_constr_of_global inj2 >>= fun inj2 -> @@ -1671,8 +1675,8 @@ let _ = optwrite = (:=) regular_subst_tactic } let restrict_to_eq_and_identity eq = (* compatibility *) - if not (is_global glob_eq eq) && - not (is_global glob_identity eq) + if not (is_global (lib_ref "core.eq.type") eq) && + not (is_global (lib_ref "core.identity.type") eq) then raise Constr_matching.PatternMatchingFailure exception FoundHyp of (Id.t * constr * bool) diff --git a/tactics/hints.ml b/tactics/hints.ml index af6d1c472f..245bdce5ad 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1292,13 +1292,13 @@ let project_hint ~poly pri l2r r = let sigma, c = Evd.fresh_global env sigma gr in let t = Retyping.get_type_of env sigma c in let t = - Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in + Tacred.reduce_to_quantified_ref env sigma (lib_ref "core.iff.type") t in let sign,ccl = decompose_prod_assum sigma t in let (a,b) = match snd (decompose_app sigma ccl) with | [a;b] -> (a,b) | _ -> assert false in let p = - if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in + if l2r then lib_ref "core.iff.proj1" else lib_ref "core.iff.proj2" in let sigma, p = Evd.fresh_global env sigma p in let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in let c = it_mkLambda_or_LetIn diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index a1bb0a7401..708412720a 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -289,24 +289,22 @@ let coq_refl_jm_pattern = mkPattern (mkGProd "A" mkGHole (mkGProd "x" (mkGVar "A") (mkGApp mkGHole [mkGVar "A"; mkGVar "x"; mkGVar "A"; mkGVar "x";]))) -open Globnames - let match_with_equation env sigma t = if not (isApp sigma t) then raise NoEquationFound; let (hdapp,args) = destApp sigma t in match EConstr.kind sigma hdapp with | Ind (ind,u) -> - if GlobRef.equal (IndRef ind) glob_eq then - Some (build_coq_eq_data()),hdapp, - PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if GlobRef.equal (IndRef ind) glob_identity then - Some (build_coq_identity_data()),hdapp, - PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if GlobRef.equal (IndRef ind) glob_jmeq then - Some (build_coq_jmeq_data()),hdapp, - HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) - else - let (mib,mip) = Global.lookup_inductive ind in + if Coqlib.check_ind_ref "core.eq.type" ind then + Some (build_coq_eq_data()),hdapp, + PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) + else if Coqlib.check_ind_ref "core.identity.type" ind then + Some (build_coq_identity_data()),hdapp, + PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) + else if Coqlib.check_ind_ref "core.JMeq.type" ind then + Some (build_coq_jmeq_data()),hdapp, + HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) + else + let (mib,mip) = Global.lookup_inductive ind in let constr_types = mip.mind_nf_lc in let nconstr = Array.length mip.mind_consnames in if Int.equal nconstr 1 then @@ -438,12 +436,12 @@ let match_eq sigma eqn (ref, hetero) = | _ -> raise PatternMatchingFailure let no_check () = true -let check_jmeq_loaded () = Library.library_is_loaded @@ Coqlib.jmeq_library_path +let check_jmeq_loaded () = has_ref "core.JMeq.type" let equalities = - [(coq_eq_ref, false), no_check, build_coq_eq_data; - (coq_jmeq_ref, true), check_jmeq_loaded, build_coq_jmeq_data; - (coq_identity_ref, false), no_check, build_coq_identity_data] + [(lazy(lib_ref "core.eq.type"), false), no_check, build_coq_eq_data; + (lazy(lib_ref "core.JMeq.type"), true), check_jmeq_loaded, build_coq_jmeq_data; + (lazy(lib_ref "core.identity.type"), false), no_check, build_coq_identity_data] let find_eq_data sigma eqn = (* fails with PatternMatchingFailure *) let d,k = first_match (match_eq sigma eqn) equalities in @@ -478,9 +476,9 @@ let find_this_eq_data_decompose gl eqn = let match_sigma env sigma ex = match EConstr.kind sigma ex with - | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (Lazy.force coq_exist_ref) f -> + | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (lib_ref "core.sig.intro") f -> build_sigma (), (snd (destConstruct sigma f), a, p, car, cdr) - | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (Lazy.force coq_existT_ref) f -> + | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (lib_ref "core.sigT.intro") f -> build_sigma_type (), (snd (destConstruct sigma f), a, p, car, cdr) | _ -> raise PatternMatchingFailure @@ -489,7 +487,7 @@ let find_sigma_data_decompose env ex = (* fails with PatternMatchingFailure *) (* Pattern "(sig ?1 ?2)" *) let coq_sig_pattern = - lazy (mkPattern (mkGAppRef coq_sig_ref [mkGPatVar "X1"; mkGPatVar "X2"])) + lazy (mkPattern (mkGAppRef (lazy (lib_ref "core.sig.type")) [mkGPatVar "X1"; mkGPatVar "X2"])) let match_sigma env sigma t = match Id.Map.bindings (matches env sigma (Lazy.force coq_sig_pattern) t) with @@ -507,44 +505,44 @@ let is_matching_sigma env sigma t = is_matching env sigma (Lazy.force coq_sig_pa let coq_eqdec ~sum ~rev = lazy ( - let eqn = mkGAppRef coq_eq_ref (List.map mkGPatVar ["X1"; "X2"; "X3"]) in - let args = [eqn; mkGAppRef coq_not_ref [eqn]] in + let eqn = mkGAppRef (lazy (lib_ref "core.eq.type")) (List.map mkGPatVar ["X1"; "X2"; "X3"]) in + let args = [eqn; mkGAppRef (lazy (lib_ref "core.not.type")) [eqn]] in let args = if rev then List.rev args else args in mkPattern (mkGAppRef sum args) ) +let sumbool_type = lazy (lib_ref "core.sumbool.type") +let or_type = lazy (lib_ref "core.or.type") + (** [{ ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 }] *) -let coq_eqdec_inf_pattern = coq_eqdec ~sum:coq_sumbool_ref ~rev:false +let coq_eqdec_inf_pattern = coq_eqdec ~sum:sumbool_type ~rev:false (** [{ ~ ?X2 = ?X3 :> ?X1 } + { ?X2 = ?X3 :> ?X1 }] *) -let coq_eqdec_inf_rev_pattern = coq_eqdec ~sum:coq_sumbool_ref ~rev:true +let coq_eqdec_inf_rev_pattern = coq_eqdec ~sum:sumbool_type ~rev:true (** %coq_or_ref (?X2 = ?X3 :> ?X1) (~ ?X2 = ?X3 :> ?X1) *) -let coq_eqdec_pattern = coq_eqdec ~sum:coq_or_ref ~rev:false +let coq_eqdec_pattern = coq_eqdec ~sum:or_type ~rev:false (** %coq_or_ref (~ ?X2 = ?X3 :> ?X1) (?X2 = ?X3 :> ?X1) *) -let coq_eqdec_rev_pattern = coq_eqdec ~sum:coq_or_ref ~rev:true - -let op_or = coq_or_ref -let op_sum = coq_sumbool_ref +let coq_eqdec_rev_pattern = coq_eqdec ~sum:or_type ~rev:true let match_eqdec env sigma t = let eqonleft,op,subst = - try true,op_sum,matches env sigma (Lazy.force coq_eqdec_inf_pattern) t + try true,sumbool_type,matches env sigma (Lazy.force coq_eqdec_inf_pattern) t with PatternMatchingFailure -> - try false,op_sum,matches env sigma (Lazy.force coq_eqdec_inf_rev_pattern) t + try false,sumbool_type,matches env sigma (Lazy.force coq_eqdec_inf_rev_pattern) t with PatternMatchingFailure -> - try true,op_or,matches env sigma (Lazy.force coq_eqdec_pattern) t + try true,or_type,matches env sigma (Lazy.force coq_eqdec_pattern) t with PatternMatchingFailure -> - false,op_or,matches env sigma (Lazy.force coq_eqdec_rev_pattern) t in + false,or_type,matches env sigma (Lazy.force coq_eqdec_rev_pattern) t in match Id.Map.bindings subst with | [(_,typ);(_,c1);(_,c2)] -> eqonleft, Lazy.force op, c1, c2, typ | _ -> anomaly (Pp.str "Unexpected pattern.") (* Patterns "~ ?" and "? -> False" *) -let coq_not_pattern = lazy (mkPattern (mkGAppRef coq_not_ref [mkGHole])) -let coq_imp_False_pattern = lazy (mkPattern (mkGArrow mkGHole (mkGRef coq_False_ref))) +let coq_not_pattern = lazy (mkPattern (mkGAppRef (lazy (lib_ref "core.not.type")) [mkGHole])) +let coq_imp_False_pattern = lazy (mkPattern (mkGArrow mkGHole (mkGRef (lazy (lib_ref "core.False.type"))))) let is_matching_not env sigma t = is_matching env sigma (Lazy.force coq_not_pattern) t let is_matching_imp_False env sigma t = is_matching env sigma (Lazy.force coq_imp_False_pattern) t diff --git a/tactics/inv.ml b/tactics/inv.ml index 5ac4284b43..6a39a10fc4 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -350,7 +350,7 @@ let remember_first_eq id x = if !x == Logic.MoveLast then x := Logic.MoveAfter i let dest_nf_eq env sigma t = match EConstr.kind sigma t with | App (r, [| t; x; y |]) -> let open Reductionops in - let lazy eq = Coqlib.coq_eq_ref in + let eq = Coqlib.lib_ref "core.eq.type" in if EConstr.is_global sigma eq r then (t, whd_all env sigma x, whd_all env sigma y) else user_err Pp.(str "Not an equality.") diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3769dca6e0..9ec3e203cc 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3552,12 +3552,13 @@ let error_ind_scheme s = let s = if not (String.is_empty s) then s^" " else s in user_err ~hdr:"Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.") -let coq_eq sigma = Evarutil.new_global sigma (Coqlib.build_coq_eq ()) -let coq_eq_refl sigma = Evarutil.new_global sigma (Coqlib.build_coq_eq_refl ()) +let coq_eq sigma = Evarutil.new_global sigma Coqlib.(lib_ref "core.eq.type") +let coq_eq_refl sigma = Evarutil.new_global sigma Coqlib.(lib_ref "core.eq.refl") -let coq_heq_ref = lazy (Coqlib.coq_reference"mkHEq" ["Logic";"JMeq"] "JMeq") +let coq_heq_ref = lazy (Coqlib.lib_ref "core.JMeq.type") let coq_heq sigma = Evarutil.new_global sigma (Lazy.force coq_heq_ref) -let coq_heq_refl sigma = Evarutil.new_global sigma (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq_refl") +let coq_heq_refl sigma = Evarutil.new_global sigma (Coqlib.lib_ref "core.JMeq.refl") +(* let coq_heq_refl = lazy (glob (lib_ref "core.JMeq.refl")) *) let mkEq sigma t x y = let sigma, eq = coq_eq sigma in @@ -3789,7 +3790,7 @@ let abstract_args gl generalize_vars dep id defined f args = let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = let open Context.Named.Declaration in Proofview.Goal.enter begin fun gl -> - Coqlib.check_required_library Coqlib.jmeq_module_name; + Coqlib.(check_required_library jmeq_module_name); let sigma = Tacmach.New.project gl in let (f, args, def, id, oldid) = let oldid = Tacmach.New.pf_get_new_id id gl in @@ -3849,7 +3850,7 @@ let specialize_eqs id = match EConstr.kind !evars ty with | Prod (na, t, b) -> (match EConstr.kind !evars t with - | App (eq, [| eqty; x; y |]) when EConstr.is_global !evars (Lazy.force coq_eq_ref) eq -> + | App (eq, [| eqty; x; y |]) when EConstr.is_global !evars Coqlib.(lib_ref "core.eq.type") eq -> let c = if noccur_between !evars 1 (List.length ctx) x then y else x in let pt = mkApp (eq, [| eqty; c; c |]) in let ind = destInd !evars eq in diff --git a/test-suite/success/btauto.v b/test-suite/success/btauto.v new file mode 100644 index 0000000000..d2512b5cbb --- /dev/null +++ b/test-suite/success/btauto.v @@ -0,0 +1,9 @@ +Require Import Btauto. + +Open Scope bool_scope. + +Lemma test_orb a b : (if a || b then negb (negb b && negb a) else negb a && negb b) = true. +Proof. btauto. Qed. + +Lemma test_xorb a : xorb a a = false. +Proof. btauto. Qed. diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 6f220f2023..0c68b75124 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -83,6 +83,8 @@ Proof. apply le_dec. Defined. +Register le_gt_dec as num.nat.le_gt_dec. + (** Proofs of decidability *) Theorem dec_le n m : decidable (n <= m). @@ -130,6 +132,16 @@ Proof. apply Nat.nlt_ge. Qed. +Register dec_le as num.nat.dec_le. +Register dec_lt as num.nat.dec_lt. +Register dec_ge as num.nat.dec_ge. +Register dec_gt as num.nat.dec_gt. +Register not_eq as num.nat.not_eq. +Register not_le as num.nat.not_le. +Register not_lt as num.nat.not_lt. +Register not_ge as num.nat.not_ge. +Register not_gt as num.nat.not_gt. + (** A ternary comparison function in the spirit of [Z.compare]. See now [Nat.compare] and its properties. diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index 3bf6cd952f..d6adb7e205 100644 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v @@ -46,6 +46,8 @@ Proof. symmetry. apply Nat.sub_1_r. Qed. +Register pred_of_minus as num.nat.pred_of_minus. + (** * Diagonal *) Notation minus_diag := Nat.sub_diag (only parsing). (* n - n = 0 *) diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 9a24c804a1..ddbc128aa1 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -30,6 +30,8 @@ Proof. elim (Nat.eq_dec n m); [left|right]; trivial. Defined. +Register dec_eq_nat as num.nat.eq_dec. + Definition UIP_nat:= Eqdep_dec.UIP_dec Nat.eq_dec. Import EqNotations. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 8a0265438a..75f14bb4da 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -41,6 +41,10 @@ Declare Scope bool_scope. Delimit Scope bool_scope with bool. Bind Scope bool_scope with bool. +Register bool as core.bool.type. +Register true as core.bool.true. +Register false as core.bool.false. + (** Basic boolean operators *) Definition andb (b1 b2:bool) : bool := if b1 then b2 else false. @@ -62,6 +66,11 @@ Definition negb (b:bool) := if b then false else true. Infix "||" := orb : bool_scope. Infix "&&" := andb : bool_scope. +Register andb as core.bool.andb. +Register orb as core.bool.orb. +Register xorb as core.bool.xorb. +Register negb as core.bool.negb. + (** Basic properties of [andb] *) Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true. @@ -70,6 +79,8 @@ Proof. Qed. Hint Resolve andb_prop: bool. +Register andb_prop as core.bool.andb_prop. + Lemma andb_true_intro : forall b1 b2:bool, b1 = true /\ b2 = true -> andb b1 b2 = true. Proof. @@ -77,12 +88,16 @@ Proof. Qed. Hint Resolve andb_true_intro: bool. +Register andb_true_intro as core.bool.andb_true_intro. + (** Interpretation of booleans as propositions *) Inductive eq_true : bool -> Prop := is_eq_true : eq_true true. Hint Constructors eq_true : eq_true. +Register eq_true as core.eq_true.type. + (** Another way of interpreting booleans as propositions *) Definition is_true b := b = true. @@ -141,6 +156,9 @@ Delimit Scope nat_scope with nat. Bind Scope nat_scope with nat. Arguments S _%nat. +Register nat as num.nat.type. +Register O as num.nat.O. +Register S as num.nat.S. (********************************************************************) (** * Container datatypes *) @@ -156,6 +174,10 @@ Inductive option (A:Type) : Type := Arguments Some {A} a. Arguments None {A}. +Register option as core.option.type. +Register Some as core.option.Some. +Register None as core.option.None. + Definition option_map (A B:Type) (f:A->B) (o : option A) : option B := match o with | Some a => @Some B (f a) @@ -187,11 +209,19 @@ Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. Arguments pair {A B} _ _. +Register prod as core.prod.type. +Register pair as core.prod.intro. +Register prod_rect as core.prod.rect. + Section projections. Context {A : Type} {B : Type}. Definition fst (p:A * B) := match p with (x, y) => x end. Definition snd (p:A * B) := match p with (x, y) => y end. + + Register fst as core.prod.proj1. + Register snd as core.prod.proj2. + End projections. Hint Resolve pair inl inr: core. @@ -239,6 +269,10 @@ Bind Scope list_scope with list. Infix "::" := cons (at level 60, right associativity) : list_scope. +Register list as core.list.type. +Register nil as core.list.nil. +Register cons as core.list.cons. + Local Open Scope list_scope. Definition length (A : Type) : list A -> nat := @@ -269,6 +303,11 @@ Inductive comparison : Set := | Lt : comparison | Gt : comparison. +Register comparison as core.comparison.type. +Register Eq as core.comparison.Eq. +Register Lt as core.comparison.Lt. +Register Gt as core.comparison.Gt. + Lemma comparison_eq_stable : forall c c' : comparison, ~~ c = c' -> c = c'. Proof. destruct c, c'; intro H; reflexivity || destruct H; discriminate. @@ -353,6 +392,10 @@ Arguments identity_ind [A] a P f y i. Arguments identity_rec [A] a P f y i. Arguments identity_rect [A] a P f y i. +Register identity as core.identity.type. +Register identity_refl as core.identity.refl. +Register identity_ind as core.identity.ind. + (** Identity type *) Definition ID := forall A:Type, A -> A. @@ -361,6 +404,8 @@ Definition id : ID := fun A x => x. Definition IDProp := forall A:Prop, A -> A. Definition idProp : IDProp := fun A x => x. +Register IDProp as core.IDProp.type. +Register idProp as core.IDProp.idProp. (* begin hide *) diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 4ec0049a9c..1db0a8e1b5 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -21,14 +21,21 @@ Notation "A -> B" := (forall (_ : A), B) : type_scope. Inductive True : Prop := I : True. +Register True as core.True.type. +Register I as core.True.I. + (** [False] is the always false proposition *) Inductive False : Prop :=. +Register False as core.False.type. + (** [not A], written [~A], is the negation of [A] *) Definition not (A:Prop) := A -> False. Notation "~ x" := (not x) : type_scope. +Register not as core.not.type. + (** Create the "core" hint database, and set its transparent state for variables and constants explicitely. *) @@ -50,6 +57,9 @@ Inductive and (A B:Prop) : Prop := where "A /\ B" := (and A B) : type_scope. +Register and as core.and.type. +Register conj as core.and.conj. + Section Conjunction. Variables A B : Prop. @@ -77,12 +87,18 @@ where "A \/ B" := (or A B) : type_scope. Arguments or_introl [A B] _, [A] B _. Arguments or_intror [A B] _, A [B] _. +Register or as core.or.type. + (** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *) Definition iff (A B:Prop) := (A -> B) /\ (B -> A). Notation "A <-> B" := (iff A B) : type_scope. +Register iff as core.iff.type. +Register proj1 as core.iff.proj1. +Register proj2 as core.iff.proj2. + Section Equivalence. Theorem iff_refl : forall A:Prop, A <-> A. @@ -257,6 +273,8 @@ Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3) Inductive ex (A:Type) (P:A -> Prop) : Prop := ex_intro : forall x:A, P x -> ex (A:=A) P. +Register ex as core.ex.type. + Inductive ex2 (A:Type) (P Q:A -> Prop) : Prop := ex_intro2 : forall x:A, P x -> Q x -> ex2 (A:=A) P Q. @@ -333,6 +351,11 @@ Hint Resolve I conj or_introl or_intror : core. Hint Resolve eq_refl: core. Hint Resolve ex_intro ex_intro2: core. +Register eq as core.eq.type. +Register eq_refl as core.eq.refl. +Register eq_ind as core.eq.ind. +Register eq_rect as core.eq.rect. + Section Logic_lemmas. Theorem absurd : forall A C:Prop, A -> ~ A -> C. @@ -351,16 +374,22 @@ Section Logic_lemmas. destruct 1; trivial. Defined. + Register eq_sym as core.eq.sym. + Theorem eq_trans : x = y -> y = z -> x = z. Proof. destruct 2; trivial. Defined. + Register eq_trans as core.eq.trans. + Theorem f_equal : x = y -> f x = f y. Proof. destruct 1; trivial. Defined. + Register f_equal as core.eq.congr. + Theorem not_eq_sym : x <> y -> y <> x. Proof. red; intros h1 h2; apply h1; destruct h2; trivial. @@ -373,6 +402,8 @@ Section Logic_lemmas. intros A x P H y H0. elim eq_sym with (1 := H0); assumption. Defined. + Register eq_ind_r as core.eq.ind_r. + Definition eq_rec_r : forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y. intros A x P H y H0; elim eq_sym with (1 := H0); assumption. @@ -458,6 +489,8 @@ Proof. destruct 1; destruct 1; reflexivity. Qed. +Register f_equal2 as core.eq.congr2. + Theorem f_equal3 : forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) (x2 y2:A2) (x3 y3:A3), diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index 6f10a93997..587de12a15 100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -51,6 +51,11 @@ Section identity_is_a_congruence. End identity_is_a_congruence. +Register identity_sym as core.identity.sym. +Register identity_trans as core.identity.trans. +Register identity_congr as core.identity.congr. + + Definition identity_ind_r : forall (A:Type) (a:A) (P:A -> Prop), P a -> forall y:A, identity y a -> P y. intros A x P H y H0; case identity_sym with (1 := H0); trivial. diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v index eb4ba0e5e6..7e7a1ced58 100644 --- a/theories/Init/Nat.v +++ b/theories/Init/Nat.v @@ -42,6 +42,8 @@ Definition pred n := | S u => u end. +Register pred as num.nat.pred. + Fixpoint add n m := match n with | 0 => m @@ -50,6 +52,8 @@ Fixpoint add n m := where "n + m" := (add n m) : nat_scope. +Register add as num.nat.add. + Definition double n := n + n. Fixpoint mul n m := @@ -60,6 +64,8 @@ Fixpoint mul n m := where "n * m" := (mul n m) : nat_scope. +Register mul as num.nat.mul. + (** Truncated subtraction: [n-m] is [0] if [n<=m] *) Fixpoint sub n m := @@ -70,6 +76,8 @@ Fixpoint sub n m := where "n - m" := (sub n m) : nat_scope. +Register sub as num.nat.sub. + (** ** Comparisons *) Fixpoint eqb n m : bool := diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 65e5e76a22..4489f4cb15 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -182,6 +182,11 @@ Notation "x <= y < z" := (x <= y /\ y < z) : nat_scope. Notation "x < y < z" := (x < y /\ y < z) : nat_scope. Notation "x < y <= z" := (x < y /\ y <= z) : nat_scope. +Register le as num.nat.le. +Register lt as num.nat.lt. +Register ge as num.nat.ge. +Register gt as num.nat.gt. + Theorem le_pred : forall n m, n <= m -> pred n <= pred m. Proof. induction 1; auto. destruct m; simpl; auto. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index a5f926f7ab..e4796a8059 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -27,6 +27,10 @@ Require Import Logic. Inductive sig (A:Type) (P:A -> Prop) : Type := exist : forall x:A, P x -> sig P. +Register sig as core.sig.type. +Register exist as core.sig.intro. +Register sig_rect as core.sig.rect. + Inductive sig2 (A:Type) (P Q:A -> Prop) : Type := exist2 : forall x:A, P x -> Q x -> sig2 P Q. @@ -36,6 +40,10 @@ Inductive sig2 (A:Type) (P Q:A -> Prop) : Type := Inductive sigT (A:Type) (P:A -> Type) : Type := existT : forall x:A, P x -> sigT P. +Register sigT as core.sigT.type. +Register existT as core.sigT.intro. +Register sigT_rect as core.sigT.rect. + Inductive sigT2 (A:Type) (P Q:A -> Type) : Type := existT2 : forall x:A, P x -> Q x -> sigT2 P Q. @@ -93,6 +101,9 @@ Section Subset_projections. | exist _ a b => b end. + Register proj1_sig as core.sig.proj1. + Register proj2_sig as core.sig.proj2. + End Subset_projections. @@ -152,6 +163,9 @@ Section Projections. | existT _ _ h => h end. + Register projT1 as core.sigT.proj1. + Register projT2 as core.sigT.proj2. + End Projections. Local Notation "( x ; y )" := (existT _ x y) (at level 0, format "( x ; '/ ' y )"). @@ -681,6 +695,8 @@ Add Printing If sumbool. Arguments left {A B} _, [A] B _. Arguments right {A B} _ , A [B] _. +Register sumbool as core.sumbool.type. + (** [sumor] is an option type equipped with the justification of why it may not be a regular value *) diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index c27ffa33f8..f4cb34c713 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -42,6 +42,8 @@ Section Well_founded. Definition well_founded := forall a:A, Acc a. + Register well_founded as core.wf.well_founded. + (** Well-founded induction on [Set] and [Prop] *) Hypothesis Rwf : well_founded. diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v index 35920d9134..49276f904f 100644 --- a/theories/Logic/Decidable.v +++ b/theories/Logic/Decidable.v @@ -87,6 +87,21 @@ Proof. unfold decidable; tauto. Qed. +Register dec_True as core.dec.True. +Register dec_False as core.dec.False. +Register dec_or as core.dec.or. +Register dec_and as core.dec.and. +Register dec_not as core.dec.not. +Register dec_imp as core.dec.imp. +Register dec_iff as core.dec.iff. +Register dec_not_not as core.dec.not_not. +Register not_not as core.dec.dec_not_not. +Register not_or as core.dec.not_or. +Register not_and as core.dec.not_and. +Register not_imp as core.dec.not_imp. +Register imp_simp as core.dec.imp_simp. +Register not_iff as core.dec.not_iff. + (** Results formulated with iff, used in FSetDecide. Negation are expanded since it is unclear whether setoid rewrite will always perform conversion. *) diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index 0560d9ed46..4e8b48af9f 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -347,6 +347,8 @@ Proof. apply eq_dec. Qed. +Register inj_pair2_eq_dec as core.eqdep_dec.inj_pair2. + (** Examples of short direct proofs of unicity of reflexivity proofs on specific domains *) diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 9c56b60aa4..25b7811417 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -28,10 +28,15 @@ Set Elimination Schemes. Arguments JMeq_refl {A x} , [A] x. +Register JMeq as core.JMeq.type. +Register JMeq_refl as core.JMeq.refl. + Hint Resolve JMeq_refl. Definition JMeq_hom {A : Type} (x y : A) := JMeq x y. +Register JMeq_hom as core.JMeq.hom. + Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x. Proof. intros; destruct H; trivial. @@ -39,12 +44,16 @@ Qed. Hint Immediate JMeq_sym. +Register JMeq_sym as core.JMeq.sym. + Lemma JMeq_trans : forall (A B C:Type) (x:A) (y:B) (z:C), JMeq x y -> JMeq y z -> JMeq x z. Proof. destruct 2; trivial. Qed. +Register JMeq_trans as core.JMeq.trans. + Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y. Lemma JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop), @@ -53,6 +62,8 @@ Proof. intros A x P H y H'; case JMeq_eq with (1 := H'); trivial. Qed. +Register JMeq_ind as core.JMeq.ind. + Lemma JMeq_rec : forall (A:Type) (x:A) (P:A -> Set), P x -> forall y, JMeq x y -> P y. Proof. @@ -89,6 +100,8 @@ Proof. intros A x B f y H; case JMeq_eq with (1 := H); trivial. Qed. +Register JMeq_congr as core.JMeq.congr. + (** [JMeq] is equivalent to [eq_dep Type (fun X => X)] *) Require Import Eqdep. diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v index 7b6740e94b..ef2c688759 100644 --- a/theories/Numbers/BinNums.v +++ b/theories/Numbers/BinNums.v @@ -29,6 +29,10 @@ Bind Scope positive_scope with positive. Arguments xO _%positive. Arguments xI _%positive. +Register xI as num.pos.xI. +Register xO as num.pos.xO. +Register xH as num.pos.xH. + (** [N] is a datatype representing natural numbers in a binary way, by extending the [positive] datatype with a zero. Numbers in [N] will also be denoted using a decimal notation; @@ -43,6 +47,10 @@ Delimit Scope N_scope with N. Bind Scope N_scope with N. Arguments Npos _%positive. +Register N as num.N.type. +Register N0 as num.N.N0. +Register Npos as num.N.Npos. + (** [Z] is a datatype representing the integers in a binary way. An integer is either zero or a strictly positive number (coded as a [positive]) or a strictly negative number @@ -60,3 +68,8 @@ Delimit Scope Z_scope with Z. Bind Scope Z_scope with Z. Arguments Zpos _%positive. Arguments Zneg _%positive. + +Register Z as num.Z.type. +Register Z0 as num.Z.Z0. +Register Zpos as num.Z.Zpos. +Register Zneg as num.Z.Zneg. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index edbae6534a..001e1cfb01 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -237,6 +237,8 @@ Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) "in" hyp(i Definition fix_proto {A : Type} (a : A) := a. +Register fix_proto as program.tactic.fix_proto. + Ltac destruct_rec_calls := match goal with | [ H : fix_proto _ |- _ ] => destruct_calls H ; clear H @@ -331,3 +333,5 @@ Ltac program_simpl := program_simplify ; try typeclasses eauto 10 with program ; Obligation Tactic := program_simpl. Definition obligation (A : Type) {a : A} := a. + +Register obligation as program.tactics.obligation. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 6278798543..8479b9a2bb 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -32,6 +32,8 @@ Section Well_founded. Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x). + Register Fix_sub as program.wf.fix_sub. + (* Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *) *) (* Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x). *) @@ -89,6 +91,8 @@ Section Measure_well_founded. Definition MR (x y: T): Prop := R (m x) (m y). + Register MR as program.wf.mr. + Lemma measure_wf: well_founded MR. Proof with auto. unfold well_founded. diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index af06bcf47e..43c8d9bc09 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -17,6 +17,8 @@ Export Morphisms.ProperNotations. Definition Setoid_Theory := @Equivalence. Definition Build_Setoid_Theory := @Build_Equivalence. +Register Build_Setoid_Theory as plugins.setoid_ring.Build_Setoid_Theory. + Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x. Proof. unfold Setoid_Theory in s. intros ; reflexivity. diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 3f676c1888..d1168694b2 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -20,6 +20,8 @@ Require Import Bool BinPos BinNat PeanoNat Nnat. Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool). +Register Ascii as plugins.syntax.Ascii. + Declare Scope char_scope. Declare ML Module "ascii_syntax_plugin". Delimit Scope char_scope with char. diff --git a/theories/Strings/String.v b/theories/Strings/String.v index b27474ef25..f6cc8c99ed 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -30,6 +30,9 @@ Delimit Scope string_scope with string. Bind Scope string_scope with string. Local Open Scope string_scope. +Register EmptyString as plugins.syntax.EmptyString. +Register String as plugins.syntax.String. + (** Equality is decidable *) Definition string_dec : forall s1 s2 : string, {s1 = s2} + {s1 <> s2}. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 1241345338..8fc3ab56c9 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -38,6 +38,14 @@ Module Z Include BinIntDef.Z. +Register add as num.Z.add. +Register opp as num.Z.opp. +Register succ as num.Z.succ. +Register pred as num.Z.pred. +Register sub as num.Z.sub. +Register mul as num.Z.mul. +Register of_nat as num.Z.of_nat. + (** When including property functors, only inline t eq zero one two *) Set Inline Level 30. @@ -68,6 +76,11 @@ Notation "( x | y )" := (divide x y) (at level 0). Definition Even a := exists b, a = 2*b. Definition Odd a := exists b, a = 2*b+1. +Register le as num.Z.le. +Register lt as num.Z.lt. +Register ge as num.Z.ge. +Register gt as num.Z.gt. + (** * Decidability of equality. *) Definition eq_dec (x y : Z) : {x = y} + {x <> y}. @@ -477,6 +490,10 @@ Qed. Include ZBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. +Register eq_decidable as num.Z.eq_decidable. +Register le_decidable as num.Z.le_decidable. +Register lt_decidable as num.Z.lt_decidable. + (** ** Specification of absolute value *) @@ -1752,6 +1769,8 @@ weak_Zmult_plus_distr_r (now Z.mul_add_distr_pos) Definition Zne (x y:Z) := x <> y. (* TODO : to remove someday ? *) +Register Zne as plugins.omega.Zne. + Ltac elim_compare com1 com2 := case (Dcompare (com1 ?= com2)%Z); [ idtac | let x := fresh "H" in diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index 5c960da1fb..776efa2978 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -609,6 +609,8 @@ Proof. destruct n. trivial. simpl. apply Pos2Z.inj_succ. Qed. +Register inj_succ as num.Nat2Z.inj_succ. + (** [Z.of_N] produce non-negative integers *) Lemma is_nonneg n : 0 <= Z.of_nat n. @@ -676,11 +678,15 @@ Proof. now rewrite <- !nat_N_Z, Nat2N.inj_add, N2Z.inj_add. Qed. +Register inj_add as num.Nat2Z.inj_add. + Lemma inj_mul n m : Z.of_nat (n*m) = Z.of_nat n * Z.of_nat m. Proof. now rewrite <- !nat_N_Z, Nat2N.inj_mul, N2Z.inj_mul. Qed. +Register inj_mul as num.Nat2Z.inj_mul. + Lemma inj_sub_max n m : Z.of_nat (n-m) = Z.max 0 (Z.of_nat n - Z.of_nat m). Proof. now rewrite <- !nat_N_Z, Nat2N.inj_sub, N2Z.inj_sub_max. @@ -692,6 +698,8 @@ Proof. now rewrite <- !nat_N_Z, Nat2N.inj_sub, N2Z.inj_sub. Qed. +Register inj_sub as num.Nat2Z.inj_sub. + Lemma inj_pred_max n : Z.of_nat (Nat.pred n) = Z.max 0 (Z.pred (Z.of_nat n)). Proof. now rewrite <- !nat_N_Z, Nat2N.inj_pred, N2Z.inj_pred_max. @@ -951,6 +959,14 @@ Definition inj_lt n m := proj1 (Nat2Z.inj_lt n m). Definition inj_ge n m := proj1 (Nat2Z.inj_ge n m). Definition inj_gt n m := proj1 (Nat2Z.inj_gt n m). +Register neq as plugins.omega.neq. +Register inj_eq as plugins.omega.inj_eq. +Register inj_neq as plugins.omega.inj_neq. +Register inj_le as plugins.omega.inj_le. +Register inj_lt as plugins.omega.inj_lt. +Register inj_ge as plugins.omega.inj_ge. +Register inj_gt as plugins.omega.inj_gt. + (** For the others, a Notation is fine *) Notation inj_0 := Nat2Z.inj_0 (only parsing). @@ -1017,3 +1033,5 @@ Theorem inj_minus2 : forall n m:nat, (m > n)%nat -> Z.of_nat (n - m) = 0. Proof. intros. rewrite not_le_minus_0; auto with arith. Qed. + +Register inj_minus2 as plugins.omega.inj_minus2. diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index 208e84aeb7..bd460f77f0 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -64,6 +64,11 @@ Proof. apply Z.lt_gt_cases. Qed. +Register dec_Zne as plugins.omega.dec_Zne. +Register dec_Zgt as plugins.omega.dec_Zgt. +Register dec_Zge as plugins.omega.dec_Zge. +Register not_Zeq as plugins.omega.not_Zeq. + (** * Relating strict and large orders *) Notation Zgt_lt := Z.gt_lt (compat "8.7"). @@ -119,6 +124,12 @@ Proof. destruct (Z.eq_decidable n m); [assumption|now elim H]. Qed. +Register Znot_le_gt as plugins.omega.Znot_le_gt. +Register Znot_lt_ge as plugins.omega.Znot_lt_ge. +Register Znot_ge_lt as plugins.omega.Znot_ge_lt. +Register Znot_gt_le as plugins.omega.Znot_gt_le. +Register not_Zne as plugins.omega.not_Zne. + (** * Equivalence and order properties *) (** Reflexivity *) diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v index 306a856381..fd357502d2 100644 --- a/theories/ZArith/auxiliary.v +++ b/theories/ZArith/auxiliary.v @@ -94,3 +94,10 @@ Proof. now apply Z.add_lt_mono_l. Qed. +Register Zegal_left as plugins.omega.Zegal_left. +Register Zne_left as plugins.omega.Zne_left. +Register Zlt_left as plugins.omega.Zlt_left. +Register Zgt_left as plugins.omega.Zgt_left. +Register Zle_left as plugins.omega.Zle_left. +Register Zge_left as plugins.omega.Zge_left. +Register Zmult_le_approx as plugins.omega.Zmult_le_approx. diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index dee7541d37..148d4437fa 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -62,29 +62,23 @@ exception NoDecidabilityCoInductive exception ConstructorWithNonParametricInductiveType of inductive exception DecidabilityIndicesNotSupported -let constr_of_global g = lazy (UnivGen.constr_of_global g) - (* Some pre declaration of constant we are going to use *) -let bb = constr_of_global Coqlib.glob_bool - -let andb_prop = fun _ -> UnivGen.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_prop +let andb_prop = fun _ -> UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.andb_prop") let andb_true_intro = fun _ -> UnivGen.constr_of_global - (Coqlib.build_bool_type()).Coqlib.andb_true_intro - -let tt = constr_of_global Coqlib.glob_true - -let ff = constr_of_global Coqlib.glob_false - -let eq = constr_of_global Coqlib.glob_eq - -let sumbool () = UnivGen.constr_of_global (Coqlib.build_coq_sumbool ()) + (Coqlib.lib_ref "core.bool.andb_true_intro") -let andb = fun _ -> UnivGen.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb +(* We avoid to use lazy as the binding of constants can change *) +let bb () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.type") +let tt () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.true") +let ff () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.false") +let eq () = UnivGen.constr_of_global (Coqlib.lib_ref "core.eq.type") -let induct_on c = induction false None c None None +let sumbool () = UnivGen.constr_of_global (Coqlib.lib_ref "core.sumbool.type") +let andb = fun _ -> UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.andb") +let induct_on c = induction false None c None None let destruct_on c = destruct false None c None None let destruct_on_using c id = @@ -119,7 +113,7 @@ let mkFullInd (ind,u) n = else mkIndU (ind,u) let check_bool_is_defined () = - try let _ = Global.type_of_global_in_context (Global.env ()) Coqlib.glob_bool in () + try let _ = Global.type_of_global_in_context (Global.env ()) Coqlib.(lib_ref "core.bool.type") in () with e when CErrors.noncritical e -> raise (UndefinedCst "bool") let check_no_indices mib = @@ -160,7 +154,7 @@ let build_beq_scheme mode kn = let eqs_typ = List.map (fun aa -> let a = lift !lift_cnt aa in incr lift_cnt; - myArrow a (myArrow a (Lazy.force bb)) + myArrow a (myArrow a (bb ())) ) ext_rel_list in let eq_input = List.fold_left2 @@ -259,7 +253,7 @@ let build_beq_scheme mode kn = List.fold_left (fun a b -> mkLambda(Anonymous,b,a)) (mkLambda (Anonymous, mkFullInd ind (n+3+(List.length rettyp_l)+nb_ind-1), - (Lazy.force bb))) + (bb ()))) (List.rev rettyp_l) in (* make_one_eq *) (* do the [| C1 ... => match Y with ... end @@ -270,17 +264,17 @@ let build_beq_scheme mode kn = Context.Rel.to_extended_list mkRel (n+nb_ind-1) mib.mind_params_ctxt)) in let constrsi = constrs (3+nparrec) in let n = Array.length constrsi in - let ar = Array.make n (Lazy.force ff) in + let ar = Array.make n (ff ()) in let eff = ref Safe_typing.empty_private_constants in for i=0 to n-1 do let nb_cstr_args = List.length constrsi.(i).cs_args in - let ar2 = Array.make n (Lazy.force ff) in + let ar2 = Array.make n (ff ()) in let constrsj = constrs (3+nparrec+nb_cstr_args) in for j=0 to n-1 do if Int.equal i j then ar2.(j) <- let cc = (match nb_cstr_args with - | 0 -> Lazy.force tt - | _ -> let eqs = Array.make nb_cstr_args (Lazy.force tt) in + | 0 -> tt () + | _ -> let eqs = Array.make nb_cstr_args (tt ()) in for ndx = 0 to nb_cstr_args-1 do let cc = RelDecl.get_type (List.nth constrsi.(i).cs_args ndx) in let eqA, eff' = compute_A_equality rel_list @@ -305,7 +299,7 @@ let build_beq_scheme mode kn = (constrsj.(j).cs_args) ) else ar2.(j) <- (List.fold_left (fun a decl -> - mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) (Lazy.force ff) (constrsj.(j).cs_args) ) + mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) (ff ()) (constrsj.(j).cs_args) ) done; ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) @@ -326,7 +320,7 @@ let build_beq_scheme mode kn = for i=0 to (nb_ind-1) do names.(i) <- Name (Id.of_string (rec_name i)); types.(i) <- mkArrow (mkFullInd ((kn,i),u) 0) - (mkArrow (mkFullInd ((kn,i),u) 1) (Lazy.force bb)); + (mkArrow (mkFullInd ((kn,i),u) 1) (bb ())); let c, eff' = make_one_eq i in cores.(i) <- c; eff := Safe_typing.concat_private eff' !eff @@ -570,15 +564,15 @@ let compute_bl_goal ind lnamesparrec nparrec = mkNamedProd x (mkVar s) ( mkNamedProd y (mkVar s) ( mkArrow - ( mkApp(Lazy.force eq,[|(Lazy.force bb);mkApp(mkVar seq,[|mkVar x;mkVar y|]);(Lazy.force tt)|])) - ( mkApp(Lazy.force eq,[|mkVar s;mkVar x;mkVar y|])) + ( mkApp(eq (),[|bb (); mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt () |])) + ( mkApp(eq (),[|mkVar s;mkVar x;mkVar y|])) )) ) list_id in let bl_input = List.fold_left2 ( fun a (s,_,sbl,_) b -> mkNamedProd sbl b a ) c (List.rev list_id) (List.rev bl_typ) in let eqs_typ = List.map (fun (s,_,_,_) -> - mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,(Lazy.force bb))) + mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,(bb ()))) ) list_id in let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b -> mkNamedProd seq b a @@ -594,8 +588,8 @@ let compute_bl_goal ind lnamesparrec nparrec = mkNamedProd n (mkFullInd (ind,u) nparrec) ( mkNamedProd m (mkFullInd (ind,u) (nparrec+1)) ( mkArrow - (mkApp(Lazy.force eq,[|(Lazy.force bb);mkApp(eqI,[|mkVar n;mkVar m|]);(Lazy.force tt)|])) - (mkApp(Lazy.force eq,[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|])) + (mkApp(eq (),[|bb ();mkApp(eqI,[|mkVar n;mkVar m|]);tt ()|])) + (mkApp(eq (),[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|])) ))), eff let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = @@ -651,7 +645,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). | App (c,ca) -> ( match EConstr.kind sigma c with | Ind (indeq, u) -> - if GlobRef.equal (IndRef indeq) Coqlib.glob_eq + if GlobRef.equal (IndRef indeq) Coqlib.(lib_ref "core.eq.type") then Tacticals.New.tclTHEN (do_replace_bl mode bl_scheme_key ind @@ -704,7 +698,7 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind let compute_lb_goal ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in - let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in + let eq = eq () and tt = tt () and bb = bb () in let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in let eqI, eff = eqI ind lnamesparrec in let create_input c = @@ -827,13 +821,13 @@ let _ = lb_scheme_kind_aux := fun () -> lb_scheme_kind (* Decidable equality *) let check_not_is_defined () = - try ignore (Coqlib.build_coq_not ()) - with e when CErrors.noncritical e -> raise (UndefinedCst "not") + try ignore (Coqlib.lib_ref "core.not.type") + with Not_found -> raise (UndefinedCst "not") (* {n=m}+{n<>m} part *) let compute_dec_goal ind lnamesparrec nparrec = check_not_is_defined (); - let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in + let eq = eq () and tt = tt () and bb = bb () in let list_id = list_id lnamesparrec in let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in let create_input c = @@ -879,14 +873,14 @@ let compute_dec_goal ind lnamesparrec nparrec = create_input ( mkNamedProd n (mkFullInd ind (2*nparrec)) ( mkNamedProd m (mkFullInd ind (2*nparrec+1)) ( - mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_global @@ Coqlib.build_coq_not(),[|eqnm|])|]) + mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.not.type",[|eqnm|])|]) ) ) ) let compute_dec_tact ind lnamesparrec nparrec = - let eq = Lazy.force eq and tt = Lazy.force tt - and ff = Lazy.force ff and bb = Lazy.force bb in + let eq = eq () and tt = tt () + and ff = ff () and bb = bb () in let list_id = list_id lnamesparrec in let eqI, eff = eqI ind lnamesparrec in let avoid = ref [] in @@ -949,7 +943,7 @@ let compute_dec_tact ind lnamesparrec nparrec = let freshH3 = fresh_id (Id.of_string "H") gl in Tacticals.New.tclTHENLIST [ simplest_right ; - unfold_constr (Lazy.force Coqlib.coq_not_ref); + unfold_constr (Coqlib.lib_ref "core.not.type"); intro; Equality.subst_all (); assert_by (Name freshH3) diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 04cd4173a8..5f340dc144 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -160,14 +160,8 @@ type recursive_preentry = (* Wellfounded definition *) -let contrib_name = "Program" -let subtac_dir = [contrib_name] -let tactics_module = subtac_dir @ ["Tactics"] - -let init_constant dir s sigma = - Evarutil.new_global sigma (Coqlib.coq_reference "Command" dir s) - -let fix_proto = init_constant tactics_module "fix_proto" +let fix_proto sigma = + Evarutil.new_global sigma (Coqlib.lib_ref "program.tactic.fix_proto") let interp_recursive ~program_mode ~cofix fixl notations = let open Context.Named.Declaration in diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 102a98f046..c33e6b72c6 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -23,27 +23,16 @@ module RelDecl = Context.Rel.Declaration open Coqlib -let contrib_name = "Program" -let subtac_dir = [contrib_name] -let fixsub_module = subtac_dir @ ["Wf"] -(* let tactics_module = subtac_dir @ ["Tactics"] *) +let init_constant sigma rf = Evarutil.new_global sigma rf +let fix_sub_ref () = lib_ref "program.wf.fix_sub" +let measure_on_R_ref () = lib_ref "program.wf.mr" +let well_founded sigma = init_constant sigma (lib_ref "core.wf.well_founded") -let init_reference dir s () = Coqlib.coq_reference "Command" dir s -let init_constant dir s sigma = - Evarutil.new_global sigma (Coqlib.coq_reference "Command" dir s) - -let make_ref l s = init_reference l s -(* let fix_proto = init_constant tactics_module "fix_proto" *) -let fix_sub_ref = make_ref fixsub_module "Fix_sub" -let measure_on_R_ref = make_ref fixsub_module "MR" -let well_founded = init_constant ["Init"; "Wf"] "well_founded" let mkSubset sigma name typ prop = let open EConstr in let sigma, app_h = Evarutil.new_global sigma (delayed_force build_sigma).typ in sigma, mkApp (app_h, [| typ; mkLambda (name, typ, prop) |]) -let sigT = Lazy.from_fun build_sigma_type - let make_qref s = qualid_of_string s let lt_ref = make_qref "Init.Peano.lt" @@ -60,8 +49,8 @@ let rec telescope sigma l = (fun (sigma, ty, tys, (k, constr)) decl -> let t = RelDecl.get_type decl in let pred = mkLambda (RelDecl.get_name decl, t, ty) in - let sigma, ty = Evarutil.new_global sigma (Lazy.force sigT).typ in - let sigma, intro = Evarutil.new_global sigma (Lazy.force sigT).intro in + let sigma, ty = Evarutil.new_global sigma (lib_ref "core.sigT.type") in + let sigma, intro = Evarutil.new_global sigma (lib_ref "core.sigT.intro") in let sigty = mkApp (ty, [|t; pred|]) in let intro = mkApp (intro, [|lift k t; lift k pred; mkRel k; constr|]) in (sigma, sigty, pred :: tys, (succ k, intro))) @@ -70,8 +59,8 @@ let rec telescope sigma l = let sigma, last, subst = List.fold_right2 (fun pred decl (sigma, prev, subst) -> let t = RelDecl.get_type decl in - let sigma, p1 = Evarutil.new_global sigma (Lazy.force sigT).proj1 in - let sigma, p2 = Evarutil.new_global sigma (Lazy.force sigT).proj2 in + let sigma, p1 = Evarutil.new_global sigma (lib_ref "core.sigT.proj1") in + let sigma, p2 = Evarutil.new_global sigma (lib_ref "core.sigT.proj2") in let proj1 = applist (p1, [t; pred; prev]) in let proj2 = applist (p2, [t; pred; prev]) in (sigma, lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst)) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 895737b538..d7229d32fe 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -212,7 +212,7 @@ GRAMMAR EXTEND Gram | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; l = LIST1 identref SEP "," -> { VernacCombinedScheme (id, l) } | IDENT "Register"; g = global; "as"; quid = qualid -> - { VernacRegister(g, RegisterRetroknowledge quid) } + { VernacRegister(g, RegisterCoqlib quid) } | IDENT "Register"; IDENT "Inline"; g = global -> { VernacRegister(g, RegisterInline) } | IDENT "Universe"; l = LIST1 identref -> { VernacUniverse l } @@ -994,7 +994,9 @@ GRAMMAR EXTEND Gram | IDENT "Transparent"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (false, true, qid) } | IDENT "All"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (true, true, qid) } | IDENT "Strategy"; qid = smart_global -> { PrintStrategy (Some qid) } - | IDENT "Strategies" -> { PrintStrategy None } ] ] + | IDENT "Strategies" -> { PrintStrategy None } + | IDENT "Registered" -> { PrintRegistered } + ] ] ; class_rawexpr: [ [ IDENT "Funclass" -> { FunClass } diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index b354ad0521..5f2818c12b 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -451,11 +451,11 @@ let fold_left' f = function [] -> invalid_arg "fold_left'" | hd :: tl -> List.fold_left f hd tl -let mk_coq_and sigma = Evarutil.new_global sigma (Coqlib.build_coq_and ()) -let mk_coq_conj sigma = Evarutil.new_global sigma (Coqlib.build_coq_conj ()) +let mk_coq_and sigma = Evarutil.new_global sigma (Coqlib.lib_ref "core.and.type") +let mk_coq_conj sigma = Evarutil.new_global sigma (Coqlib.lib_ref "core.and.conj") -let mk_coq_prod sigma = Evarutil.new_global sigma (Coqlib.build_coq_prod ()) -let mk_coq_pair sigma = Evarutil.new_global sigma (Coqlib.build_coq_pair ()) +let mk_coq_prod sigma = Evarutil.new_global sigma (Coqlib.lib_ref "core.prod.type") +let mk_coq_pair sigma = Evarutil.new_global sigma (Coqlib.lib_ref "core.prod.intro") let build_combined_scheme env schemes = let evdref = ref (Evd.from_env env) in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index c4a10b4be6..757a56d436 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -256,11 +256,9 @@ let eterm_obligations env name evm fs ?status t ty = let evmap f c = pi1 (subst_evar_constr evts 0 f c) in Array.of_list (List.rev evars), (evnames, evmap), t', ty -let tactics_module = ["Program";"Tactics"] -let safe_init_constant md name () = - Coqlib.check_required_library ("Coq"::md); - UnivGen.constr_of_global (Coqlib.coq_reference "Obligations" md name) -let hide_obligation = safe_init_constant tactics_module "obligation" +let hide_obligation () = + Coqlib.check_required_library ["Coq";"Program";"Tactics"]; + UnivGen.constr_of_global (Coqlib.lib_ref "program.tactics.obligation") let pperror cmd = CErrors.user_err ~hdr:"Program" cmd let error s = pperror (str s) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index b4b3aead91..a0e8f38c0b 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -533,6 +533,8 @@ open Pputils keyword "Print Strategies" | PrintStrategy (Some qid) -> keyword "Print Strategy" ++ pr_smart_global qid + | PrintRegistered -> + keyword "Print Registered" let pr_using e = let rec aux = function @@ -1159,14 +1161,16 @@ open Pputils | LocateOther (s, qid) -> keyword s ++ spc () ++ pr_ltac_ref qid in return (keyword "Locate" ++ spc() ++ pr_locate loc) - | VernacRegister (id, RegisterInline) -> + | VernacRegister (qid, RegisterCoqlib name) -> return ( hov 2 - (keyword "Register Inline" ++ spc() ++ pr_qualid id) + (keyword "Register" ++ spc() ++ pr_qualid qid ++ spc () ++ str "as" + ++ spc () ++ pr_qualid name) ) - | VernacRegister (id, RegisterRetroknowledge n) -> + | VernacRegister (qid, RegisterInline) -> return ( - hov 2 (keyword "Register" ++ spc () ++ pr_qualid id ++ spc () ++ keyword "as" ++ pr_qualid n) + hov 2 + (keyword "Register Inline" ++ spc() ++ pr_qualid qid) ) | VernacComments l -> return ( diff --git a/vernac/search.ml b/vernac/search.ml index e8ccec11ca..04dcb7d565 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -236,13 +236,13 @@ let search_pattern gopt pat mods pr_search = (** SearchRewrite *) -let eq = Coqlib.glob_eq +let eq () = Coqlib.(lib_ref "core.eq.type") let rewrite_pat1 pat = - PApp (PRef eq, [| PMeta None; pat; PMeta None |]) + PApp (PRef (eq ()), [| PMeta None; pat; PMeta None |]) let rewrite_pat2 pat = - PApp (PRef eq, [| PMeta None; PMeta None; pat |]) + PApp (PRef (eq ()), [| PMeta None; PMeta None; pat |]) let search_rewrite gopt pat mods pr_search = let pat1 = rewrite_pat1 pat in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index cf2fecb9c1..76f42db34d 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -311,6 +311,13 @@ let print_strategy r = let lvl = get_strategy oracle key in pr_strategy (r, lvl) +let print_registered () = + let pr_lib_ref (s,r) = + pr_global r ++ str " registered as " ++ str s + in + hov 0 (prlist_with_sep fnl pr_lib_ref @@ Coqlib.get_lib_refs ()) + + let dump_universes_gen g s = let output = open_out s in let output_constraint, close = @@ -1866,6 +1873,7 @@ let vernac_print ~atts env sigma = Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in Printer.pr_assumptionset env sigma nassums | PrintStrategy r -> print_strategy r + | PrintRegistered -> print_registered () let global_module qid = try Nametab.full_name_module qid @@ -1972,14 +1980,14 @@ let vernac_register qid r = if not (isConstRef gr) then user_err Pp.(str "Register inline: a constant is expected"); Global.register_inline (destConstRef gr) - | RegisterRetroknowledge n -> + | RegisterCoqlib n -> let path, id = Libnames.repr_qualid n in if DirPath.equal path Retroknowledge.int31_path then let f = Retroknowledge.(KInt31 (int31_field_of_string (Id.to_string id))) in Global.register f gr else - user_err Pp.(str "Register in unknown namespace: " ++ str (DirPath.to_string path)) + Coqlib.register_ref (Libnames.string_of_qualid n) gr (********************) (* Proof management *) @@ -2226,7 +2234,7 @@ let interp ?proof ~atts ~st c = | VernacSearch (s,g,r) -> vernac_search ~atts s g r | VernacLocate l -> Feedback.msg_notice @@ vernac_locate l - | VernacRegister (id, r) -> vernac_register id r + | VernacRegister (qid, r) -> vernac_register qid r | VernacComments l -> Flags.if_verbose Feedback.msg_info (str "Comments ok\n") (* Proof management *) @@ -2278,6 +2286,7 @@ let check_vernac_supports_locality c l = | VernacSetOption _ | VernacUnsetOption _ | VernacDeclareReduction _ | VernacExtend _ + | VernacRegister _ | VernacInductive _) -> () | Some _, _ -> user_err Pp.(str "This command does not support Locality") diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index a2ea706b75..27b485d94d 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -57,6 +57,7 @@ type printable = | PrintImplicit of qualid or_by_notation | PrintAssumptions of bool * bool * qualid or_by_notation | PrintStrategy of qualid or_by_notation option + | PrintRegistered type search_about_item = | SearchSubPattern of constr_pattern_expr @@ -230,7 +231,7 @@ type extend_name = It will be extended with primitive inductive types and operators *) type register_kind = | RegisterInline - | RegisterRetroknowledge of qualid + | RegisterCoqlib of qualid (** {6 Types concerning the module layer} *) |