diff options
29 files changed, 160 insertions, 180 deletions
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/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/interp/coqlib.ml b/library/coqlib.ml index 9105bdd54..955ff4c08 100644 --- a/interp/coqlib.ml +++ b/library/coqlib.ml @@ -10,11 +10,9 @@ open CErrors open Util open Pp open Names -open Term open Libnames open Globnames open Nametab -open Smartlocate let coq = Nameops.coq_string (* "Coq" *) @@ -26,10 +24,16 @@ type message = string let make_dir l = DirPath.make (List.rev_map Id.of_string l) let find_reference locstr dir s = - let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in - try global_of_extended_global (Nametab.extended_global_of_path sp) + 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 -> - anomaly ~label:locstr (str "cannot find " ++ Libnames.pr_path sp) + (* 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 @@ -37,14 +41,10 @@ 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 = 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 @@ -61,9 +61,6 @@ let gen_reference_in_modules locstr dirs s = 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 = @@ -91,10 +88,6 @@ 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 @@ -144,12 +137,6 @@ let make_con dir id = Globnames.encode_con dir (Id.of_string id) 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") @@ -189,14 +176,14 @@ type coq_sigma_data = { typ : global_reference } type coq_bool_data = { - andb : constr; - andb_prop : constr; - andb_true_intro : constr} + andb : global_reference; + andb_prop : global_reference; + andb_true_intro : global_reference} 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" } + { 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") @@ -239,7 +226,6 @@ type coq_inversion_data = { } 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 *) @@ -302,7 +288,7 @@ let build_coq_inversion_jmeq_data () = inv_congr = Lazy.force coq_jmeq_congr_canonical } (* Specif *) -let coq_sumbool = lazy_init_constant ["Specif"] "sumbool" +let coq_sumbool = lazy_init_reference ["Specif"] "sumbool" let build_coq_sumbool () = Lazy.force coq_sumbool @@ -344,22 +330,22 @@ let build_coq_inversion_eq_true_data () = inv_congr = Lazy.force coq_eq_true_congr } (* The False proposition *) -let coq_False = lazy_init_constant ["Logic"] "False" +let coq_False = lazy_init_reference ["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" +let coq_True = lazy_init_reference ["Logic"] "True" +let coq_I = lazy_init_reference ["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_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_constant ["Logic"] "proj1" -let coq_iff_right_proj = lazy_init_constant ["Logic"] "proj2" +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 @@ -393,7 +379,5 @@ 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/library/coqlib.mli index 49802089d..716d97c9d 100644 --- a/interp/coqlib.mli +++ b/library/coqlib.mli @@ -9,7 +9,6 @@ open Names open Libnames open Globnames -open Term open Util (** This module collects the global references, constructions and @@ -50,7 +49,6 @@ val coq_reference : message -> string list -> string -> global_reference 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 @@ -72,6 +70,10 @@ 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 @@ -102,9 +104,9 @@ val glob_jmeq : global_reference at runtime. *) type coq_bool_data = { - andb : constr; - andb_prop : constr; - andb_true_intro : constr} + andb : global_reference; + andb_prop : global_reference; + andb_true_intro : global_reference} val build_bool_type : coq_bool_data delayed (** {6 For Equality tactics } *) @@ -161,33 +163,33 @@ 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 +val build_coq_sumbool : global_reference delayed (** {6 ... } *) (** Connectives The False proposition *) -val build_coq_False : constr delayed +val build_coq_False : global_reference delayed (** The True proposition and its unique proof *) -val build_coq_True : constr delayed -val build_coq_I : constr delayed +val build_coq_True : global_reference delayed +val build_coq_I : global_reference delayed (** Negation *) -val build_coq_not : constr delayed +val build_coq_not : global_reference delayed (** Conjunction *) -val build_coq_and : constr delayed -val build_coq_conj : constr delayed -val build_coq_iff : constr delayed +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 : constr delayed -val build_coq_iff_right_proj : constr delayed +val build_coq_iff_left_proj : global_reference delayed +val build_coq_iff_right_proj : global_reference delayed (** Disjunction *) -val build_coq_or : constr delayed +val build_coq_or : global_reference delayed (** Existential quantifier *) -val build_coq_ex : constr delayed +val build_coq_ex : global_reference delayed val coq_eq_ref : global_reference lazy_t val coq_identity_ref : global_reference lazy_t @@ -205,10 +207,5 @@ 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/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 *) |