From 5cc13770ac2358d583b21f217b8c65d2d5abd850 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 24 May 2017 19:57:06 +0200 Subject: [coqlib] Move `Coqlib` to `library/`. We move Coqlib to library in preparation for the late binding of Gallina-level references. Placing `Coqlib` in `library/` is convenient as some components such as pretyping need to depend on it. By moving we lose the ability to locate references by syntactic abbreviations, but IMHO it makes to require ML code to refer to a true constant instead of an abbreviation/notation. Unfortunately this change means that we break the `Coqlib` API (providing a compatibility function is not possible), however we do so for a good reason. The main changes are: - move `Coqlib` to `library/`. - remove reference -> term from `Coqlib`. In particular, clients will have different needs with regards to universes/evar_maps, so we force them to call the (not very safe) `Universes.constr_of_global` explicitly so the users are marked. - move late binding of impossible case from `Termops` to `pretying/Evarconv`. Remove hook. - `Coqlib.find_reference` doesn't support syntactic abbreviations anymore. - remove duplication of `Coqlib` code in `Program`. - remove duplication of `Coqlib` code in `Ltac.Rewrite`. - A special note about bug 5066 and commit 6e87877 . This case illustrates the danger of duplication in the code base; the solution chosen there was to transform the not-found anomaly into an error message, however the general policy was far from clear. The long term solution is indeed make `find_reference` emit `Not_found` and let the client handle the error maybe non-fatally. (so they can test for constants. --- dev/ci/ci-user-overlay.sh | 6 +- dev/doc/changes.txt | 13 + engine/termops.ml | 22 -- engine/termops.mli | 4 - interp/coqlib.ml | 399 ------------------------- interp/coqlib.mli | 214 ------------- interp/interp.mllib | 1 - library/coqlib.ml | 383 ++++++++++++++++++++++++ library/coqlib.mli | 211 +++++++++++++ library/library.mllib | 1 + plugins/fourier/fourierR.ml | 6 +- plugins/funind/functional_principles_proofs.ml | 8 +- plugins/funind/indfun_common.ml | 3 +- plugins/funind/invfun.ml | 2 +- plugins/funind/recdef.ml | 6 +- plugins/ltac/extratactics.ml4 | 5 +- plugins/ltac/rewrite.ml | 28 +- plugins/micromega/coq_micromega.ml | 29 +- plugins/nsatz/nsatz.ml | 2 +- plugins/omega/coq_omega.ml | 2 +- plugins/romega/const_omega.ml | 10 +- plugins/setoid_ring/newring.ml | 4 +- pretyping/cases.ml | 1 - pretyping/evarconv.ml | 27 +- pretyping/evarconv.mli | 2 + pretyping/program.ml | 19 +- tactics/contradiction.ml | 4 +- tactics/eqdecide.ml | 4 +- tactics/equality.ml | 6 +- vernac/auto_ind_decl.ml | 9 +- vernac/indschemes.ml | 3 +- 31 files changed, 707 insertions(+), 727 deletions(-) delete mode 100644 interp/coqlib.ml delete mode 100644 interp/coqlib.mli create mode 100644 library/coqlib.ml create mode 100644 library/coqlib.mli diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index 1f7fbcbf6..bfa43cde1 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -25,8 +25,10 @@ echo $TRAVIS_PULL_REQUEST echo $TRAVIS_BRANCH echo $TRAVIS_COMMIT -if [ $TRAVIS_PULL_REQUEST == "481" ] || [ $TRAVIS_BRANCH == "options+remove_non_sync" ]; then - mathcomp_CI_BRANCH=options+remove_non_sync +if [ $TRAVIS_PULL_REQUEST == "678" ] || [ $TRAVIS_BRANCH == "coqlib-part-02" ]; then + + mathcomp_CI_BRANCH=coqlib-part-02 mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git + fi diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index d52c18462..bb6c2f660 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -108,6 +108,19 @@ In GOption: passed to workers, etc... As a consequence, the field `Goptions.optsync` has been removed. +In Coqlib / reference location: + + We have removed from Coqlib functions returning `constr` from + names. Now it is only possible to obtain references, that must be + processed wrt the particular needs of the client. + + Users of `coq_constant/gen_constant` can do + `Universes.constr_of_global (find_reference dir r)` _however_ note + the warnings in the `Universes.constr_of_global` in the + documentation. It is very likely that you were previously suffering + from problems with polymorphic universes due to using + `Coqlib.coq_constant` that used to do this. + ** Tactic API ** - pf_constr_of_global now returns a tactic instead of taking a continuation. diff --git a/engine/termops.ml b/engine/termops.ml index 19e62f8e6..ca32c06a7 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1468,25 +1468,3 @@ let env_rel_context_chop k env = let ctx1,ctx2 = List.chop k rels in push_rel_context ctx2 (reset_with_named_context (named_context_val env) env), ctx1 - -(*******************************************) -(* Functions to deal with impossible cases *) -(*******************************************) -let impossible_default_case = ref None - -let set_impossible_default_clause c = impossible_default_case := Some c - -let coq_unit_judge = - let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in - let na1 = Name (Id.of_string "A") in - let na2 = Name (Id.of_string "H") in - fun () -> - match !impossible_default_case with - | Some fn -> - let (id,type_of_id), ctx = fn () in - make_judge id type_of_id, ctx - | None -> - (* In case the constants id/ID are not defined *) - make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1))) - (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2))), - Univ.ContextSet.empty diff --git a/engine/termops.mli b/engine/termops.mli index fe6dfb0ce..58837ba03 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -275,10 +275,6 @@ val on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) puns val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment -(** {6 Functions to deal with impossible cases } *) -val set_impossible_default_clause : (unit -> (Constr.constr * Constr.types) Univ.in_universe_context_set) -> unit -val coq_unit_judge : unit -> unsafe_judgment Univ.in_universe_context_set - (** {5 Debug pretty-printers} *) open Evd diff --git a/interp/coqlib.ml b/interp/coqlib.ml deleted file mode 100644 index 9105bdd54..000000000 --- a/interp/coqlib.ml +++ /dev/null @@ -1,399 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - anomaly ~label:locstr (str "cannot find " ++ Libnames.pr_path sp) - -let coq_reference locstr dir s = find_reference locstr (coq::dir) s - -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 - -let global_of_extended q = - try Some (global_of_extended_global q) with Not_found -> None - -let gen_reference_in_modules locstr dirs s = - let dirs = List.map make_dir dirs in - let qualid = qualid_of_string s in - let all = Nametab.locate_extended_all qualid in - let all = List.map_filter global_of_extended all in - let all = List.sort_uniquize RefOrdered_env.compare all in - let these = List.filter (has_suffix_in_dirs dirs) all in - match these with - | [x] -> x - | [] -> - anomaly ~label:locstr (str "cannot find " ++ str s ++ - str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ - prlist_with_sep pr_comma pr_dirpath dirs) - | l -> - anomaly ~label:locstr - (str "ambiguous name " ++ str s ++ str " can represent " ++ - prlist_with_sep pr_comma - (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++ - str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ - prlist_with_sep pr_comma pr_dirpath dirs) - -let gen_constant_in_modules locstr dirs s = - Universes.constr_of_global (gen_reference_in_modules locstr dirs s) - -(* For tactics/commands requiring vernacular libraries *) - -let check_required_library d = - let dir = make_dir d in - if Library.library_is_loaded dir then () - else - let in_current_dir = match Lib.current_mp () with - | MPfile dp -> DirPath.equal dir dp - | _ -> 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 " ++ pr_dirpath 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 init_constant dir s = - let d = coq::"Init"::dir in - check_required_library d; Universes.constr_of_global @@ 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 - -let arith_dir = [coq;"Arith"] -let arith_modules = [arith_dir] - -let numbers_dir = [coq;"Numbers"] -let parith_dir = [coq;"PArith"] -let narith_dir = [coq;"NArith"] -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"]; - init_dir@["Specif"]; - init_dir@["Logic_Type"]; - init_dir@["Nat"]; - init_dir@["Peano"]; - 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 = make_dir logic_module_name - -let logic_type_module_name = init_dir@["Logic_Type"] -let logic_type_module = make_dir logic_type_module_name - -let datatypes_module_name = init_dir@["Datatypes"] -let datatypes_module = make_dir datatypes_module_name - -let jmeq_module_name = [coq;"Logic";"JMeq"] -let jmeq_module = make_dir jmeq_module_name - -(* TODO: temporary hack. Works only if the module isn't an alias *) -let make_ind dir id = Globnames.encode_mind dir (Id.of_string id) -let make_con dir id = Globnames.encode_con dir (Id.of_string id) - -(** Identity *) - -let id = make_con datatypes_module "idProp" -let type_of_id = make_con datatypes_module "IDProp" - -let _ = Termops.set_impossible_default_clause - (fun () -> - let c, ctx = Universes.fresh_global_instance (Global.env()) (ConstRef id) in - let (_, u) = destConst c in - (c,mkConstU (type_of_id,u)), ctx) - -(** Natural numbers *) -let nat_kn = make_ind datatypes_module "nat" -let nat_path = Libnames.make_path datatypes_module (Id.of_string "nat") - -let glob_nat = IndRef (nat_kn,0) - -let path_of_O = ((nat_kn,0),1) -let path_of_S = ((nat_kn,0),2) -let glob_O = ConstructRef path_of_O -let glob_S = ConstructRef path_of_S - -(** Booleans *) -let bool_kn = make_ind datatypes_module "bool" - -let glob_bool = IndRef (bool_kn,0) - -let path_of_true = ((bool_kn,0),1) -let path_of_false = ((bool_kn,0),2) -let glob_true = ConstructRef path_of_true -let glob_false = ConstructRef path_of_false - -(** Equality *) -let eq_kn = make_ind logic_module "eq" -let glob_eq = IndRef (eq_kn,0) - -let identity_kn = make_ind datatypes_module "identity" -let glob_identity = IndRef (identity_kn,0) - -let jmeq_kn = make_ind jmeq_module "JMeq" -let glob_jmeq = IndRef (jmeq_kn,0) - -type coq_sigma_data = { - proj1 : global_reference; - proj2 : global_reference; - elim : global_reference; - intro : global_reference; - typ : global_reference } - -type coq_bool_data = { - andb : constr; - andb_prop : constr; - andb_true_intro : constr} - -let build_bool_type () = - { andb = init_constant ["Datatypes"] "andb"; - andb_prop = init_constant ["Datatypes"] "andb_prop"; - andb_true_intro = init_constant ["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" } - -(* Equalities *) -type coq_eq_data = { - eq : global_reference; - ind : global_reference; - refl : global_reference; - sym : global_reference; - trans: global_reference; - congr: global_reference } - -(* Data needed for discriminate and injection *) -type coq_inversion_data = { - inv_eq : global_reference; (* : forall params, t -> Prop *) - inv_ind : global_reference; (* : forall params P y, eq params y -> P y *) - inv_congr: global_reference (* : 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_init_constant dir id = lazy (init_constant 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_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_constant ["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" - -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 } - -(* The False proposition *) -let coq_False = lazy_init_constant ["Logic"] "False" - -(* The True proposition and its unique proof *) -let coq_True = lazy_init_constant ["Logic"] "True" -let coq_I = lazy_init_constant ["Logic"] "I" - -(* Connectives *) -let coq_not = lazy_init_constant ["Logic"] "not" -let coq_and = lazy_init_constant ["Logic"] "and" -let coq_conj = lazy_init_constant ["Logic"] "conj" -let coq_or = lazy_init_constant ["Logic"] "or" -let coq_ex = lazy_init_constant ["Logic"] "ex" -let coq_iff = lazy_init_constant ["Logic"] "iff" - -let coq_iff_left_proj = lazy_init_constant ["Logic"] "proj1" -let coq_iff_right_proj = lazy_init_constant ["Logic"] "proj2" - -(* Runtime part *) -let build_coq_True () = Lazy.force coq_True -let build_coq_I () = Lazy.force coq_I - -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_iff_left_proj () = Lazy.force coq_iff_left_proj -let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj - - -(* 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") - -(* Deprecated *) -let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s) -let gen_reference = coq_reference -let gen_constant = coq_constant - diff --git a/interp/coqlib.mli b/interp/coqlib.mli deleted file mode 100644 index 49802089d..000000000 --- a/interp/coqlib.mli +++ /dev/null @@ -1,214 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* global_reference] - - such that [find_reference "core.eq.type"] returns the proper [global_reference] - - [bind_reference : string -> global_reference -> unit] - - will bind a reference. - - A feature based approach would be possible too. - - Contrary to the old approach of raising an anomaly, we expect - tactics to gracefully fail in the absence of some primitive. - - This is work in progress, see below. -*) - -(** {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 *) - -type message = string - -val find_reference : message -> string list -> string -> global_reference -val coq_reference : message -> string list -> string -> global_reference - -(** For tactics/commands requiring vernacular libraries *) -val check_required_library : string list -> unit - -(** Search in several modules (not prefixed by "Coq") *) -val gen_constant_in_modules : string->string list list-> string -> constr -val gen_reference_in_modules : string->string list list-> string -> global_reference - -val arith_modules : string list list -val zarith_base_modules : string list list -val init_modules : string list list - -(** {6 Global references } *) - -(** Modules *) -val prelude_module : DirPath.t - -val logic_module : DirPath.t -val logic_module_name : string list - -val logic_type_module : DirPath.t - -val jmeq_module : DirPath.t -val jmeq_module_name : string list - -val datatypes_module_name : string list - -(** Natural numbers *) -val nat_path : full_path -val glob_nat : global_reference -val path_of_O : constructor -val path_of_S : constructor -val glob_O : global_reference -val glob_S : global_reference - -(** Booleans *) -val glob_bool : global_reference -val path_of_true : constructor -val path_of_false : constructor -val glob_true : global_reference -val glob_false : global_reference - - -(** Equality *) -val glob_eq : global_reference -val glob_identity : global_reference -val glob_jmeq : global_reference - -(** {6 ... } *) -(** Constructions and patterns related to Coq initial state are unknown - at compile time. Therefore, we can only provide methods to build - them at runtime. This is the purpose of the [constr delayed] and - [constr_pattern delayed] types. Objects of this time needs to be - forced with [delayed_force] to get the actual constr or pattern - at runtime. *) - -type coq_bool_data = { - andb : constr; - andb_prop : constr; - andb_true_intro : constr} -val build_bool_type : coq_bool_data delayed - -(** {6 For Equality tactics } *) -type coq_sigma_data = { - proj1 : global_reference; - proj2 : global_reference; - elim : global_reference; - intro : global_reference; - typ : global_reference } - -val build_sigma_set : coq_sigma_data delayed -val build_sigma_type : coq_sigma_data delayed -val build_sigma : coq_sigma_data delayed - -(* 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 *) - -(** Non-dependent pairs in Set from Datatypes *) -val build_prod : coq_sigma_data delayed - -type coq_eq_data = { - eq : global_reference; - ind : global_reference; - refl : global_reference; - sym : global_reference; - trans: global_reference; - congr: global_reference } - -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 - -val build_coq_eq : global_reference delayed (** = [(build_coq_eq_data()).eq] *) -val build_coq_eq_refl : global_reference delayed (** = [(build_coq_eq_data()).refl] *) -val build_coq_eq_sym : global_reference delayed (** = [(build_coq_eq_data()).sym] *) -val build_coq_f_equal2 : global_reference delayed - -(** Data needed for discriminate and injection *) - -type coq_inversion_data = { - inv_eq : global_reference; (** : forall params, args -> Prop *) - inv_ind : global_reference; (** : forall params P (H : P params) args, eq params args - -> P args *) - inv_congr: global_reference (** : forall params B (f:t->B) args, eq params args -> - f params = f args *) -} - -val build_coq_inversion_eq_data : coq_inversion_data delayed -val build_coq_inversion_identity_data : coq_inversion_data delayed -val build_coq_inversion_jmeq_data : coq_inversion_data delayed -val build_coq_inversion_eq_true_data : coq_inversion_data delayed - -(** Specif *) -val build_coq_sumbool : constr delayed - -(** {6 ... } *) -(** Connectives - The False proposition *) -val build_coq_False : constr delayed - -(** The True proposition and its unique proof *) -val build_coq_True : constr delayed -val build_coq_I : constr delayed - -(** Negation *) -val build_coq_not : constr delayed - -(** Conjunction *) -val build_coq_and : constr delayed -val build_coq_conj : constr delayed -val build_coq_iff : constr delayed - -val build_coq_iff_left_proj : constr delayed -val build_coq_iff_right_proj : constr delayed - -(** Disjunction *) -val build_coq_or : constr delayed - -(** Existential quantifier *) -val build_coq_ex : constr delayed - -val coq_eq_ref : global_reference lazy_t -val coq_identity_ref : global_reference lazy_t -val coq_jmeq_ref : global_reference lazy_t -val coq_eq_true_ref : global_reference lazy_t -val coq_existS_ref : global_reference lazy_t -val coq_existT_ref : global_reference lazy_t -val coq_exist_ref : global_reference lazy_t -val coq_not_ref : global_reference lazy_t -val coq_False_ref : global_reference lazy_t -val coq_sumbool_ref : global_reference lazy_t -val coq_sig_ref : global_reference lazy_t - -val coq_or_ref : global_reference lazy_t -val coq_iff_ref : global_reference lazy_t - -(* Deprecated functions *) -val coq_constant : message -> string list -> string -> constr -[@@ocaml.deprecated "Please use Coqlib.find_reference"] -val gen_constant : message -> string list -> string -> constr -[@@ocaml.deprecated "Please use Coqlib.find_reference"] -val gen_reference : message -> string list -> string -> global_reference -[@@ocaml.deprecated "Please use Coqlib.find_reference"] - diff --git a/interp/interp.mllib b/interp/interp.mllib index 607af82a0..6d290a325 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -14,6 +14,5 @@ Implicit_quantifiers Constrintern Modintern Constrextern -Coqlib Discharge Declare diff --git a/library/coqlib.ml b/library/coqlib.ml new file mode 100644 index 000000000..955ff4c08 --- /dev/null +++ b/library/coqlib.ml @@ -0,0 +1,383 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + (* 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 " ++ Libnames.pr_dirpath dp ++ + str " has to be required first.") + +let coq_reference locstr dir s = find_reference locstr (coq::dir) s + +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 + +let gen_reference_in_modules locstr dirs s = + let dirs = List.map make_dir dirs in + let qualid = qualid_of_string s in + let all = Nametab.locate_all qualid in + let all = List.sort_uniquize RefOrdered_env.compare all in + let these = List.filter (has_suffix_in_dirs dirs) all in + match these with + | [x] -> x + | [] -> + anomaly ~label:locstr (str "cannot find " ++ str s ++ + str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ + prlist_with_sep pr_comma pr_dirpath dirs) + | l -> + anomaly ~label:locstr + (str "ambiguous name " ++ str s ++ str " can represent " ++ + prlist_with_sep pr_comma + (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++ + str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++ + prlist_with_sep pr_comma pr_dirpath dirs) + +(* For tactics/commands requiring vernacular libraries *) + +let check_required_library d = + let dir = make_dir d in + if Library.library_is_loaded dir then () + else + let in_current_dir = match Lib.current_mp () with + | MPfile dp -> DirPath.equal dir dp + | _ -> 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 " ++ pr_dirpath 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 + +let arith_dir = [coq;"Arith"] +let arith_modules = [arith_dir] + +let numbers_dir = [coq;"Numbers"] +let parith_dir = [coq;"PArith"] +let narith_dir = [coq;"NArith"] +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"]; + init_dir@["Specif"]; + init_dir@["Logic_Type"]; + init_dir@["Nat"]; + init_dir@["Peano"]; + 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 = make_dir logic_module_name + +let logic_type_module_name = init_dir@["Logic_Type"] +let logic_type_module = make_dir logic_type_module_name + +let datatypes_module_name = init_dir@["Datatypes"] +let datatypes_module = make_dir datatypes_module_name + +let jmeq_module_name = [coq;"Logic";"JMeq"] +let jmeq_module = make_dir jmeq_module_name + +(* TODO: temporary hack. Works only if the module isn't an alias *) +let make_ind dir id = Globnames.encode_mind dir (Id.of_string id) +let make_con dir id = Globnames.encode_con dir (Id.of_string id) + +(** Identity *) + +let id = make_con datatypes_module "idProp" +let type_of_id = make_con datatypes_module "IDProp" + +(** Natural numbers *) +let nat_kn = make_ind datatypes_module "nat" +let nat_path = Libnames.make_path datatypes_module (Id.of_string "nat") + +let glob_nat = IndRef (nat_kn,0) + +let path_of_O = ((nat_kn,0),1) +let path_of_S = ((nat_kn,0),2) +let glob_O = ConstructRef path_of_O +let glob_S = ConstructRef path_of_S + +(** Booleans *) +let bool_kn = make_ind datatypes_module "bool" + +let glob_bool = IndRef (bool_kn,0) + +let path_of_true = ((bool_kn,0),1) +let path_of_false = ((bool_kn,0),2) +let glob_true = ConstructRef path_of_true +let glob_false = ConstructRef path_of_false + +(** Equality *) +let eq_kn = make_ind logic_module "eq" +let glob_eq = IndRef (eq_kn,0) + +let identity_kn = make_ind datatypes_module "identity" +let glob_identity = IndRef (identity_kn,0) + +let jmeq_kn = make_ind jmeq_module "JMeq" +let glob_jmeq = IndRef (jmeq_kn,0) + +type coq_sigma_data = { + proj1 : global_reference; + proj2 : global_reference; + elim : global_reference; + intro : global_reference; + typ : global_reference } + +type coq_bool_data = { + andb : global_reference; + andb_prop : global_reference; + andb_true_intro : global_reference} + +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" } + +(* Equalities *) +type coq_eq_data = { + eq : global_reference; + ind : global_reference; + refl : global_reference; + sym : global_reference; + trans: global_reference; + congr: global_reference } + +(* Data needed for discriminate and injection *) +type coq_inversion_data = { + inv_eq : global_reference; (* : forall params, t -> Prop *) + inv_ind : global_reference; (* : forall params P y, eq params y -> P y *) + inv_congr: global_reference (* : 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_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" + +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 } + +(* 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" + +(* 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" + +let coq_iff_left_proj = lazy_init_reference ["Logic"] "proj1" +let coq_iff_right_proj = lazy_init_reference ["Logic"] "proj2" + +(* Runtime part *) +let build_coq_True () = Lazy.force coq_True +let build_coq_I () = Lazy.force coq_I + +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_iff_left_proj () = Lazy.force coq_iff_left_proj +let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj + + +(* 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") + +(* Deprecated *) +let gen_reference = coq_reference + diff --git a/library/coqlib.mli b/library/coqlib.mli new file mode 100644 index 000000000..716d97c9d --- /dev/null +++ b/library/coqlib.mli @@ -0,0 +1,211 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* global_reference] + + such that [find_reference "core.eq.type"] returns the proper [global_reference] + + [bind_reference : string -> global_reference -> unit] + + will bind a reference. + + A feature based approach would be possible too. + + Contrary to the old approach of raising an anomaly, we expect + tactics to gracefully fail in the absence of some primitive. + + This is work in progress, see below. +*) + +(** {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 *) + +type message = string + +val find_reference : message -> string list -> string -> global_reference +val coq_reference : message -> string list -> string -> global_reference + +(** For tactics/commands requiring vernacular libraries *) +val check_required_library : string list -> unit + +(** Search in several modules (not prefixed by "Coq") *) +val gen_reference_in_modules : string->string list list-> string -> global_reference + +val arith_modules : string list list +val zarith_base_modules : string list list +val init_modules : string list list + +(** {6 Global references } *) + +(** Modules *) +val prelude_module : DirPath.t + +val logic_module : DirPath.t +val logic_module_name : string list + +val logic_type_module : DirPath.t + +val jmeq_module : DirPath.t +val jmeq_module_name : string list + +val datatypes_module_name : string list + +(** Identity *) +val id : constant +val type_of_id : constant + +(** Natural numbers *) +val nat_path : full_path +val glob_nat : global_reference +val path_of_O : constructor +val path_of_S : constructor +val glob_O : global_reference +val glob_S : global_reference + +(** Booleans *) +val glob_bool : global_reference +val path_of_true : constructor +val path_of_false : constructor +val glob_true : global_reference +val glob_false : global_reference + + +(** Equality *) +val glob_eq : global_reference +val glob_identity : global_reference +val glob_jmeq : global_reference + +(** {6 ... } *) +(** Constructions and patterns related to Coq initial state are unknown + at compile time. Therefore, we can only provide methods to build + them at runtime. This is the purpose of the [constr delayed] and + [constr_pattern delayed] types. Objects of this time needs to be + forced with [delayed_force] to get the actual constr or pattern + at runtime. *) + +type coq_bool_data = { + andb : global_reference; + andb_prop : global_reference; + andb_true_intro : global_reference} +val build_bool_type : coq_bool_data delayed + +(** {6 For Equality tactics } *) +type coq_sigma_data = { + proj1 : global_reference; + proj2 : global_reference; + elim : global_reference; + intro : global_reference; + typ : global_reference } + +val build_sigma_set : coq_sigma_data delayed +val build_sigma_type : coq_sigma_data delayed +val build_sigma : coq_sigma_data delayed + +(* 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 *) + +(** Non-dependent pairs in Set from Datatypes *) +val build_prod : coq_sigma_data delayed + +type coq_eq_data = { + eq : global_reference; + ind : global_reference; + refl : global_reference; + sym : global_reference; + trans: global_reference; + congr: global_reference } + +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 + +val build_coq_eq : global_reference delayed (** = [(build_coq_eq_data()).eq] *) +val build_coq_eq_refl : global_reference delayed (** = [(build_coq_eq_data()).refl] *) +val build_coq_eq_sym : global_reference delayed (** = [(build_coq_eq_data()).sym] *) +val build_coq_f_equal2 : global_reference delayed + +(** Data needed for discriminate and injection *) + +type coq_inversion_data = { + inv_eq : global_reference; (** : forall params, args -> Prop *) + inv_ind : global_reference; (** : forall params P (H : P params) args, eq params args + -> P args *) + inv_congr: global_reference (** : forall params B (f:t->B) args, eq params args -> + f params = f args *) +} + +val build_coq_inversion_eq_data : coq_inversion_data delayed +val build_coq_inversion_identity_data : coq_inversion_data delayed +val build_coq_inversion_jmeq_data : coq_inversion_data delayed +val build_coq_inversion_eq_true_data : coq_inversion_data delayed + +(** Specif *) +val build_coq_sumbool : global_reference delayed + +(** {6 ... } *) +(** Connectives + The False proposition *) +val build_coq_False : global_reference delayed + +(** The True proposition and its unique proof *) +val build_coq_True : global_reference delayed +val build_coq_I : global_reference delayed + +(** Negation *) +val build_coq_not : global_reference delayed + +(** Conjunction *) +val build_coq_and : global_reference delayed +val build_coq_conj : global_reference delayed +val build_coq_iff : global_reference delayed + +val build_coq_iff_left_proj : global_reference delayed +val build_coq_iff_right_proj : global_reference delayed + +(** Disjunction *) +val build_coq_or : global_reference delayed + +(** Existential quantifier *) +val build_coq_ex : global_reference delayed + +val coq_eq_ref : global_reference lazy_t +val coq_identity_ref : global_reference lazy_t +val coq_jmeq_ref : global_reference lazy_t +val coq_eq_true_ref : global_reference lazy_t +val coq_existS_ref : global_reference lazy_t +val coq_existT_ref : global_reference lazy_t +val coq_exist_ref : global_reference lazy_t +val coq_not_ref : global_reference lazy_t +val coq_False_ref : global_reference lazy_t +val coq_sumbool_ref : global_reference lazy_t +val coq_sig_ref : global_reference lazy_t + +val coq_or_ref : global_reference lazy_t +val coq_iff_ref : global_reference lazy_t + +(* Deprecated functions *) +val gen_reference : message -> string list -> string -> global_reference +[@@ocaml.deprecated "Please use Coqlib.find_reference"] diff --git a/library/library.mllib b/library/library.mllib index df4f73503..6f433b77d 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -16,3 +16,4 @@ Goptions Decls Heads Keys +Coqlib diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index d35e4ec6f..5cac3cbaf 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -291,9 +291,9 @@ let constant path s = Universes.constr_of_global @@ (* Standard library *) open Coqlib let coq_sym_eqT = lazy (build_coq_eq_sym ()) -let coq_False = lazy (build_coq_False ()) -let coq_not = lazy (build_coq_not ()) -let coq_eq = lazy (build_coq_eq ()) +let coq_False = lazy (Universes.constr_of_global @@ build_coq_False ()) +let coq_not = lazy (Universes.constr_of_global @@ build_coq_not ()) +let coq_eq = lazy (Universes.constr_of_global @@ build_coq_eq ()) (* Rdefinitions *) let constant_real = constant ["Reals";"Rdefinitions"] diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 55d361e3d..f8c7f98f6 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -409,9 +409,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 (Coqlib.build_coq_False ()) in - let coq_True = EConstr.of_constr (Coqlib.build_coq_True ()) in - let coq_I = EConstr.of_constr (Coqlib.build_coq_I ()) in + let coq_False = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ()) in + let coq_True = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_True ()) in + let coq_I = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_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 @@ -1596,7 +1596,7 @@ let prove_principle_for_gen match !tcc_lemma_ref with | Undefined -> error "No tcc proof !!" | Value lemma -> EConstr.of_constr lemma - | Not_needed -> EConstr.of_constr (Coqlib.build_coq_I ()) + | Not_needed -> EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_I ()) in (* let rec list_diff del_list check_list = *) (* match del_list with *) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 257f02b70..90a082d1e 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -120,7 +120,8 @@ let def_of_const t = |_ -> assert false let coq_constant s = - Coqlib.gen_constant_in_modules "RecursiveDefinition" + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s;; let find_reference sl s = diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 8c972cd7c..8eaa9b0f5 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -546,7 +546,7 @@ and intros_with_rewrite_aux : tactic = intros_with_rewrite ] g end - | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Coqlib.build_coq_False ())) -> + | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ())) -> Proofview.V82.of_tactic tauto g | Case(_,_,v,_) -> tclTHENSEQ[ diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index eabad955e..00020609e 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -54,7 +54,9 @@ let arith_Nat = ["Arith";"PeanoNat";"Nat"] let arith_Lt = ["Arith";"Lt"] let coq_init_constant s = - EConstr.of_constr (Coqlib.gen_constant_in_modules "RecursiveDefinition" Coqlib.init_modules s) + EConstr.of_constr ( + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in @@ -1223,7 +1225,7 @@ let get_current_subgoals_types () = exception EmptySubgoals let build_and_l sigma l = - let and_constr = Coqlib.build_coq_and () in + let and_constr = Universes.constr_of_global @@ Coqlib.build_coq_and () in let conj_constr = coq_conj () in let mk_and p1 p2 = mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index cbd8a7f0f..5273eb3b5 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -306,7 +306,7 @@ let project_hint pri l2r r = | _ -> assert false in let p = if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in - let p = EConstr.of_constr p in + let p = EConstr.of_constr @@ Universes.constr_of_global 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 (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in @@ -735,7 +735,8 @@ let rewrite_except h = let refl_equal = let coq_base_constant s = - Coqlib.gen_constant_in_modules "RecursiveDefinition" + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "RecursiveDefinition" (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s in function () -> (coq_base_constant "eq_refl") diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index e8c9f4eba..b0db2839b 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -55,22 +55,16 @@ let init_setoid () = if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then () else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"] -let make_dir l = DirPath.make (List.rev_map Id.of_string l) +let lazy_find_reference dir s = + let gr = lazy (Coqlib.coq_reference "generalized rewriting" dir s) in + fun () -> Lazy.force gr -let try_find_global_reference dir s = - let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in - try Nametab.global_of_path sp - with Not_found -> - anomaly (str "Global reference " ++ str s ++ str " not found in generalized rewriting") - -let find_reference dir s = - let gr = lazy (try_find_global_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 = - let gr = lazy (try_find_global_reference dir s) in + let gr = lazy (find_reference dir s) in fun (evd,cstrs) -> let sigma = Sigma.Unsafe.of_evar_map evd in let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force gr) in @@ -81,7 +75,7 @@ let find_global dir s = (** Global constants. *) -let coq_eq_ref = find_reference ["Init"; "Logic"] "eq" +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" @@ -158,11 +152,11 @@ end) = struct let forall_relation = find_global morphisms "forall_relation" let pointwise_relation = find_global morphisms "pointwise_relation" - let forall_relation_ref = find_reference morphisms "forall_relation" - let pointwise_relation_ref = find_reference morphisms "pointwise_relation" + let forall_relation_ref = lazy_find_reference morphisms "forall_relation" + let pointwise_relation_ref = lazy_find_reference morphisms "pointwise_relation" let respectful = find_global morphisms "respectful" - let respectful_ref = find_reference morphisms "respectful" + let respectful_ref = lazy_find_reference morphisms "respectful" let default_relation = find_global ["Classes"; "SetoidTactics"] "DefaultRelation" @@ -174,8 +168,8 @@ end) = struct let rewrite_relation_class = find_global relation_classes "RewriteRelation" - let proper_class = lazy (class_info (try_find_global_reference morphisms "Proper")) - let proper_proxy_class = lazy (class_info (try_find_global_reference morphisms "ProperProxy")) + let proper_class = lazy (class_info (find_reference morphisms "Proper")) + let proper_proxy_class = lazy (class_info (find_reference morphisms "ProperProxy")) let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs)))) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 053bb6fa1..7497aae3c 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -328,7 +328,6 @@ let selecti s m = module M = struct - open Coqlib open Constr open EConstr @@ -356,8 +355,8 @@ struct ["LRing_normalise"]] let coq_modules = - init_modules @ - [logic_dir] @ arith_modules @ zarith_base_modules @ mic_modules + Coqlib.(init_modules @ + [logic_dir] @ arith_modules @ zarith_base_modules @ mic_modules) let bin_module = [["Coq";"Numbers";"BinNums"]] @@ -375,8 +374,8 @@ struct * ZMicromega.v *) - let gen_constant_in_modules s m n = EConstr.of_constr (gen_constant_in_modules s m n) - let init_constant = gen_constant_in_modules "ZMicromega" init_modules + let gen_constant_in_modules s m n = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules s m n) + let init_constant = gen_constant_in_modules "ZMicromega" Coqlib.init_modules 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 @@ -1529,18 +1528,18 @@ let rec apply_ids t ids = | i::ids -> apply_ids (Term.mkApp(t,[| Term.mkVar i |])) ids let coq_Node = - lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node")) + lazy (gen_constant_in_modules "VarMap" + [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node") let coq_Leaf = - lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf")) + lazy (gen_constant_in_modules "VarMap" + [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf") let coq_Empty = - lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty")) + lazy (gen_constant_in_modules "VarMap" + [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty") let coq_VarMap = - lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t")) + lazy (gen_constant_in_modules "VarMap" + [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t") let rec dump_varmap typ m = @@ -2059,8 +2058,8 @@ let micromega_order_changer cert env ff = [ ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |])); ("__varmap", vm, Term.mkApp - (EConstr.of_constr (Coqlib.gen_constant_in_modules "VarMap" - [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t"), [|typ|])); + (gen_constant_in_modules "VarMap" + [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|])); ("__wit", cert, cert_typ) ] (Tacmach.New.pf_concl gl))); diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 8c3471a98..3a0d1dcbc 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -543,7 +543,7 @@ let nsatz lpol = let return_term t = let a = - mkApp(gen_constant "CC" ["Init";"Logic"] "refl_equal",[|tllp ();t|]) in + mkApp(gen_constant "CC" ["Init";"Logic"] "eq_refl",[|tllp ();t|]) in let a = EConstr.of_constr a in generalize [a] diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 334baec8d..27ce0103a 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -196,7 +196,7 @@ 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 (gen_constant_in_modules n m s) +let gen_constant_in_modules n m s = EConstr.of_constr (Universes.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 diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index f38ca85b6..fbed1df17 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -63,13 +63,13 @@ let coq_modules = let bin_module = [["Coq";"Numbers";"BinNums"]] let z_module = [["Coq";"ZArith";"BinInt"]] -let init_constant = Coqlib.gen_constant_in_modules "Omega" Coqlib.init_modules -let constant = Coqlib.gen_constant_in_modules "Omega" coq_modules -let z_constant = Coqlib.gen_constant_in_modules "Omega" z_module -let bin_constant = Coqlib.gen_constant_in_modules "Omega" bin_module +let init_constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" Coqlib.init_modules x +let constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" coq_modules x +let z_constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" z_module x +let bin_constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" bin_module x (* Logic *) -let coq_refl_equal = lazy(init_constant "eq_refl") +let coq_refl_equal = lazy(init_constant "eq_refl") let coq_and = lazy(init_constant "and") let coq_not = lazy(init_constant "not") let coq_or = lazy(init_constant "or") diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index d84e62a93..0cb72cc3a 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -229,7 +229,7 @@ let stdlib_modules = ] let coq_constant c = - lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c)) + lazy (EConstr.of_constr (Universes.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) @@ -274,7 +274,7 @@ let plugin_modules = ] let my_constant c = - lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "Ring" plugin_modules c)) + lazy (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c)) let my_reference c = lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index e7b17991e..c2c8065a9 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -961,7 +961,6 @@ let expand_arg tms (p,ccl) ((_,t),_,na) = let k = length_of_tomatch_type_sign na t in (p+k,liftn_predicate (k-1) (p+1) ccl tms) - let use_unit_judge evd = let j, ctx = coq_unit_judge () in let evd' = Evd.merge_context_set Evd.univ_flexible_alg evd ctx in diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 42aaf3a22..af84b70a3 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -42,6 +42,31 @@ let _ = Goptions.declare_bool_option { Goptions.optwrite = (fun a -> debug_unification:=a); } +(*******************************************) +(* 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 = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in + let (_, u) = Term.destConst c in + Some (c, Term.mkConstU (Coqlib.type_of_id, u), ctx) + +let coq_unit_judge = + let open Environ in + let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in + let na1 = Name (Id.of_string "A") in + let na2 = Name (Id.of_string "H") in + fun () -> + match impossible_default_case () with + | Some (id, type_of_id, ctx) -> + make_judge id type_of_id, ctx + | None -> + (* In case the constants id/ID are not defined *) + Environ.make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1))) + (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2))), + Univ.ContextSet.empty + let unfold_projection env evd ts p c = let cst = Projection.constant p in if is_transparent_constant ts cst then @@ -351,7 +376,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 = match ground_test with | Some result -> result | None -> - (* Until pattern-unification is used consistently, use nohdbeta to not + (* Until pattern-unification is used consistently, use nohdbeta to not destroy beta-redexes that can be used for 1st-order unification *) let term1 = apprec_nohdbeta (fst ts) env evd term1 in let term2 = apprec_nohdbeta (fst ts) env evd term2 in diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 7cee1e8a7..45857df2a 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -80,3 +80,5 @@ val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state * bool -> Evarsolve.unification_result (**/**) +(** {6 Functions to deal with impossible cases } *) +val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set diff --git a/pretyping/program.ml b/pretyping/program.ml index de485dbe8..8769c5659 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -6,26 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open CErrors open Util -open Names -let make_dir l = DirPath.make (List.rev_map Id.of_string l) - -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 -> - user_err (str "Library " ++ Libnames.pr_dirpath dp ++ - str " has to be required first.") - -let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s -let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s) - -let init_constant dir s () = coq_constant "Program" dir s -let init_reference dir s () = coq_reference "Program" dir s +let init_constant dir s () = Universes.constr_of_global @@ Coqlib.coq_reference "Program" dir s +let init_reference dir s () = Coqlib.coq_reference "Program" dir s let papp evdref r args = let open EConstr in diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 768d6860d..fe44559ed 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -20,7 +20,7 @@ module NamedDecl = Context.Named.Declaration (* Absurd *) let mk_absurd_proof t = - let build_coq_not () = EConstr.of_constr (build_coq_not ()) in + let build_coq_not () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_not ()) in let id = Namegen.default_dependent_ident in mkLambda (Names.Name id,mkApp(build_coq_not (),[|t|]), mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|]))) @@ -35,7 +35,7 @@ let absurd c = let t = j.Environ.utj_val in let tac = Tacticals.New.tclTHENLIST [ - elim_type (EConstr.of_constr (build_coq_False ())); + elim_type (EConstr.of_constr (Universes.constr_of_global @@ build_coq_False ())); Simple.apply (mk_absurd_proof t) ] in Sigma.Unsafe.of_pair (tac, sigma) diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 641929a77..bda25d7f0 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -106,8 +106,8 @@ let solveNoteqBranch side = let make_eq () = (*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ())) -let build_coq_not () = EConstr.of_constr (build_coq_not ()) -let build_coq_sumbool () = EConstr.of_constr (build_coq_sumbool ()) +let build_coq_not () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_not ()) +let build_coq_sumbool () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_sumbool ()) let mkDecideEqGoal eqonleft op rectype c1 c2 = let equality = mkApp(make_eq(), [|rectype; c1; c2|]) in diff --git a/tactics/equality.ml b/tactics/equality.ml index f9f9b9dd7..0a68ff129 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -934,9 +934,9 @@ let build_selector env sigma dirn c ind special default = let ci = make_case_info env ind RegularStyle in mkCase (ci, p, c, Array.of_list brl) -let build_coq_False () = EConstr.of_constr (build_coq_False ()) -let build_coq_True () = EConstr.of_constr (build_coq_True ()) -let build_coq_I () = EConstr.of_constr (build_coq_I ()) +let build_coq_False () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_False ()) +let build_coq_True () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_True ()) +let build_coq_I () = EConstr.of_constr (Universes.constr_of_global @@ build_coq_I ()) let rec build_discriminator env sigma dirn c = function | [] -> diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 31d610abd..cf534f13a 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -62,9 +62,10 @@ let constr_of_global g = lazy (Universes.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 _ -> (Coqlib.build_bool_type()).Coqlib.andb_prop +let andb_prop = fun _ -> Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_prop let andb_true_intro = fun _ -> + Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_true_intro let tt = constr_of_global Coqlib.glob_true @@ -73,9 +74,9 @@ let ff = constr_of_global Coqlib.glob_false let eq = constr_of_global Coqlib.glob_eq -let sumbool = Coqlib.build_coq_sumbool +let sumbool () = Universes.constr_of_global (Coqlib.build_coq_sumbool ()) -let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb +let andb = fun _ -> Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb let induct_on c = induction false None c None None @@ -849,7 +850,7 @@ 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 (Coqlib.build_coq_not(),[|eqnm|])|]) + mkApp(sumbool(),[|eqnm;mkApp (Universes.constr_of_global @@ Coqlib.build_coq_not(),[|eqnm|])|]) ) ) ) diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index b21e80bef..885769143 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -472,7 +472,8 @@ let build_combined_scheme env schemes = let ctx, ind, nargs = find_inductive t in (* Number of clauses, including the predicates quantification *) let prods = nb_prod Evd.empty (EConstr.of_constr t) - (nargs + 1) (** FIXME *) in - let coqand = Coqlib.build_coq_and () and coqconj = Coqlib.build_coq_conj () in + let coqand = Universes.constr_of_global @@ Coqlib.build_coq_and () in + let coqconj = Universes.constr_of_global @@ Coqlib.build_coq_conj () in let relargs = rel_vect 0 prods in let concls = List.rev_map (fun (cst, t) -> (* FIXME *) -- cgit v1.2.3