Less "Coq" strings everywhere

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16725 85f007b7-540e-0410-9357-904b9bb8a0f7

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"]