diff options
Diffstat (limited to 'plugins')
28 files changed, 425 insertions, 383 deletions
diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v index d82e8ae8ad..4cde08872f 100644 --- a/plugins/btauto/Reflect.v +++ b/plugins/btauto/Reflect.v @@ -396,3 +396,16 @@ lazymatch goal with end | _ => fail "Cannot recognize a boolean equality" end. *) + +Register formula_var as plugins.btauto.f_var. +Register formula_btm as plugins.btauto.f_btm. +Register formula_top as plugins.btauto.f_top. +Register formula_cnj as plugins.btauto.f_cnj. +Register formula_dsj as plugins.btauto.f_dsj. +Register formula_neg as plugins.btauto.f_neg. +Register formula_xor as plugins.btauto.f_xor. +Register formula_ifb as plugins.btauto.f_ifb. + +Register formula_eval as plugins.btauto.eval. +Register boolean_witness as plugins.btauto.witness. +Register reduce_poly_of_formula_sound_alt as plugins.btauto.soundness. diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index b0f97c59b8..ac0a875229 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -12,17 +12,7 @@ open Constr let contrib_name = "btauto" -let init_constant dir s = - let find_constant contrib dir s = - UnivGen.constr_of_global (Coqlib.find_reference contrib dir s) - in - find_constant contrib_name dir s - -let get_constant dir s = lazy (UnivGen.constr_of_global @@ Coqlib.coq_reference contrib_name dir s) - -let get_inductive dir s = - let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in - Lazy.from_fun (fun () -> Globnames.destIndRef (glob_ref ())) +let bt_lib_constr n = lazy (UnivGen.constr_of_global @@ Coqlib.lib_ref n) let decomp_term sigma (c : Constr.t) = Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c))) @@ -31,11 +21,11 @@ let lapp c v = Constr.mkApp (Lazy.force c, v) let (===) = Constr.equal + module CoqList = struct - let path = ["Init"; "Datatypes"] - let typ = get_constant path "list" - let _nil = get_constant path "nil" - let _cons = get_constant path "cons" + let typ = bt_lib_constr "core.list.type" + let _nil = bt_lib_constr "core.list.nil" + let _cons = bt_lib_constr "core.list.cons" let cons ty h t = lapp _cons [|ty; h ; t|] let nil ty = lapp _nil [|ty|] @@ -47,11 +37,10 @@ module CoqList = struct end module CoqPositive = struct - let path = ["Numbers"; "BinNums"] - let typ = get_constant path "positive" - let _xH = get_constant path "xH" - let _xO = get_constant path "xO" - let _xI = get_constant path "xI" + let typ = bt_lib_constr "num.pos.type" + let _xH = bt_lib_constr "num.pos.xH" + let _xO = bt_lib_constr "num.pos.xO" + let _xI = bt_lib_constr "num.pos.xI" (* A coq nat from an int *) let rec of_int n = @@ -91,14 +80,14 @@ end module Bool = struct - let typ = get_constant ["Init"; "Datatypes"] "bool" - let ind = get_inductive ["Init"; "Datatypes"] "bool" - let trueb = get_constant ["Init"; "Datatypes"] "true" - let falseb = get_constant ["Init"; "Datatypes"] "false" - let andb = get_constant ["Init"; "Datatypes"] "andb" - let orb = get_constant ["Init"; "Datatypes"] "orb" - let xorb = get_constant ["Init"; "Datatypes"] "xorb" - let negb = get_constant ["Init"; "Datatypes"] "negb" + let ind = lazy (Globnames.destIndRef (Coqlib.lib_ref "core.bool.type")) + let typ = bt_lib_constr "core.bool.type" + let trueb = bt_lib_constr "core.bool.true" + let falseb = bt_lib_constr "core.bool.false" + let andb = bt_lib_constr "core.bool.andb" + let orb = bt_lib_constr "core.bool.orb" + let xorb = bt_lib_constr "core.bool.xorb" + let negb = bt_lib_constr "core.bool.negb" type t = | Var of int @@ -150,21 +139,20 @@ module Btauto = struct open Pp - let eq = get_constant ["Init"; "Logic"] "eq" - - let f_var = get_constant ["btauto"; "Reflect"] "formula_var" - let f_btm = get_constant ["btauto"; "Reflect"] "formula_btm" - let f_top = get_constant ["btauto"; "Reflect"] "formula_top" - let f_cnj = get_constant ["btauto"; "Reflect"] "formula_cnj" - let f_dsj = get_constant ["btauto"; "Reflect"] "formula_dsj" - let f_neg = get_constant ["btauto"; "Reflect"] "formula_neg" - let f_xor = get_constant ["btauto"; "Reflect"] "formula_xor" - let f_ifb = get_constant ["btauto"; "Reflect"] "formula_ifb" + let eq = bt_lib_constr "core.eq.type" - let eval = get_constant ["btauto"; "Reflect"] "formula_eval" - let witness = get_constant ["btauto"; "Reflect"] "boolean_witness" + let f_var = bt_lib_constr "plugins.btauto.f_var" + let f_btm = bt_lib_constr "plugins.btauto.f_btm" + let f_top = bt_lib_constr "plugins.btauto.f_top" + let f_cnj = bt_lib_constr "plugins.btauto.f_cnj" + let f_dsj = bt_lib_constr "plugins.btauto.f_dsj" + let f_neg = bt_lib_constr "plugins.btauto.f_neg" + let f_xor = bt_lib_constr "plugins.btauto.f_xor" + let f_ifb = bt_lib_constr "plugins.btauto.f_ifb" - let soundness = get_constant ["btauto"; "Reflect"] "reduce_poly_of_formula_sound_alt" + let eval = bt_lib_constr "plugins.btauto.eval" + let witness = bt_lib_constr "plugins.btauto.witness" + let soundness = bt_lib_constr "plugins.btauto.soundness" let rec convert = function | Bool.Var n -> lapp f_var [|CoqPositive.of_int n|] diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 2eaa6146e1..055d36747d 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -28,17 +28,13 @@ open Proofview.Notations module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -let reference dir s = lazy (Coqlib.coq_reference "CC" dir s) - -let _f_equal = reference ["Init";"Logic"] "f_equal" -let _eq_rect = reference ["Init";"Logic"] "eq_rect" -let _refl_equal = reference ["Init";"Logic"] "eq_refl" -let _sym_eq = reference ["Init";"Logic"] "eq_sym" -let _trans_eq = reference ["Init";"Logic"] "eq_trans" -let _eq = reference ["Init";"Logic"] "eq" -let _False = reference ["Init";"Logic"] "False" -let _True = reference ["Init";"Logic"] "True" -let _I = reference ["Init";"Logic"] "I" +let _f_equal = lazy (Coqlib.lib_ref "core.eq.congr") +let _eq_rect = lazy (Coqlib.lib_ref "core.eq.rect") +let _refl_equal = lazy (Coqlib.lib_ref "core.eq.refl") +let _sym_eq = lazy (Coqlib.lib_ref "core.eq.sym") +let _trans_eq = lazy (Coqlib.lib_ref "core.eq.trans") +let _eq = lazy (Coqlib.lib_ref "core.eq.type") +let _False = lazy (Coqlib.lib_ref "core.False.type") let whd env sigma t = Reductionops.clos_whd_flags CClosure.betaiotazeta env sigma t @@ -423,7 +419,7 @@ let build_term_to_complete uf pac = let cc_tactic depth additionnal_terms = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in - Coqlib.check_required_library Coqlib.logic_module_name; + Coqlib.(check_required_library logic_module_name); let _ = debug (fun () -> Pp.str "Reading subgoal ...") in let state = make_prb gl depth additionnal_terms in let _ = debug (fun () -> Pp.str "Problem built, solving ...") in diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 7e54bc8adb..fdeef5f0ac 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -109,11 +109,11 @@ let gen_ground_tac flag taco ids bases = (* special for compatibility with Intuition -let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str +let constant str = Coqlib.get_constr str let defined_connectives=lazy - [[],EvalConstRef (destConst (constant "not")); - [],EvalConstRef (destConst (constant "iff"))] + [[],EvalConstRef (destConst (constant "core.not.type")); + [],EvalConstRef (destConst (constant "core.iff.type"))] let normalize_evaluables= onAllHypsAndConcl diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 3ae777cc9a..8fa676de44 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -234,11 +234,11 @@ let ll_forall_tac prod backtrack id continue seq= (* special for compatibility with old Intuition *) let constant str = UnivGen.constr_of_global - @@ Coqlib.coq_reference "User" ["Init";"Logic"] str + @@ Coqlib.lib_ref str -let defined_connectives=lazy - [AllOccurrences,EvalConstRef (fst (Constr.destConst (constant "not"))); - AllOccurrences,EvalConstRef (fst (Constr.destConst (constant "iff")))] +let defined_connectives = lazy + [AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.not.type"))); + AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.iff.type")))] let normalize_evaluables= Proofview.Goal.enter begin fun gl -> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 5336948642..b12364d04a 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -414,9 +414,9 @@ let rewrite_until_var arg_num eq_ids : tactic = let rec_pte_id = Id.of_string "Hrec" let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = - let coq_False = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_False ()) in - let coq_True = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_True ()) in - let coq_I = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_I ()) in + let coq_False = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type") in + let coq_True = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.type") in + let coq_I = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I") in let rec scan_type context type_of_hyp : tactic = if isLetIn sigma type_of_hyp then let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in @@ -1605,7 +1605,7 @@ let prove_principle_for_gen match !tcc_lemma_ref with | Undefined -> user_err Pp.(str "No tcc proof !!") | Value lemma -> EConstr.of_constr lemma - | Not_needed -> EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_I ()) + | Not_needed -> EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.I") in (* let rec list_diff del_list check_list = *) (* match del_list with *) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 0c45de4dc4..7c80b776a4 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -259,11 +259,8 @@ let mk_result ctxt value avoid = Some functions to deal with overlapping patterns **************************************************) -let coq_True_ref = - lazy (Coqlib.coq_reference "" ["Init";"Logic"] "True") - -let coq_False_ref = - lazy (Coqlib.coq_reference "" ["Init";"Logic"] "False") +let coq_True_ref = lazy (Coqlib.lib_ref "core.True.type") +let coq_False_ref = lazy (Coqlib.lib_ref "core.False.type") (* [make_discr_match_el \[e1,...en\]] builds match e1,...,en with @@ -957,7 +954,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = assert false end | GApp(eq_as_ref,[ty; id ;rt]) - when is_gvar id && is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous + when is_gvar id && is_gr eq_as_ref Coqlib.(lib_ref "core.eq.type") && n == Anonymous -> let loc1 = rt.CAst.loc in let loc2 = eq_as_ref.CAst.loc in @@ -1078,7 +1075,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = else new_b, Id.Set.add id id_to_exclude *) | GApp(eq_as_ref,[ty;rt1;rt2]) - when is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous + when is_gr eq_as_ref Coqlib.(lib_ref "core.eq.type") && n == Anonymous -> begin try @@ -1089,7 +1086,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = List.fold_left (fun acc (lhs,rhs) -> mkGProd(Anonymous, - mkGApp(mkGRef(Lazy.force Coqlib.coq_eq_ref),[mkGHole ();lhs;rhs]),acc) + mkGApp(mkGRef Coqlib.(lib_ref "core.eq.type"),[mkGHole ();lhs;rhs]),acc) ) b l diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index f81de82d5e..5b45a8dbed 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -38,11 +38,11 @@ let glob_decompose_app = (* [glob_make_eq t1 t2] build the glob_constr corresponding to [t2 = t1] *) let glob_make_eq ?(typ= mkGHole ()) t1 t2 = - mkGApp(mkGRef (Lazy.force Coqlib.coq_eq_ref),[typ;t2;t1]) + mkGApp(mkGRef (Coqlib.lib_ref "core.eq.type"),[typ;t2;t1]) (* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *) let glob_make_neq t1 t2 = - mkGApp(mkGRef (Lazy.force Coqlib.coq_not_ref),[glob_make_eq t1 t2]) + mkGApp(mkGRef (Coqlib.lib_ref "core.not.type"),[glob_make_eq t1 t2]) let remove_name_from_mapping mapping na = match na with diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 6ed382ca1c..03a64988e4 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -114,6 +114,7 @@ let def_of_const t = with Not_found -> assert false) |_ -> assert false +[@@@ocaml.warning "-3"] let coq_constant s = UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" @@ -441,7 +442,7 @@ let jmeq () = Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ UnivGen.constr_of_global @@ - Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq" + Coqlib.lib_ref "core.JMeq.type" with e when CErrors.noncritical e -> raise (ToShow e) let jmeq_refl () = @@ -449,7 +450,7 @@ let jmeq_refl () = Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ UnivGen.constr_of_global @@ - Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq_refl" + Coqlib.lib_ref "core.JMeq.refl" with e when CErrors.noncritical e -> raise (ToShow e) let h_intros l = @@ -461,8 +462,10 @@ let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded" let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc") let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv") +[@@@ocaml.warning "-3"] let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_global @@ - Coqlib.coq_reference "" ["Arith";"Wf_nat"] "well_founded_ltof" + Coqlib.find_reference "IndFun" ["Coq"; "Arith";"Wf_nat"] "well_founded_ltof" +[@@@ocaml.warning "+3"] let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof") diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 56fe430077..b8973a18dc 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -81,10 +81,9 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl let make_eq () = try - EConstr.of_constr (UnivGen.constr_of_global (Coqlib.build_coq_eq ())) - with _ -> assert false + EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref "core.eq.type")) + with _ -> assert false - (* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true] (resp. g_to_f = false) where [graph] is the graph of [f] and is the [i]th function in the block. @@ -512,7 +511,7 @@ and intros_with_rewrite_aux : Tacmach.tactic = intros_with_rewrite ] g end - | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_False ())) -> + | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type")) -> Proofview.V82.of_tactic tauto g | Case(_,_,v,_) -> tclTHENLIST[ diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 633d98a585..89dfb58017 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -49,11 +49,12 @@ open Context.Rel.Declaration (* Ugly things which should not be here *) +[@@@ocaml.warning "-3"] let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_global @@ - Coqlib.coq_reference "RecursiveDefinition" m s + Coqlib.find_reference "RecursiveDefinition" m s -let arith_Nat = ["Arith";"PeanoNat";"Nat"] -let arith_Lt = ["Arith";"Lt"] +let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"] +let arith_Lt = ["Coq"; "Arith";"Lt"] let pr_leconstr_rd = let sigma, env = Pfedit.get_current_context () in @@ -63,6 +64,7 @@ let coq_init_constant s = EConstr.of_constr ( UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) +[@@@ocaml.warning "+3"] let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in @@ -143,6 +145,7 @@ let def_id = Id.of_string "def" let p_id = Id.of_string "p" let rec_res_id = Id.of_string "rec_res";; let lt = function () -> (coq_init_constant "lt") +[@@@ocaml.warning "-3"] let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le") let ex = function () -> (coq_init_constant "ex") let nat = function () -> (coq_init_constant "nat") @@ -163,7 +166,6 @@ let coq_S = function () -> (coq_init_constant "S") let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r") let max_ref = function () -> (find_reference ["Recdef"] "max") let max_constr = function () -> EConstr.of_constr (constr_of_global (delayed_force max_ref)) -let coq_conj = function () -> find_reference Coqlib.logic_module_name "conj" let f_S t = mkApp(delayed_force coq_S, [|t|]);; @@ -1241,8 +1243,8 @@ let get_current_subgoals_types () = exception EmptySubgoals let build_and_l sigma l = - let and_constr = UnivGen.constr_of_global @@ Coqlib.build_coq_and () in - let conj_constr = coq_conj () in + let and_constr = UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type" in + let conj_constr = Coqlib.build_coq_conj () in let mk_and p1 p2 = mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in let rec is_well_founded t = diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index ba3fa6fa0d..e5b032e638 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -693,12 +693,7 @@ let rewrite_except h = end -let refl_equal = - let coq_base_constant s = - Coqlib.gen_reference_in_modules "RecursiveDefinition" - (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s in - function () -> (coq_base_constant "eq_refl") - +let refl_equal () = Coqlib.lib_ref "core.eq.type" (* This is simply an implementation of the case_eq tactic. this code should be replaced by a call to the tactic but I don't know how to diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 5b8bd6d01a..9dd98a4ab7 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -56,12 +56,14 @@ let init_setoid () = if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then () else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"] +let find_reference dir s = + Coqlib.find_reference "generalized rewriting" dir s +[@@warning "-3"] + let lazy_find_reference dir s = - let gr = lazy (Coqlib.coq_reference "generalized rewriting" dir s) in + let gr = lazy (find_reference dir s) in fun () -> Lazy.force gr -let find_reference dir s = Coqlib.coq_reference "generalized rewriting" dir s - type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *) let find_global dir s = @@ -74,13 +76,13 @@ let find_global dir s = (** Global constants. *) -let coq_eq_ref = lazy_find_reference ["Init"; "Logic"] "eq" -let coq_eq = find_global ["Init"; "Logic"] "eq" -let coq_f_equal = find_global ["Init"; "Logic"] "f_equal" -let coq_all = find_global ["Init"; "Logic"] "all" -let impl = find_global ["Program"; "Basics"] "impl" +let coq_eq_ref () = Coqlib.lib_ref "core.eq.type" +let coq_eq = find_global ["Coq"; "Init"; "Logic"] "eq" +let coq_f_equal = find_global ["Coq"; "Init"; "Logic"] "f_equal" +let coq_all = find_global ["Coq"; "Init"; "Logic"] "all" +let impl = find_global ["Coq"; "Program"; "Basics"] "impl" -(** Bookkeeping which evars are constraints so that we can +(** Bookkeeping which evars are constraints so that we can remove them at the end of the tactic. *) let goalevars evars = fst evars @@ -154,7 +156,7 @@ end) = struct let respectful = find_global morphisms "respectful" let respectful_ref = lazy_find_reference morphisms "respectful" - let default_relation = find_global ["Classes"; "SetoidTactics"] "DefaultRelation" + let default_relation = find_global ["Coq"; "Classes"; "SetoidTactics"] "DefaultRelation" let coq_forall = find_global morphisms "forall_def" @@ -374,12 +376,12 @@ let type_app_poly env env evd f args = module PropGlobal = struct module Consts = struct - let relation_classes = ["Classes"; "RelationClasses"] - let morphisms = ["Classes"; "Morphisms"] - let relation = ["Relations";"Relation_Definitions"], "relation" + let relation_classes = ["Coq"; "Classes"; "RelationClasses"] + let morphisms = ["Coq"; "Classes"; "Morphisms"] + let relation = ["Coq"; "Relations";"Relation_Definitions"], "relation" let app_poly = app_poly_nocheck - let arrow = find_global ["Program"; "Basics"] "arrow" - let coq_inverse = find_global ["Program"; "Basics"] "flip" + let arrow = find_global ["Coq"; "Program"; "Basics"] "arrow" + let coq_inverse = find_global ["Coq"; "Program"; "Basics"] "flip" end module G = GlobalBindings(Consts) @@ -395,12 +397,12 @@ end module TypeGlobal = struct module Consts = struct - let relation_classes = ["Classes"; "CRelationClasses"] - let morphisms = ["Classes"; "CMorphisms"] + let relation_classes = ["Coq"; "Classes"; "CRelationClasses"] + let morphisms = ["Coq"; "Classes"; "CMorphisms"] let relation = relation_classes, "crelation" let app_poly = app_poly_check - let arrow = find_global ["Classes"; "CRelationClasses"] "arrow" - let coq_inverse = find_global ["Classes"; "CRelationClasses"] "flip" + let arrow = find_global ["Coq"; "Classes"; "CRelationClasses"] "arrow" + let coq_inverse = find_global ["Coq"; "Classes"; "CRelationClasses"] "flip" end module G = GlobalBindings(Consts) @@ -740,9 +742,9 @@ let new_global (evars, cstrs) gr = (sigma, cstrs), c let make_eq sigma = - new_global sigma (Coqlib.build_coq_eq ()) + new_global sigma Coqlib.(lib_ref "core.eq.type") let make_eq_refl sigma = - new_global sigma (Coqlib.build_coq_eq_refl ()) + new_global sigma Coqlib.(lib_ref "core.eq.refl") let get_rew_prf evars r = match r.rew_prf with | RewPrf (rel, prf) -> evars, (rel, prf) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index ec080edbdb..402e8b91e6 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -357,6 +357,8 @@ struct ["Coq";"Reals" ; "Rpow_def"]; ["LRing_normalise"]] +[@@@ocaml.warning "-3"] + let coq_modules = Coqlib.(init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules @ mic_modules) @@ -379,6 +381,8 @@ struct let gen_constant_in_modules s m n = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules s m n) let init_constant = gen_constant_in_modules "ZMicromega" Coqlib.init_modules + [@@@ocaml.warning "+3"] + let constant = gen_constant_in_modules "ZMicromega" coq_modules let bin_constant = gen_constant_in_modules "ZMicromega" bin_module let r_constant = gen_constant_in_modules "ZMicromega" r_modules diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index d2d4639d2b..11d0a4a44d 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -12,7 +12,6 @@ open CErrors open Util open Constr open Tactics -open Coqlib open Num open Utile @@ -136,36 +135,32 @@ let mul = function | (Const n,q) when eq_num n num_1 -> q | (p,q) -> Mul(p,q) -let gen_constant msg path s = UnivGen.constr_of_global @@ - coq_reference msg path s +let gen_constant n = lazy (UnivGen.constr_of_global (Coqlib.lib_ref n)) -let tpexpr = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PExpr") -let ttconst = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEc") -let ttvar = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEX") -let ttadd = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEadd") -let ttsub = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEsub") -let ttmul = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEmul") -let ttopp = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEopp") -let ttpow = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEpow") +let tpexpr = gen_constant "plugins.setoid_ring.pexpr" +let ttconst = gen_constant "plugins.setoid_ring.const" +let ttvar = gen_constant "plugins.setoid_ring.var" +let ttadd = gen_constant "plugins.setoid_ring.add" +let ttsub = gen_constant "plugins.setoid_ring.sub" +let ttmul = gen_constant "plugins.setoid_ring.mul" +let ttopp = gen_constant "plugins.setoid_ring.opp" +let ttpow = gen_constant "plugins.setoid_ring.pow" -let datatypes = ["Init";"Datatypes"] -let binnums = ["Numbers";"BinNums"] +let tlist = gen_constant "core.list.type" +let lnil = gen_constant "core.list.nil" +let lcons = gen_constant "core.list.cons" -let tlist = lazy (gen_constant "CC" datatypes "list") -let lnil = lazy (gen_constant "CC" datatypes "nil") -let lcons = lazy (gen_constant "CC" datatypes "cons") +let tz = gen_constant "num.Z.type" +let z0 = gen_constant "num.Z.Z0" +let zpos = gen_constant "num.Z.Zpos" +let zneg = gen_constant "num.Z.Zneg" -let tz = lazy (gen_constant "CC" binnums "Z") -let z0 = lazy (gen_constant "CC" binnums "Z0") -let zpos = lazy (gen_constant "CC" binnums "Zpos") -let zneg = lazy(gen_constant "CC" binnums "Zneg") +let pxI = gen_constant "num.pos.xI" +let pxO = gen_constant "num.pos.xO" +let pxH = gen_constant "num.pos.xH" -let pxI = lazy(gen_constant "CC" binnums "xI") -let pxO = lazy(gen_constant "CC" binnums "xO") -let pxH = lazy(gen_constant "CC" binnums "xH") - -let nN0 = lazy (gen_constant "CC" binnums "N0") -let nNpos = lazy(gen_constant "CC" binnums "Npos") +let nN0 = gen_constant "num.N.N0" +let nNpos = gen_constant "num.N.Npos" let mkt_app name l = mkApp (Lazy.force name, Array.of_list l) @@ -545,7 +540,7 @@ let nsatz lpol = let return_term t = let a = - mkApp(gen_constant "CC" ["Init";"Logic"] "eq_refl",[|tllp ();t|]) in + mkApp (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.eq.refl",[|tllp ();t|]) in let a = EConstr.of_constr a in generalize [a] diff --git a/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v index dc86a98998..9593e1225c 100644 --- a/plugins/omega/OmegaLemmas.v +++ b/plugins/omega/OmegaLemmas.v @@ -267,3 +267,49 @@ Proof. intros n; exists (Z.of_nat n); split; trivial. rewrite Z.mul_1_r, Z.add_0_r. apply Nat2Z.is_nonneg. Qed. + +Register fast_Zplus_assoc_reverse as plugins.omega.fast_Zplus_assoc_reverse. +Register fast_Zplus_assoc as plugins.omega.fast_Zplus_assoc. +Register fast_Zmult_assoc_reverse as plugins.omega.fast_Zmult_assoc_reverse. +Register fast_Zplus_permute as plugins.omega.fast_Zplus_permute. +Register fast_Zplus_comm as plugins.omega.fast_Zplus_comm. +Register fast_Zmult_comm as plugins.omega.fast_Zmult_comm. + +Register OMEGA1 as plugins.omega.OMEGA1. +Register OMEGA2 as plugins.omega.OMEGA2. +Register OMEGA3 as plugins.omega.OMEGA3. +Register OMEGA4 as plugins.omega.OMEGA4. +Register OMEGA5 as plugins.omega.OMEGA5. +Register OMEGA6 as plugins.omega.OMEGA6. +Register OMEGA7 as plugins.omega.OMEGA7. +Register OMEGA8 as plugins.omega.OMEGA8. +Register OMEGA9 as plugins.omega.OMEGA9. +Register fast_OMEGA10 as plugins.omega.fast_OMEGA10. +Register fast_OMEGA11 as plugins.omega.fast_OMEGA11. +Register fast_OMEGA12 as plugins.omega.fast_OMEGA12. +Register fast_OMEGA13 as plugins.omega.fast_OMEGA13. +Register fast_OMEGA14 as plugins.omega.fast_OMEGA14. +Register fast_OMEGA15 as plugins.omega.fast_OMEGA15. +Register fast_OMEGA16 as plugins.omega.fast_OMEGA16. +Register OMEGA17 as plugins.omega.OMEGA17. +Register OMEGA18 as plugins.omega.OMEGA18. +Register OMEGA19 as plugins.omega.OMEGA19. +Register OMEGA20 as plugins.omega.OMEGA20. + +Register fast_Zred_factor0 as plugins.omega.fast_Zred_factor0. +Register fast_Zred_factor1 as plugins.omega.fast_Zred_factor1. +Register fast_Zred_factor2 as plugins.omega.fast_Zred_factor2. +Register fast_Zred_factor3 as plugins.omega.fast_Zred_factor3. +Register fast_Zred_factor4 as plugins.omega.fast_Zred_factor4. +Register fast_Zred_factor5 as plugins.omega.fast_Zred_factor5. +Register fast_Zred_factor6 as plugins.omega.fast_Zred_factor6. + +Register fast_Zmult_plus_distr_l as plugins.omega.fast_Zmult_plus_distr_l. +Register fast_Zmult_opp_comm as plugins.omega.fast_Zmult_opp_comm. +Register fast_Zopp_plus_distr as plugins.omega.fast_Zopp_plus_distr. +Register fast_Zopp_mult_distr_r as plugins.omega.fast_Zopp_mult_distr_r. +Register fast_Zopp_eq_mult_neg_1 as plugins.omega.fast_Zopp_eq_mult_neg_1. +Register fast_Zopp_involutive as plugins.omega.fast_Zopp_involutive. + +Register new_var as plugins.omega.new_var. +Register intro_Z as plugins.omega.intro_Z. diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index abae6940fa..f55458de8d 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -193,172 +193,159 @@ let reset_all () = To use the constant Zplus, one must type "Lazy.force coq_Zplus" This is the right way to access to Coq constants in tactics ML code *) -open Coqlib - -let logic_dir = ["Coq";"Logic";"Decidable"] -let coq_modules = - init_modules @arith_modules @ [logic_dir] @ zarith_base_modules - @ [["Coq"; "omega"; "OmegaLemmas"]] - -let gen_constant_in_modules n m s = EConstr.of_constr (UnivGen.constr_of_global @@ gen_reference_in_modules n m s) -let init_constant = gen_constant_in_modules "Omega" init_modules -let constant = gen_constant_in_modules "Omega" coq_modules - -let z_constant = gen_constant_in_modules "Omega" [["Coq";"ZArith"]] -let zbase_constant = - gen_constant_in_modules "Omega" [["Coq";"ZArith";"BinInt"]] +let gen_constant k = lazy (k |> Coqlib.lib_ref |> UnivGen.constr_of_global |> EConstr.of_constr) (* Zarith *) -let coq_xH = lazy (constant "xH") -let coq_xO = lazy (constant "xO") -let coq_xI = lazy (constant "xI") -let coq_Z0 = lazy (constant "Z0") -let coq_Zpos = lazy (constant "Zpos") -let coq_Zneg = lazy (constant "Zneg") -let coq_Z = lazy (constant "Z") -let coq_comparison = lazy (constant "comparison") -let coq_Gt = lazy (constant "Gt") -let coq_Zplus = lazy (zbase_constant "Z.add") -let coq_Zmult = lazy (zbase_constant "Z.mul") -let coq_Zopp = lazy (zbase_constant "Z.opp") -let coq_Zminus = lazy (zbase_constant "Z.sub") -let coq_Zsucc = lazy (zbase_constant "Z.succ") -let coq_Zpred = lazy (zbase_constant "Z.pred") -let coq_Z_of_nat = lazy (zbase_constant "Z.of_nat") -let coq_inj_plus = lazy (z_constant "Nat2Z.inj_add") -let coq_inj_mult = lazy (z_constant "Nat2Z.inj_mul") -let coq_inj_minus1 = lazy (z_constant "Nat2Z.inj_sub") -let coq_inj_minus2 = lazy (constant "inj_minus2") -let coq_inj_S = lazy (z_constant "Nat2Z.inj_succ") -let coq_inj_le = lazy (z_constant "Znat.inj_le") -let coq_inj_lt = lazy (z_constant "Znat.inj_lt") -let coq_inj_ge = lazy (z_constant "Znat.inj_ge") -let coq_inj_gt = lazy (z_constant "Znat.inj_gt") -let coq_inj_neq = lazy (z_constant "inj_neq") -let coq_inj_eq = lazy (z_constant "inj_eq") -let coq_fast_Zplus_assoc_reverse = lazy (constant "fast_Zplus_assoc_reverse") -let coq_fast_Zplus_assoc = lazy (constant "fast_Zplus_assoc") -let coq_fast_Zmult_assoc_reverse = lazy (constant "fast_Zmult_assoc_reverse") -let coq_fast_Zplus_permute = lazy (constant "fast_Zplus_permute") -let coq_fast_Zplus_comm = lazy (constant "fast_Zplus_comm") -let coq_fast_Zmult_comm = lazy (constant "fast_Zmult_comm") -let coq_Zmult_le_approx = lazy (constant "Zmult_le_approx") -let coq_OMEGA1 = lazy (constant "OMEGA1") -let coq_OMEGA2 = lazy (constant "OMEGA2") -let coq_OMEGA3 = lazy (constant "OMEGA3") -let coq_OMEGA4 = lazy (constant "OMEGA4") -let coq_OMEGA5 = lazy (constant "OMEGA5") -let coq_OMEGA6 = lazy (constant "OMEGA6") -let coq_OMEGA7 = lazy (constant "OMEGA7") -let coq_OMEGA8 = lazy (constant "OMEGA8") -let coq_OMEGA9 = lazy (constant "OMEGA9") -let coq_fast_OMEGA10 = lazy (constant "fast_OMEGA10") -let coq_fast_OMEGA11 = lazy (constant "fast_OMEGA11") -let coq_fast_OMEGA12 = lazy (constant "fast_OMEGA12") -let coq_fast_OMEGA13 = lazy (constant "fast_OMEGA13") -let coq_fast_OMEGA14 = lazy (constant "fast_OMEGA14") -let coq_fast_OMEGA15 = lazy (constant "fast_OMEGA15") -let coq_fast_OMEGA16 = lazy (constant "fast_OMEGA16") -let coq_OMEGA17 = lazy (constant "OMEGA17") -let coq_OMEGA18 = lazy (constant "OMEGA18") -let coq_OMEGA19 = lazy (constant "OMEGA19") -let coq_OMEGA20 = lazy (constant "OMEGA20") -let coq_fast_Zred_factor0 = lazy (constant "fast_Zred_factor0") -let coq_fast_Zred_factor1 = lazy (constant "fast_Zred_factor1") -let coq_fast_Zred_factor2 = lazy (constant "fast_Zred_factor2") -let coq_fast_Zred_factor3 = lazy (constant "fast_Zred_factor3") -let coq_fast_Zred_factor4 = lazy (constant "fast_Zred_factor4") -let coq_fast_Zred_factor5 = lazy (constant "fast_Zred_factor5") -let coq_fast_Zred_factor6 = lazy (constant "fast_Zred_factor6") -let coq_fast_Zmult_plus_distr_l = lazy (constant "fast_Zmult_plus_distr_l") -let coq_fast_Zmult_opp_comm = lazy (constant "fast_Zmult_opp_comm") -let coq_fast_Zopp_plus_distr = lazy (constant "fast_Zopp_plus_distr") -let coq_fast_Zopp_mult_distr_r = lazy (constant "fast_Zopp_mult_distr_r") -let coq_fast_Zopp_eq_mult_neg_1 = lazy (constant "fast_Zopp_eq_mult_neg_1") -let coq_fast_Zopp_involutive = lazy (constant "fast_Zopp_involutive") -let coq_Zegal_left = lazy (constant "Zegal_left") -let coq_Zne_left = lazy (constant "Zne_left") -let coq_Zlt_left = lazy (constant "Zlt_left") -let coq_Zge_left = lazy (constant "Zge_left") -let coq_Zgt_left = lazy (constant "Zgt_left") -let coq_Zle_left = lazy (constant "Zle_left") -let coq_new_var = lazy (constant "new_var") -let coq_intro_Z = lazy (constant "intro_Z") - -let coq_dec_eq = lazy (zbase_constant "Z.eq_decidable") -let coq_dec_Zne = lazy (constant "dec_Zne") -let coq_dec_Zle = lazy (zbase_constant "Z.le_decidable") -let coq_dec_Zlt = lazy (zbase_constant "Z.lt_decidable") -let coq_dec_Zgt = lazy (constant "dec_Zgt") -let coq_dec_Zge = lazy (constant "dec_Zge") - -let coq_not_Zeq = lazy (constant "not_Zeq") -let coq_not_Zne = lazy (constant "not_Zne") -let coq_Znot_le_gt = lazy (constant "Znot_le_gt") -let coq_Znot_lt_ge = lazy (constant "Znot_lt_ge") -let coq_Znot_ge_lt = lazy (constant "Znot_ge_lt") -let coq_Znot_gt_le = lazy (constant "Znot_gt_le") -let coq_neq = lazy (constant "neq") -let coq_Zne = lazy (constant "Zne") -let coq_Zle = lazy (zbase_constant "Z.le") -let coq_Zgt = lazy (zbase_constant "Z.gt") -let coq_Zge = lazy (zbase_constant "Z.ge") -let coq_Zlt = lazy (zbase_constant "Z.lt") +let coq_xH = gen_constant "num.pos.xH" +let coq_xO = gen_constant "num.pos.xO" +let coq_xI = gen_constant "num.pos.xI" +let coq_Z0 = gen_constant "num.Z.Z0" +let coq_Zpos = gen_constant "num.Z.Zpos" +let coq_Zneg = gen_constant "num.Z.Zneg" +let coq_Z = gen_constant "num.Z.type" +let coq_comparison = gen_constant "core.comparison.type" +let coq_Gt = gen_constant "core.comparison.Gt" +let coq_Zplus = gen_constant "num.Z.add" +let coq_Zmult = gen_constant "num.Z.mul" +let coq_Zopp = gen_constant "num.Z.opp" +let coq_Zminus = gen_constant "num.Z.sub" +let coq_Zsucc = gen_constant "num.Z.succ" +let coq_Zpred = gen_constant "num.Z.pred" +let coq_Z_of_nat = gen_constant "num.Z.of_nat" +let coq_inj_plus = gen_constant "num.Nat2Z.inj_add" +let coq_inj_mult = gen_constant "num.Nat2Z.inj_mul" +let coq_inj_minus1 = gen_constant "num.Nat2Z.inj_sub" +let coq_inj_minus2 = gen_constant "plugins.omega.inj_minus2" +let coq_inj_S = gen_constant "num.Nat2Z.inj_succ" +let coq_inj_eq = gen_constant "plugins.omega.inj_eq" +let coq_inj_neq = gen_constant "plugins.omega.inj_neq" +let coq_inj_le = gen_constant "plugins.omega.inj_le" +let coq_inj_lt = gen_constant "plugins.omega.inj_lt" +let coq_inj_ge = gen_constant "plugins.omega.inj_ge" +let coq_inj_gt = gen_constant "plugins.omega.inj_gt" +let coq_fast_Zplus_assoc_reverse = gen_constant "plugins.omega.fast_Zplus_assoc_reverse" +let coq_fast_Zplus_assoc = gen_constant "plugins.omega.fast_Zplus_assoc" +let coq_fast_Zmult_assoc_reverse = gen_constant "plugins.omega.fast_Zmult_assoc_reverse" +let coq_fast_Zplus_permute = gen_constant "plugins.omega.fast_Zplus_permute" +let coq_fast_Zplus_comm = gen_constant "plugins.omega.fast_Zplus_comm" +let coq_fast_Zmult_comm = gen_constant "plugins.omega.fast_Zmult_comm" +let coq_Zmult_le_approx = gen_constant "plugins.omega.Zmult_le_approx" +let coq_OMEGA1 = gen_constant "plugins.omega.OMEGA1" +let coq_OMEGA2 = gen_constant "plugins.omega.OMEGA2" +let coq_OMEGA3 = gen_constant "plugins.omega.OMEGA3" +let coq_OMEGA4 = gen_constant "plugins.omega.OMEGA4" +let coq_OMEGA5 = gen_constant "plugins.omega.OMEGA5" +let coq_OMEGA6 = gen_constant "plugins.omega.OMEGA6" +let coq_OMEGA7 = gen_constant "plugins.omega.OMEGA7" +let coq_OMEGA8 = gen_constant "plugins.omega.OMEGA8" +let coq_OMEGA9 = gen_constant "plugins.omega.OMEGA9" +let coq_fast_OMEGA10 = gen_constant "plugins.omega.fast_OMEGA10" +let coq_fast_OMEGA11 = gen_constant "plugins.omega.fast_OMEGA11" +let coq_fast_OMEGA12 = gen_constant "plugins.omega.fast_OMEGA12" +let coq_fast_OMEGA13 = gen_constant "plugins.omega.fast_OMEGA13" +let coq_fast_OMEGA14 = gen_constant "plugins.omega.fast_OMEGA14" +let coq_fast_OMEGA15 = gen_constant "plugins.omega.fast_OMEGA15" +let coq_fast_OMEGA16 = gen_constant "plugins.omega.fast_OMEGA16" +let coq_OMEGA17 = gen_constant "plugins.omega.OMEGA17" +let coq_OMEGA18 = gen_constant "plugins.omega.OMEGA18" +let coq_OMEGA19 = gen_constant "plugins.omega.OMEGA19" +let coq_OMEGA20 = gen_constant "plugins.omega.OMEGA20" +let coq_fast_Zred_factor0 = gen_constant "plugins.omega.fast_Zred_factor0" +let coq_fast_Zred_factor1 = gen_constant "plugins.omega.fast_Zred_factor1" +let coq_fast_Zred_factor2 = gen_constant "plugins.omega.fast_Zred_factor2" +let coq_fast_Zred_factor3 = gen_constant "plugins.omega.fast_Zred_factor3" +let coq_fast_Zred_factor4 = gen_constant "plugins.omega.fast_Zred_factor4" +let coq_fast_Zred_factor5 = gen_constant "plugins.omega.fast_Zred_factor5" +let coq_fast_Zred_factor6 = gen_constant "plugins.omega.fast_Zred_factor6" +let coq_fast_Zmult_plus_distr_l = gen_constant "plugins.omega.fast_Zmult_plus_distr_l" +let coq_fast_Zmult_opp_comm = gen_constant "plugins.omega.fast_Zmult_opp_comm" +let coq_fast_Zopp_plus_distr = gen_constant "plugins.omega.fast_Zopp_plus_distr" +let coq_fast_Zopp_mult_distr_r = gen_constant "plugins.omega.fast_Zopp_mult_distr_r" +let coq_fast_Zopp_eq_mult_neg_1 = gen_constant "plugins.omega.fast_Zopp_eq_mult_neg_1" +let coq_fast_Zopp_involutive = gen_constant "plugins.omega.fast_Zopp_involutive" +let coq_Zegal_left = gen_constant "plugins.omega.Zegal_left" +let coq_Zne_left = gen_constant "plugins.omega.Zne_left" +let coq_Zlt_left = gen_constant "plugins.omega.Zlt_left" +let coq_Zge_left = gen_constant "plugins.omega.Zge_left" +let coq_Zgt_left = gen_constant "plugins.omega.Zgt_left" +let coq_Zle_left = gen_constant "plugins.omega.Zle_left" +let coq_new_var = gen_constant "plugins.omega.new_var" +let coq_intro_Z = gen_constant "plugins.omega.intro_Z" + +let coq_dec_eq = gen_constant "num.Z.eq_decidable" +let coq_dec_Zne = gen_constant "plugins.omega.dec_Zne" +let coq_dec_Zle = gen_constant "num.Z.le_decidable" +let coq_dec_Zlt = gen_constant "num.Z.lt_decidable" +let coq_dec_Zgt = gen_constant "plugins.omega.dec_Zgt" +let coq_dec_Zge = gen_constant "plugins.omega.dec_Zge" + +let coq_not_Zeq = gen_constant "plugins.omega.not_Zeq" +let coq_not_Zne = gen_constant "plugins.omega.not_Zne" +let coq_Znot_le_gt = gen_constant "plugins.omega.Znot_le_gt" +let coq_Znot_lt_ge = gen_constant "plugins.omega.Znot_lt_ge" +let coq_Znot_ge_lt = gen_constant "plugins.omega.Znot_ge_lt" +let coq_Znot_gt_le = gen_constant "plugins.omega.Znot_gt_le" +let coq_neq = gen_constant "plugins.omega.neq" +let coq_Zne = gen_constant "plugins.omega.Zne" +let coq_Zle = gen_constant "num.Z.le" +let coq_Zlt = gen_constant "num.Z.lt" +let coq_Zge = gen_constant "num.Z.ge" +let coq_Zgt = gen_constant "num.Z.gt" (* Peano/Datatypes *) -let coq_le = lazy (init_constant "le") -let coq_lt = lazy (init_constant "lt") -let coq_ge = lazy (init_constant "ge") -let coq_gt = lazy (init_constant "gt") -let coq_minus = lazy (init_constant "Nat.sub") -let coq_plus = lazy (init_constant "Nat.add") -let coq_mult = lazy (init_constant "Nat.mul") -let coq_pred = lazy (init_constant "Nat.pred") -let coq_nat = lazy (init_constant "nat") -let coq_S = lazy (init_constant "S") -let coq_O = lazy (init_constant "O") +let coq_nat = gen_constant "num.nat.type" +let coq_O = gen_constant "num.nat.O" +let coq_S = gen_constant "num.nat.S" +let coq_le = gen_constant "num.nat.le" +let coq_lt = gen_constant "num.nat.lt" +let coq_ge = gen_constant "num.nat.ge" +let coq_gt = gen_constant "num.nat.gt" +let coq_plus = gen_constant "num.nat.add" +let coq_minus = gen_constant "num.nat.sub" +let coq_mult = gen_constant "num.nat.mul" +let coq_pred = gen_constant "num.nat.pred" (* Compare_dec/Peano_dec/Minus *) -let coq_pred_of_minus = lazy (constant "pred_of_minus") -let coq_le_gt_dec = lazy (constant "le_gt_dec") -let coq_dec_eq_nat = lazy (constant "dec_eq_nat") -let coq_dec_le = lazy (constant "dec_le") -let coq_dec_lt = lazy (constant "dec_lt") -let coq_dec_ge = lazy (constant "dec_ge") -let coq_dec_gt = lazy (constant "dec_gt") -let coq_not_eq = lazy (constant "not_eq") -let coq_not_le = lazy (constant "not_le") -let coq_not_lt = lazy (constant "not_lt") -let coq_not_ge = lazy (constant "not_ge") -let coq_not_gt = lazy (constant "not_gt") +let coq_pred_of_minus = gen_constant "num.nat.pred_of_minus" +let coq_le_gt_dec = gen_constant "num.nat.le_gt_dec" +let coq_dec_eq_nat = gen_constant "num.nat.eq_dec" +let coq_dec_le = gen_constant "num.nat.dec_le" +let coq_dec_lt = gen_constant "num.nat.dec_lt" +let coq_dec_ge = gen_constant "num.nat.dec_ge" +let coq_dec_gt = gen_constant "num.nat.dec_gt" +let coq_not_eq = gen_constant "num.nat.not_eq" +let coq_not_le = gen_constant "num.nat.not_le" +let coq_not_lt = gen_constant "num.nat.not_lt" +let coq_not_ge = gen_constant "num.nat.not_ge" +let coq_not_gt = gen_constant "num.nat.not_gt" (* Logic/Decidable *) -let coq_eq_ind_r = lazy (constant "eq_ind_r") - -let coq_dec_or = lazy (constant "dec_or") -let coq_dec_and = lazy (constant "dec_and") -let coq_dec_imp = lazy (constant "dec_imp") -let coq_dec_iff = lazy (constant "dec_iff") -let coq_dec_not = lazy (constant "dec_not") -let coq_dec_False = lazy (constant "dec_False") -let coq_dec_not_not = lazy (constant "dec_not_not") -let coq_dec_True = lazy (constant "dec_True") - -let coq_not_or = lazy (constant "not_or") -let coq_not_and = lazy (constant "not_and") -let coq_not_imp = lazy (constant "not_imp") -let coq_not_iff = lazy (constant "not_iff") -let coq_not_not = lazy (constant "not_not") -let coq_imp_simp = lazy (constant "imp_simp") -let coq_iff = lazy (constant "iff") -let coq_not = lazy (init_constant "not") -let coq_and = lazy (init_constant "and") -let coq_or = lazy (init_constant "or") -let coq_eq = lazy (init_constant "eq") -let coq_ex = lazy (init_constant "ex") -let coq_False = lazy (init_constant "False") -let coq_True = lazy (init_constant "True") +let coq_eq_ind_r = gen_constant "core.eq.ind_r" + +let coq_dec_or = gen_constant "core.dec.or" +let coq_dec_and = gen_constant "core.dec.and" +let coq_dec_imp = gen_constant "core.dec.imp" +let coq_dec_iff = gen_constant "core.dec.iff" +let coq_dec_not = gen_constant "core.dec.not" +let coq_dec_False = gen_constant "core.dec.False" +let coq_dec_not_not = gen_constant "core.dec.not_not" +let coq_dec_True = gen_constant "core.dec.True" + +let coq_not_or = gen_constant "core.dec.not_or" +let coq_not_and = gen_constant "core.dec.not_and" +let coq_not_imp = gen_constant "core.dec.not_imp" +let coq_not_iff = gen_constant "core.dec.not_iff" +let coq_not_not = gen_constant "core.dec.dec_not_not" +let coq_imp_simp = gen_constant "core.dec.imp_simp" +let coq_iff = gen_constant "core.iff.type" +let coq_not = gen_constant "core.not.type" +let coq_and = gen_constant "core.and.type" +let coq_or = gen_constant "core.or.type" +let coq_eq = gen_constant "core.eq.type" +let coq_ex = gen_constant "core.ex.type" +let coq_False = gen_constant "core.False.type" +let coq_True = gen_constant "core.True.type" (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *) diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v index 600e8993b4..99c02995fb 100644 --- a/plugins/rtauto/Bintree.v +++ b/plugins/rtauto/Bintree.v @@ -319,6 +319,9 @@ Arguments F_empty [A]. Arguments F_push [A] a S _. Arguments In [A] x S F. +Register empty as plugins.rtauto.empty. +Register push as plugins.rtauto.push. + Section Map. Variables A B:Set. diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v index 06cdf76b4e..f027a4a46e 100644 --- a/plugins/rtauto/Rtauto.v +++ b/plugins/rtauto/Rtauto.v @@ -387,3 +387,24 @@ exact (Reflect (empty \ A \ B \ C) Qed. Print toto. *) + +Register Reflect as plugins.rtauto.Reflect. + +Register Atom as plugins.rtauto.Atom. +Register Arrow as plugins.rtauto.Arrow. +Register Bot as plugins.rtauto.Bot. +Register Conjunct as plugins.rtauto.Conjunct. +Register Disjunct as plugins.rtauto.Disjunct. + +Register Ax as plugins.rtauto.Ax. +Register I_Arrow as plugins.rtauto.I_Arrow. +Register E_Arrow as plugins.rtauto.E_Arrow. +Register D_Arrow as plugins.rtauto.D_Arrow. +Register E_False as plugins.rtauto.E_False. +Register I_And as plugins.rtauto.I_And. +Register E_And as plugins.rtauto.E_And. +Register D_And as plugins.rtauto.D_And. +Register I_Or_l as plugins.rtauto.I_Or_l. +Register I_Or_r as plugins.rtauto.I_Or_r. +Register E_Or as plugins.rtauto.E_Or. +Register D_Or as plugins.rtauto.D_Or. diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 8a0f48dc4d..79418da27c 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -26,49 +26,39 @@ let step_count = ref 0 let node_count = ref 0 -let logic_constant s = UnivGen.constr_of_global @@ - Coqlib.coq_reference "refl_tauto" ["Init";"Logic"] s - -let li_False = lazy (destInd (logic_constant "False")) -let li_and = lazy (destInd (logic_constant "and")) -let li_or = lazy (destInd (logic_constant "or")) - -let pos_constant s = UnivGen.constr_of_global @@ - Coqlib.coq_reference "refl_tauto" ["Numbers";"BinNums"] s - -let l_xI = lazy (pos_constant "xI") -let l_xO = lazy (pos_constant "xO") -let l_xH = lazy (pos_constant "xH") - -let store_constant s = UnivGen.constr_of_global @@ - Coqlib.coq_reference "refl_tauto" ["rtauto";"Bintree"] s - -let l_empty = lazy (store_constant "empty") -let l_push = lazy (store_constant "push") - -let constant s = UnivGen.constr_of_global @@ - Coqlib.coq_reference "refl_tauto" ["rtauto";"Rtauto"] s - -let l_Reflect = lazy (constant "Reflect") - -let l_Atom = lazy (constant "Atom") -let l_Arrow = lazy (constant "Arrow") -let l_Bot = lazy (constant "Bot") -let l_Conjunct = lazy (constant "Conjunct") -let l_Disjunct = lazy (constant "Disjunct") - -let l_Ax = lazy (constant "Ax") -let l_I_Arrow = lazy (constant "I_Arrow") -let l_E_Arrow = lazy (constant "E_Arrow") -let l_D_Arrow = lazy (constant "D_Arrow") -let l_E_False = lazy (constant "E_False") -let l_I_And = lazy (constant "I_And") -let l_E_And = lazy (constant "E_And") -let l_D_And = lazy (constant "D_And") -let l_I_Or_l = lazy (constant "I_Or_l") -let l_I_Or_r = lazy (constant "I_Or_r") -let l_E_Or = lazy (constant "E_Or") -let l_D_Or = lazy (constant "D_Or") +let li_False = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type")) +let li_and = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type")) +let li_or = lazy (destInd (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.or.type")) + +let gen_constant n = lazy (UnivGen.constr_of_global (Coqlib.lib_ref n)) + +let l_xI = gen_constant "num.pos.xI" +let l_xO = gen_constant "num.pos.xO" +let l_xH = gen_constant "num.pos.xH" + +let l_empty = gen_constant "plugins.rtauto.empty" +let l_push = gen_constant "plugins.rtauto.push" + +let l_Reflect = gen_constant "plugins.rtauto.Reflect" + +let l_Atom = gen_constant "plugins.rtauto.Atom" +let l_Arrow = gen_constant "plugins.rtauto.Arrow" +let l_Bot = gen_constant "plugins.rtauto.Bot" +let l_Conjunct = gen_constant "plugins.rtauto.Conjunct" +let l_Disjunct = gen_constant "plugins.rtauto.Disjunct" + +let l_Ax = gen_constant "plugins.rtauto.Ax" +let l_I_Arrow = gen_constant "plugins.rtauto.I_Arrow" +let l_E_Arrow = gen_constant "plugins.rtauto.E_Arrow" +let l_D_Arrow = gen_constant "plugins.rtauto.D_Arrow" +let l_E_False = gen_constant "plugins.rtauto.E_False" +let l_I_And = gen_constant "plugins.rtauto.I_And" +let l_E_And = gen_constant "plugins.rtauto.E_And" +let l_D_And = gen_constant "plugins.rtauto.D_And" +let l_I_Or_l = gen_constant "plugins.rtauto.I_Or_l" +let l_I_Or_r = gen_constant "plugins.rtauto.I_Or_r" +let l_E_Or = gen_constant "plugins.rtauto.E_Or" +let l_D_Or = gen_constant "plugins.rtauto.D_Or" let special_whd gl c = diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index 33df36d847..ccd82eabcd 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -919,6 +919,14 @@ Section MakeRingPol. | PEopp : PExpr -> PExpr | PEpow : PExpr -> N -> PExpr. + Register PExpr as plugins.setoid_ring.pexpr. + Register PEc as plugins.setoid_ring.const. + Register PEX as plugins.setoid_ring.var. + Register PEadd as plugins.setoid_ring.add. + Register PEsub as plugins.setoid_ring.sub. + Register PEmul as plugins.setoid_ring.mul. + Register PEopp as plugins.setoid_ring.opp. + Register PEpow as plugins.setoid_ring.pow. (** evaluation of polynomial expressions towards R *) Definition mk_X j := mkPinj_pred j mkX. diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 0734654abf..85e759d152 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -205,25 +205,16 @@ let exec_tactic env evd n f args = let nf c = constr_of evd c in Array.map nf !tactic_res, Evd.universe_context_set evd -let stdlib_modules = - [["Coq";"Setoids";"Setoid"]; - ["Coq";"Lists";"List"]; - ["Coq";"Init";"Datatypes"]; - ["Coq";"Init";"Logic"]; - ] - -let coq_constant c = - lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" stdlib_modules c)) -let coq_reference c = - lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c) - -let coq_mk_Setoid = coq_constant "Build_Setoid_Theory" -let coq_None = coq_reference "None" -let coq_Some = coq_reference "Some" -let coq_eq = coq_constant "eq" - -let coq_cons = coq_reference "cons" -let coq_nil = coq_reference "nil" +let gen_constant n = lazy (EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref n))) +let gen_reference n = lazy (Coqlib.lib_ref n) + +let coq_mk_Setoid = gen_constant "plugins.setoid_ring.Build_Setoid_Theory" +let coq_None = gen_reference "core.option.None" +let coq_Some = gen_reference "core.option.Some" +let coq_eq = gen_constant "core.eq.type" + +let coq_cons = gen_reference "core.list.cons" +let coq_nil = gen_reference "core.list.nil" let lapp f args = mkApp(Lazy.force f,args) @@ -260,16 +251,18 @@ let plugin_modules = let my_constant c = lazy (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c)) + [@@ocaml.warning "-3"] let my_reference c = lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c) + [@@ocaml.warning "-3"] let znew_ring_path = DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"]) let zltac s = lazy(KerName.make (ModPath.MPfile znew_ring_path) (Label.make s)) -let mk_cst l s = lazy (Coqlib.coq_reference "newring" l s);; -let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;; +let mk_cst l s = lazy (Coqlib.coq_reference "newring" l s) [@@ocaml.warning "-3"] +let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s (* Ring theory *) @@ -907,7 +900,7 @@ let ftheory_to_obj : field_info -> obj = let field_equality evd r inv req = match EConstr.kind !evd req with | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) -> - let c = UnivGen.constr_of_global (Coqlib.build_coq_eq_data()).congr in + let c = UnivGen.constr_of_global Coqlib.(lib_ref "core.eq.congr") in let c = EConstr.of_constr c in mkApp(c,[|r;r;inv|]) | _ -> diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index f2f236f448..1492cfb4e4 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -201,8 +201,8 @@ let mkRInd mind = DAst.make @@ GRef (IndRef mind,None) let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t) let rec mkRnat n = - if n <= 0 then DAst.make @@ GRef (Coqlib.glob_O, None) else - mkRApp (DAst.make @@ GRef (Coqlib.glob_S, None)) [mkRnat (n - 1)] + if n <= 0 then DAst.make @@ GRef (Coqlib.lib_ref "num.nat.O", None) else + mkRApp (DAst.make @@ GRef (Coqlib.lib_ref "num.nat.S", None)) [mkRnat (n - 1)] let glob_constr ist genv = function | _, Some ce -> @@ -763,7 +763,7 @@ let mkEtaApp c n imin = let mkRefl t c gl = let sigma = project gl in - let (sigma, refl) = EConstr.fresh_global (pf_env gl) sigma Coqlib.((build_coq_eq_data()).refl) in + let (sigma, refl) = EConstr.fresh_global (pf_env gl) sigma Coqlib.(lib_ref "core.eq.refl") in EConstr.mkApp (refl, [|t; c|]), { gl with sigma } let discharge_hyp (id', (id, mode)) gl = @@ -1220,7 +1220,7 @@ let genclrtac cl cs clr = (fun type_err gl -> tclTHEN (tclTHEN (Proofview.V82.of_tactic (Tactics.elim_type (EConstr.of_constr - (UnivGen.constr_of_global @@ Coqlib.build_coq_False ())))) (old_cleartac clr)) + (UnivGen.constr_of_global @@ Coqlib.(lib_ref "core.False.type"))))) (old_cleartac clr)) (fun gl -> raise type_err) gl)) (old_cleartac clr) @@ -1504,7 +1504,7 @@ let tclOPTION o d = let tacIS_INJECTION_CASE ?ty t = begin tclOPTION ty (tacTYPEOF t) >>= fun ty -> tacREDUCE_TO_QUANTIFIED_IND ty >>= fun ((mind,_),_) -> - tclUNIT (GlobRef.equal (GlobRef.IndRef mind) (Coqlib.build_coq_eq ())) + tclUNIT (Coqlib.check_ind_ref "core.eq.type" mind) end let tclWITHTOP tac = Goal.enter begin fun gl -> diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 602fcfcab5..7f9a9e125e 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -115,7 +115,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let orig_gl, concl, env = gl, pf_concl gl, pf_env gl in ppdebug(lazy(Pp.str(if is_case then "==CASE==" else "==ELIM=="))); let fire_subst gl t = Reductionops.nf_evar (project gl) t in - let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in + let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in let eq = EConstr.of_constr eq in let is_undef_pat = function | sigma, T t -> EConstr.isEvar sigma (EConstr.of_constr t) @@ -421,7 +421,7 @@ let injectl2rtac sigma c = match EConstr.kind sigma c with let is_injection_case c gl = let gl, cty = pfe_type_of gl c in let (mind,_), _ = pf_reduce_to_quantified_ind gl cty in - GlobRef.equal (IndRef mind) (Coqlib.build_coq_eq ()) + GlobRef.equal (IndRef mind) Coqlib.(lib_ref "core.eq.type") let perform_injection c gl = let gl, cty = pfe_type_of gl c in diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 2af917b939..c04ced4ab4 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -130,7 +130,7 @@ let newssrcongrtac arg ist gl = let ssr_congr lr = EConstr.mkApp (arr, lr) in (* here thw two cases: simple equality or arrow *) let equality, _, eq_args, gl' = - let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in + let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in pf_saturate gl (EConstr.of_constr eq) 3 in tclMATCH_GOAL (equality, gl') (fun gl' -> fs gl' (List.assoc 0 eq_args)) (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) ty) ist) @@ -386,7 +386,7 @@ let rwcltac cl rdx dir sr gl = ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env (pf_env gl) (project gl) (snd sr))); let cvtac, rwtac, gl = if EConstr.Vars.closed0 (project gl) r' then - let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, Coqlib.build_coq_eq () in + let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, Coqlib.(lib_ref "core.eq.type") in let sigma, c_ty = Typing.type_of env sigma c in ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty)); match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with @@ -427,6 +427,7 @@ let rwcltac cl rdx dir sr gl = ;; +[@@@ocaml.warning "-3"] let lz_coq_prod = let prod = lazy (Coqlib.build_prod ()) in fun () -> Lazy.force prod @@ -438,7 +439,7 @@ let lz_setoid_relation = | _ -> let srel = try Some (UnivGen.constr_of_global @@ - Coqlib.coq_reference "Class_setoid" sdir "RewriteRelation") + Coqlib.find_reference "Class_setoid" ("Coq"::sdir) "RewriteRelation" [@ocaml.warning "-3"]) with _ -> None in last_srel := (env, srel); srel @@ -484,7 +485,7 @@ let rwprocess_rule dir rule gl = | _ -> let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in EConstr.mkApp (pi2, ra), sigma in - if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.build_coq_True ())) then + if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.(lib_ref "core.True.type"))) then let s, sigma = sr sigma 2 in loop (converse_dir d) sigma s a.(1) rs 0 else diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 1dbacf0ff7..ce439d0497 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -149,6 +149,7 @@ let tac_case t = end (** [=> [: id]] ************************************************************) +[@@@ocaml.warning "-3"] let mk_abstract_id = let open Coqlib in let ssr_abstract_id = Summary.ref ~name:"SSR:abstractid" 0 in @@ -375,7 +376,7 @@ let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr = let rec gen_eq_tac () = Goal.enter begin fun g -> let sigma, env, concl = Goal.(sigma g, env g, concl g) in let sigma, eq = - EConstr.fresh_global env sigma (Coqlib.build_coq_eq ()) in + EConstr.fresh_global env sigma (Coqlib.lib_ref "core.eq.type") in let ctx, last = EConstr.decompose_prod_assum sigma concl in let args = match EConstr.kind_of_type sigma last with | Term.AtomicType (hd, args) -> diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 8ee6fbf036..94255bab6c 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -40,8 +40,7 @@ let ascii_kn = MutInd.make2 ascii_modpath ascii_label let path_of_Ascii = ((ascii_kn,0),1) let static_glob_Ascii = ConstructRef path_of_Ascii -let make_reference id = find_reference "Ascii interpretation" ascii_module id -let glob_Ascii = lazy (make_reference "Ascii") +let glob_Ascii = lazy (lib_ref "plugins.syntax.Ascii") open Lazy @@ -49,7 +48,7 @@ let interp_ascii ?loc p = let rec aux n p = if Int.equal n 0 then [] else let mp = p mod 2 in - (DAst.make ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None)) + (DAst.make ?loc @@ GRef (lib_ref (if Int.equal mp 0 then "core.bool.false" else "core.bool.true"),None)) :: (aux (n-1) (p/2)) in DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p) @@ -67,8 +66,8 @@ let interp_ascii_string ?loc s = let uninterp_ascii r = let rec uninterp_bool_list n = function | [] when Int.equal n 0 -> 0 - | r::l when is_gr r glob_true -> 1+2*(uninterp_bool_list (n-1) l) - | r::l when is_gr r glob_false -> 2*(uninterp_bool_list (n-1) l) + | r::l when is_gr r (lib_ref "core.bool.true") -> 1+2*(uninterp_bool_list (n-1) l) + | r::l when is_gr r (lib_ref "core.bool.false") -> 2*(uninterp_bool_list (n-1) l) | _ -> raise Non_closed_ascii in try let aux c = match DAst.get c with diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index 703b40dd3e..59e65a0672 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -31,9 +31,8 @@ let string_kn = MutInd.make2 string_modpath @@ Label.make "string" let static_glob_EmptyString = ConstructRef ((string_kn,0),1) let static_glob_String = ConstructRef ((string_kn,0),2) -let make_reference id = find_reference "String interpretation" string_module id -let glob_String = lazy (make_reference "String") -let glob_EmptyString = lazy (make_reference "EmptyString") +let glob_String = lazy (lib_ref "plugins.syntax.String") +let glob_EmptyString = lazy (lib_ref "plugins.syntax.EmptyString") let is_gr c gr = match DAst.get c with | GRef (r, _) -> GlobRef.equal r gr |