Names: shortcuts for building {kn, constant, mind} with empty sections

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

7 files changed, 12 insertions, 13 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 073f77403..86ea93294 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -584,7 +584,7 @@ let pp_module mp =
     the constants are directly turned into chars *)
 
 let mk_ind path s =
-  make_mind (MPfile (dirpath_of_string path)) DirPath.empty (Label.make s)
+  MutInd.make2 (MPfile (dirpath_of_string path)) (Label.make s)
 
 let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii"
 
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index e94644821..5aee45dcc 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -219,13 +219,13 @@ let env_for_mtb_with_def env mp seb idl =
 let rec extract_sfb_spec env mp = function
   | [] -> []
   | (l,SFBconst cb) :: msig ->
-      let kn = make_con mp DirPath.empty l in
+      let kn = Constant.make2 mp l in
       let s = extract_constant_spec env kn cb in
       let specs = extract_sfb_spec env mp msig in
       if logical_spec s then specs
       else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
   | (l,SFBmind _) :: msig ->
-      let mind = make_mind mp DirPath.empty l in
+      let mind = MutInd.make2 mp l in
       let s = Sind (mind, extract_inductive env mind) in
       let specs = extract_sfb_spec env mp msig in
       if logical_spec s then specs
@@ -288,7 +288,7 @@ let rec extract_sfb env mp all = function
   | (l,SFBconst cb) :: msb ->
       (try
 	 let vl,recd,msb = factor_fix env l cb msb in
-	 let vc = Array.map (make_con mp DirPath.empty) vl in
+	 let vc = Array.map (Constant.make2 mp) vl in
 	 let ms = extract_sfb env mp all msb in
 	 let b = Array.exists Visit.needed_con vc in
 	 if all || b then
@@ -298,7 +298,7 @@ let rec extract_sfb env mp all = function
 	 else ms
        with Impossible ->
 	 let ms = extract_sfb env mp all msb in
-	 let c = make_con mp DirPath.empty l in
+	 let c = Constant.make2 mp l in
 	 let b = Visit.needed_con c in
 	 if all || b then
 	   let d = extract_constant env c cb in
@@ -307,7 +307,7 @@ let rec extract_sfb env mp all = function
 	 else ms)
   | (l,SFBmind mib) :: msb ->
       let ms = extract_sfb env mp all msb in
-      let mind = make_mind mp DirPath.empty l in
+      let mind = MutInd.make2 mp l in
       let b = Visit.needed_ind mind in
       if all || b then
 	let d = Dind (mind, extract_inductive env mind) in
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 62ce3f31d..c8f376565 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -442,7 +442,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  List.skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
 	assert (List.length field_names = List.length typ);
 	let projs = ref Cset.empty in
-	let mp,d,_ = repr_mind kn in
+	let mp = MutInd.modpath kn in
 	let rec select_fields l typs = match l,typs with
 	  | [],[] -> []
 	  | _::l, typ::typs when isDummy (expand env typ) ->
@@ -450,7 +450,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  | Anonymous::l, typ::typs ->
 	      None :: (select_fields l typs)
 	  | Name id::l, typ::typs ->
-	      let knp = make_con mp d (Label.of_id id) in
+	      let knp = Constant.make2 mp (Label.of_id id) in
 	      (* Is it safe to use [id] for projections [foo.id] ? *)
 	      if List.for_all ((=) Keep) (type2signature env typ)
 	      then projs := Cset.add knp !projs;
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 7d95d2e17..8ecd8cd7c 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1304,9 +1304,8 @@ let inline_test r t =
        not (is_fix t2) && ml_size t < 12 && is_not_strict t)
 
 let con_of_string s =
-  let null = DirPath.empty in
   match DirPath.repr (dirpath_of_string s) with
-    | id :: d -> make_con (MPfile (DirPath.make d)) null (Label.of_id id)
+    | id :: d -> Constant.make2 (MPfile (DirPath.make d)) (Label.of_id id)
     | [] -> assert false
 
 let manual_inline_set =
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 01234aa18..58186e904 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -34,7 +34,7 @@ let se_iter do_decl do_spec do_mp =
 	let mp_w =
 	  List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl'
 	in
-	let r = ConstRef (make_con mp_w DirPath.empty (Label.of_id l')) in
+	let r = ConstRef (Constant.make2 mp_w (Label.of_id l')) in
 	mt_iter mt; do_decl (Dtype(r,l,t))
     | MTwith (mt,ML_With_module(idl,mp))->
         let mp_mt = msid_of_mt mt in
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index dfa5ff6f9..6c3054e2c 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -650,7 +650,7 @@ and pp_module_type params = function
       let mp_w =
 	List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl'
       in
-      let r = ConstRef (make_con mp_w DirPath.empty (Label.of_id l)) in
+      let r = ConstRef (Constant.make2 mp_w (Label.of_id l)) in
       push_visible mp_mt [];
       let pp_w = str " with type " ++ ids ++ pp_global Type r in
       pop_visible();
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 8d3629d35..1cce6cd70 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -18,7 +18,7 @@ open Glob_term
 let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
-let make_mind mp id = Names.make_mind mp DirPath.empty (Label.make id)
+let make_mind mp id = Names.MutInd.make2 mp (Label.make id)
 let make_mind_mpfile dir id = make_mind (MPfile (make_dir dir)) id
 let make_mind_mpdot dir modname id =
   let mp = MPdot (MPfile (make_dir dir), Label.make modname)