Removed some useless code in mod_typing that was redundant with safe_typing.

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

5 files changed, 13 insertions, 78 deletions

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 8bb616d8b..fb134b1c7 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -79,7 +79,6 @@ type specification_entry =
 and module_type_entry = 
     MTEident of kernel_name
   | MTEfunsig of mod_bound_id * module_type_entry * module_type_entry
-  | MTEsig of mod_self_id * module_signature_entry
   | MTEwith of module_type_entry * with_declaration
 
 and module_signature_entry = (label * specification_entry) list
@@ -91,7 +90,6 @@ and with_declaration =
 and module_expr = 
     MEident of module_path
   | MEfunctor of mod_bound_id * module_type_entry * module_expr
-  | MEstruct of mod_self_id * module_structure
   | MEapply of module_expr * module_expr
 
 and module_structure = (label * specification_entry) list
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 2e40099b3..61c0b8c3b 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -78,7 +78,6 @@ type specification_entry =
 and module_type_entry = 
     MTEident of kernel_name
   | MTEfunsig of mod_bound_id * module_type_entry * module_type_entry
-  | MTEsig of mod_self_id * module_signature_entry
   | MTEwith of module_type_entry * with_declaration
 
 and module_signature_entry = (label * specification_entry) list
@@ -90,7 +89,6 @@ and with_declaration =
 and module_expr = 
     MEident of module_path
   | MEfunctor of mod_bound_id * module_type_entry * module_expr
-  | MEstruct of mod_self_id * module_structure
   | MEapply of module_expr * module_expr
 
 and module_structure = (label * specification_entry) list
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index e9bca9065..ad5df805b 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -54,9 +54,6 @@ let rec translate_modtype env mte =
 	  add_module (MPbound arg_id) (module_body_of_type arg_b) env in
 	let body_b = translate_modtype env' body_e in
 	  MTBfunsig (arg_id,arg_b,body_b)
-    | MTEsig (msid,sig_e) ->
-	let str_b,sig_b = translate_entry_list env msid false sig_e in
-	  MTBsig (msid,sig_b)
     | MTEwith (mte, with_decl) ->
 	let mtb = translate_modtype env mte in
 	  merge_with env mtb with_decl
@@ -162,47 +159,8 @@ and merge_with env mtb with_decl =
 	Not_found -> error_no_such_label l
       | Reduction.NotConvertible -> error_with_incorrect l
 
-and translate_entry_list env msid is_definition sig_e = 
-  let mp = MPself msid in
-  let do_entry env (l,e) = 
-    let kn = make_kn mp empty_dirpath l in
-    let con = make_con mp empty_dirpath l in
-    match e with
-      | SPEconst ce ->
-	  let cb = translate_constant env con ce in
-	    begin match cb.const_hyps with
-	      |	(_::_) -> error_local_context (Some l)
-	      | [] ->
-		  add_constant con cb env, (l, SEBconst cb), (l, SPBconst cb)
-	    end
-      | SPEmind mie -> 
-	  let mib = translate_mind env mie in
-	    begin match mib.mind_hyps with
-	      |	(_::_) -> error_local_context (Some l)
-	      | [] ->
-		  add_mind kn mib env, (l, SEBmind mib), (l, SPBmind mib)
-	    end
-      | SPEmodule me ->
-	  let mb = translate_module env is_definition me in
-	  let mspec = 
-	    { msb_modtype = mb.mod_type;
-	      msb_equiv = mb.mod_equiv;
-	      msb_constraints = mb.mod_constraints }
-	  in
-	  let mp' = MPdot (mp,l) in
-	    add_module mp' mb env, (l, SEBmodule mb), (l, SPBmodule mspec)
-      | SPEmodtype mte ->
-	  let mtb = translate_modtype env mte in
-	    add_modtype kn mtb env, (l, SEBmodtype mtb), (l, SPBmodtype mtb)
-  in
-  let _,str_b,sig_b = list_fold_map2 do_entry env sig_e
-  in
-    str_b,sig_b
-
-(* if [is_definition=true], [mod_entry_expr] may be any expression.
-   Otherwise it must be a path *)
 
-and translate_module env is_definition me =
+and translate_module env  me =
   match me.mod_entry_expr, me.mod_entry_type with
     | None, None -> 
 	anomaly "Mod_typing.translate_module: empty type and expr in module entry"
@@ -222,18 +180,7 @@ and translate_module env is_definition me =
 	  with 
 	    | Not_path -> None
 	in
-	let meb,mtb1 = 
-	  if is_definition then
-	    translate_mexpr env mexpr
-	  else 
-	    let mp = 
-	      try 
-		path_of_mexpr mexpr 
-	      with 
-		| Not_path -> error_declaration_not_path mexpr
-	    in
-	      MEBident mp, type_modpath env mp
-	in
+	let meb,mtb1 = translate_mexpr env mexpr in
 	let mtb, mod_user_type, cst =
 	  match me.mod_entry_type with
 	    | None -> mtb1, None, Constraint.empty
@@ -279,14 +226,9 @@ and translate_mexpr env mexpr = match mexpr with
            functor application. *)
 	subst_modtype 
          (map_mbid farg_id mp (Some resolve)) fbody_b
-  | MEstruct (msid,structure) ->
-      let structure,signature = translate_entry_list env msid true structure in
-	MEBstruct (msid,structure),
-	MTBsig (msid,signature)
-
+ 
 
-(* is_definition is true - me.mod_entry_expr may be any expression *)
-let translate_module env me = translate_module env true me
+let translate_module env me = translate_module env  me
 
 let rec add_module_expr_constraints env = function
   | MEBident _ -> env
diff --git a/library/declaremods.ml b/library/declaremods.ml
index eb005e6d6..8bfc7ac85 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -131,7 +131,6 @@ let rec check_sig env = function
 
 let rec check_sig_entry env = function
   | MTEident kn -> check_sig env (Environ.lookup_modtype kn env)
-  | MTEsig _ -> ()
   | MTEfunsig _ -> Modops.error_result_must_be_signature ()
   | MTEwith (mte,_) -> check_sig_entry env mte
 
@@ -420,9 +419,7 @@ let rec get_modtype_substobjs = function
       let substobjs = get_modtype_substobjs mty in
       let modobjs = MPmap.find mp !modtab_substobjs in
 	replace_module_object idl substobjs modobjs
-  | MTEsig (msid,_) -> 
-      todo "Anonymous module types"; (empty_subst, [], msid, [])
-
+ 
 (* push names of bound modules (and their components) to Nametab *)
 (* add objects associated to them *)
 let process_module_bindings argids args =
@@ -440,8 +437,7 @@ let replace_module mtb id mb = todo "replace module after with"; mtb
 
 let rec get_some_body mty env = match mty with
     MTEident kn -> Environ.lookup_modtype kn env 
-  | MTEfunsig _ 
-  | MTEsig _ -> anomaly "anonymous module types not supported"
+  | MTEfunsig _ -> anomaly "anonymous module types not supported"
   | MTEwith (mty,With_Definition _) -> get_some_body mty env 
   | MTEwith (mty,With_Module (id,mp)) -> 
       replace_module (get_some_body mty env) id (Environ.lookup_module mp env)
@@ -517,9 +513,6 @@ let end_module id =
 	  (empty_subst, mbids, msid, substitute), keep, special
       | Some (MTEident ln) ->
 	  abstract_substobjs mbids (KNmap.find ln (!modtypetab)), [], []
-      | Some (MTEsig (msid,_)) ->
-	  todo "Anonymous signatures not supported";
-	  (empty_subst, mbids, msid, []), keep, special
       | Some (MTEwith _ as mty) ->
 	  abstract_substobjs mbids (get_modtype_substobjs mty), [], []
       | Some (MTEfunsig _) -> 
@@ -711,8 +704,6 @@ let rec get_module_substobjs env = function
   | MEfunctor (mbid,mty,mexpr) ->
        let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
 	(subst, mbid::mbids, msid, objs)
-  | MEstruct (msid,_) ->
-      (empty_subst, [], msid, [])
   | MEapply (mexpr, MEident mp) ->
       let feb,ftb = Mod_typing.translate_mexpr env mexpr in
       let ftb = Modops.scrape_modtype env ftb in
@@ -726,7 +717,7 @@ let rec get_module_substobjs env = function
                   objects (that are all non-logical objects) *)
 	       (add_mbid mbid mp (Some resolve) subst, mbids, msid, objs)
 	   | [] -> match mexpr with
-	       | MEident _ | MEstruct _ -> error "Application of a non-functor"
+	       | MEident _  -> error "Application of a non-functor"
 	       | _ -> error "Application of a functor with too few arguments")
   | MEapply (_,mexpr) ->
       Modops.error_application_to_not_path mexpr
diff --git a/test-suite/modules/pseudo_circular_with.v b/test-suite/modules/pseudo_circular_with.v
new file mode 100644
index 000000000..9e46d17ed
--- /dev/null
+++ b/test-suite/modules/pseudo_circular_with.v
@@ -0,0 +1,6 @@
+Module Type S. End S.
+Module Type T. Declare Module M:S. End T.
+Module N:S. End N.
+
+Module NN:T. Module M:=N. End NN.
+Module Type U := T with Module M:=NN.
\ No newline at end of file