From c1159f736c8d8f5b95bc53af7614a63f2ab9a86b Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 22 Aug 2013 14:29:55 +0000 Subject: Less "Coq" strings everywhere git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16725 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/coqlib.ml | 32 +++++++++++++++++--------------- interp/coqlib.mli | 5 ++++- library/nameops.ml | 3 ++- library/nameops.mli | 3 ++- plugins/cc/cctac.ml | 2 +- plugins/funind/indfun_common.ml | 4 ++-- plugins/funind/recdef.ml | 2 +- plugins/syntax/nat_syntax.ml | 2 +- tactics/tactics.ml | 2 +- toplevel/obligations.ml | 2 +- 10 files changed, 32 insertions(+), 25 deletions(-) diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 9ce330078..2256764a3 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -16,6 +16,8 @@ open Globnames open Nametab open Smartlocate +let coq = Nameops.coq_string (* "Coq" *) + (************************************************************************) (* Generic functions to find Coq objects *) @@ -29,7 +31,7 @@ let find_reference locstr dir s = with Not_found -> anomaly ~label:locstr (str "cannot find " ++ Libnames.pr_path sp) -let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s +let coq_reference locstr dir s = find_reference locstr (coq::dir) s let coq_constant locstr dir s = constr_of_global (coq_reference locstr dir s) let gen_reference = coq_reference @@ -85,27 +87,27 @@ let check_required_library d = let init_reference dir s = let d = "Init"::dir in - check_required_library ("Coq"::d); gen_reference "Coqlib" d s + check_required_library (coq::d); gen_reference "Coqlib" d s let init_constant dir s = let d = "Init"::dir in - check_required_library ("Coq"::d); gen_constant "Coqlib" d s + check_required_library (coq::d); gen_constant "Coqlib" d s let logic_constant dir s = let d = "Logic"::dir in - check_required_library ("Coq"::d); gen_constant "Coqlib" d s + check_required_library (coq::d); gen_constant "Coqlib" d s -let arith_dir = ["Coq";"Arith"] +let arith_dir = [coq;"Arith"] let arith_modules = [arith_dir] -let numbers_dir = [ "Coq";"Numbers"] -let parith_dir = ["Coq";"PArith"] -let narith_dir = ["Coq";"NArith"] -let zarith_dir = ["Coq";"ZArith"] +let numbers_dir = [coq;"Numbers"] +let parith_dir = [coq;"PArith"] +let narith_dir = [coq;"NArith"] +let zarith_dir = [coq;"ZArith"] let zarith_base_modules = [numbers_dir;parith_dir;narith_dir;zarith_dir] -let init_dir = ["Coq";"Init"] +let init_dir = [coq;"Init"] let init_modules = [ init_dir@["Datatypes"]; init_dir@["Logic"]; @@ -115,19 +117,19 @@ let init_modules = [ init_dir@["Wf"] ] -let logic_module_name = ["Coq";"Init";"Logic"] +let logic_module_name = init_dir@["Logic"] let logic_module = make_dir logic_module_name -let logic_type_module_name = ["Coq";"Init";"Logic_Type"] +let logic_type_module_name = init_dir@["Logic_Type"] let logic_type_module = make_dir logic_type_module_name -let datatypes_module_name = ["Coq";"Init";"Datatypes"] +let datatypes_module_name = init_dir@["Datatypes"] let datatypes_module = make_dir datatypes_module_name -let arith_module_name = ["Coq";"Arith";"Arith"] +let arith_module_name = arith_dir@["Arith"] let arith_module = make_dir arith_module_name -let jmeq_module_name = ["Coq";"Logic";"JMeq"] +let jmeq_module_name = [coq;"Logic";"JMeq"] let jmeq_module = make_dir jmeq_module_name (* TODO: temporary hack. Works only if the module isn't an alias *) diff --git a/interp/coqlib.mli b/interp/coqlib.mli index d9c0d3ae0..b8e461665 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -55,11 +55,14 @@ val check_required_library : string list -> unit (** Modules *) val logic_module : DirPath.t +val logic_module_name : string list + val logic_type_module : DirPath.t + val jmeq_module : DirPath.t +val jmeq_module_name : string list val datatypes_module_name : string list -val logic_module_name : string list (** Natural numbers *) val nat_path : full_path diff --git a/library/nameops.ml b/library/nameops.ml index 3b8de17d2..22a21a4d5 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -141,7 +141,8 @@ let pr_lab l = str (Label.to_string l) let default_library = Names.DirPath.initial (* = ["Top"] *) (*s Roots of the space of absolute names *) -let coq_root = Id.of_string "Coq" +let coq_string = "Coq" +let coq_root = Id.of_string coq_string let default_root_prefix = DirPath.empty (* Metavariables *) diff --git a/library/nameops.mli b/library/nameops.mli index 53cc86786..a30aae2e2 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -43,7 +43,8 @@ val pr_lab : Label.t -> Pp.std_ppcmds val default_library : DirPath.t (** This is the root of the standard library of Coq *) -val coq_root : module_ident +val coq_root : module_ident (** "Coq" *) +val coq_string : string (** "Coq" *) (** This is the default root prefix for developments which doesn't mention a root *) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index a7800667f..780a4877a 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -371,7 +371,7 @@ let build_term_to_complete uf meta pac = applistc (mkConstruct cinfo.ci_constr) all_args let cc_tactic depth additionnal_terms gls= - Coqlib.check_required_library ["Coq";"Init";"Logic"]; + Coqlib.check_required_library Coqlib.logic_module_name; let _ = debug (Pp.str "Reading subgoal ...") in let state = make_prb gls depth additionnal_terms in let _ = debug (Pp.str "Problem built, solving ...") in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 827747c6b..f504b0734 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -473,13 +473,13 @@ exception ToShow of exn let jmeq () = try - Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; + Coqlib.check_required_library Coqlib.jmeq_module_name; Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq" with e when Errors.noncritical e -> raise (ToShow e) let jmeq_refl () = try - Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; + Coqlib.check_required_library Coqlib.jmeq_module_name; Coqlib.gen_constant "Function" ["Logic";"JMeq"] "JMeq_refl" with e when Errors.noncritical e -> raise (ToShow e) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index d2d5a957f..857e82fc5 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -150,7 +150,7 @@ let coq_S = function () -> (coq_base_constant "S") let lt_n_O = function () -> (coq_base_constant "lt_n_O") let max_ref = function () -> (find_reference ["Recdef"] "max") let max_constr = function () -> (constr_of_global (delayed_force max_ref)) -let coq_conj = function () -> find_reference ["Coq";"Init";"Logic"] "conj" +let coq_conj = function () -> find_reference Coqlib.logic_module_name "conj" let f_S t = mkApp(delayed_force coq_S, [|t|]);; diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 24ce7d652..59180be81 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -65,6 +65,6 @@ let uninterp_nat p = let _ = Notation.declare_numeral_interpreter "nat_scope" - (nat_path,["Coq";"Init";"Datatypes"]) + (nat_path,datatypes_module_name) nat_of_int ([GRef (Loc.ghost,glob_S); GRef (Loc.ghost,glob_O)], uninterp_nat, true) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ee92762cb..b0f150158 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2553,7 +2553,7 @@ let abstract_args gl generalize_vars dep id defined f args = else None let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id gl = - Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; + Coqlib.check_required_library Coqlib.jmeq_module_name; let f, args, def, id, oldid = let oldid = pf_get_new_id id gl in let (_, b, t) = pf_get_hyp gl id in diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 58201a5f8..ed315bcf5 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -1008,7 +1008,7 @@ let next_obligation n tac = solve_obligation prg i tac let init_program () = - Coqlib.check_required_library ["Coq";"Init";"Datatypes"]; + Coqlib.check_required_library Coqlib.datatypes_module_name; Coqlib.check_required_library ["Coq";"Init";"Specif"]; Coqlib.check_required_library ["Coq";"Program";"Tactics"] -- cgit v1.2.3