Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

7 files changed, 53 insertions, 52 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 40ac604e..82df62b4 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -211,7 +211,7 @@ let locate_absolute_library dir =
   if loadpath = [] then raise LibUnmappedDir;
   try
     let name = string_of_id base^".vo" in
-    let _, file = System.where_in_path false loadpath name in
+    let _, file = System.where_in_path ~warn:false loadpath name in
     (dir, file)
   with Not_found ->
   (* Last chance, removed from the file system but still in memory *)
@@ -231,7 +231,7 @@ let locate_qualified_library qid =
     in
     if loadpath = [] then raise LibUnmappedDir;
     let name =  qid.basename^".vo" in
-    let path, file = System.where_in_path true loadpath name in
+    let path, file = System.where_in_path loadpath name in
     let dir =
       extend_dirpath (find_logical_path path) (id_of_string qid.basename) in
     (* Look if loaded *)
diff --git a/checker/checker.ml b/checker/checker.ml
index 1ed094cf..3d928933 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -43,7 +43,8 @@ let (/) = Filename.concat
 
 let get_version_date () =
   try
-    let ch = open_in (Coq_config.coqlib^"/revision") in
+    let coqlib = Envars.coqlib () in 
+    let ch = open_in (Filename.concat coqlib "revision") in
     let ver = input_line ch in
     let rev = input_line ch in
       (ver,rev)
@@ -108,13 +109,9 @@ let set_rec_include d p =
   check_coq_overwriting p;
   push_rec_include(d,p)
 
-(* Initializes the LoadPath according to COQLIB and Coq_config *)
+(* Initializes the LoadPath *)
 let init_load_path () =
-  let coqlib =
-    (* variable COQLIB overrides the default library *)
-    getenv_else "COQLIB"
-      (if Coq_config.local || !Flags.boot then Coq_config.coqtop
-	else Coq_config.coqlib) in
+  let coqlib = Envars.coqlib () in
   let user_contrib = coqlib/"user-contrib" in
   let contrib = coqlib/"contrib" in
   (* first user-contrib *)
@@ -323,7 +320,7 @@ let parse_args() =
     | "-debug" :: rem -> set_debug (); parse rem
 
     | "-where" :: _ ->
-        print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0
+        print_endline (Envars.coqlib ()); exit 0
 
     | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
 
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 71b6c9ca..2cf3854a 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -562,7 +562,7 @@ type structure_field_body =
   | SFBconst of constant_body
   | SFBmind of mutual_inductive_body
   | SFBmodule of module_body
-  | SFBalias of module_path * Univ.constraints option
+  | SFBalias of module_path * struct_expr_body option * Univ.constraints option
   | SFBmodtype of module_type_body
 
 and structure_body = (label * structure_field_body) list
@@ -576,7 +576,8 @@ and struct_expr_body =
   | SEBwith of struct_expr_body * with_declaration_body
 
 and with_declaration_body =
-    With_module_body of identifier list * module_path * Univ.constraints
+    With_module_body of identifier list * module_path *
+      struct_expr_body option * Univ.constraints
   | With_definition_body of  identifier list * constant_body
         
 and module_body = 
@@ -592,13 +593,14 @@ and module_type_body =
       typ_alias : substitution}
 
 	
-let subst_with_body sub = function
-  | With_module_body(id,mp,cst) ->
-      With_module_body(id,subst_mp sub mp,cst)
+let rec subst_with_body sub = function
+  | With_module_body(id,mp,typ_opt,cst) ->
+      With_module_body(id,subst_mp sub mp,
+		       Option.smartmap (subst_struct_expr sub) typ_opt,cst)
   | With_definition_body(id,cb) ->
       With_definition_body( id,subst_const_body sub cb)
 
-let rec subst_modtype sub mtb =
+and subst_modtype sub mtb =
   let typ_expr' = subst_struct_expr sub mtb.typ_expr in
     if typ_expr'==mtb.typ_expr then
       mtb
@@ -616,8 +618,8 @@ and subst_structure sub sign =
 	SFBmodule (subst_module sub mb)
     | SFBmodtype mtb -> 
 	SFBmodtype (subst_modtype sub mtb)
-    | SFBalias (mp,cst) ->
-	SFBalias (subst_mp sub mp,cst)
+    | SFBalias (mp,typ_opt ,cst) ->
+	SFBalias (subst_mp sub mp,Option.smartmap (subst_struct_expr sub) typ_opt,cst)
   in
     List.map (fun (l,b) -> (l,subst_body b)) sign
 
diff --git a/checker/declarations.mli b/checker/declarations.mli
index fdea3383..78bf2053 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -150,7 +150,8 @@ type structure_field_body =
   | SFBconst of constant_body
   | SFBmind of mutual_inductive_body
   | SFBmodule of module_body
-  | SFBalias of module_path * Univ.constraints option
+  | SFBalias of module_path * struct_expr_body option 
+      * Univ.constraints option
   | SFBmodtype of module_type_body
 
 and structure_body = (label * structure_field_body) list
@@ -164,7 +165,8 @@ and struct_expr_body =
   | SEBwith of struct_expr_body * with_declaration_body
 
 and with_declaration_body =
-    With_module_body of identifier list * module_path * Univ.constraints
+    With_module_body of identifier list * module_path *
+      struct_expr_body option * Univ.constraints
   | With_definition_body of  identifier list * constant_body
         
 and module_body = 
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 379273af..af5e4f46 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -145,9 +145,9 @@ and check_with_aux_def env mtb with_decl =
     | _ -> error_signature_expected mtb
   in
   let id,idl = match with_decl with 
-    | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_) ->
+    | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) ->
                                            id,idl
-    | With_definition_body ([],_) | With_module_body ([],_,_) -> assert false
+    | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false
   in
   let l = label_of_id id in
     try
@@ -173,8 +173,8 @@ and check_with_aux_def env mtb with_decl =
 			let new_with_decl = match with_decl with
 			    With_definition_body (_,c) ->
                               With_definition_body (idl,c)
-			  | With_module_body (_,c,cst) ->
-                              With_module_body (idl,c,cst) in 
+			  | With_module_body (_,c,t,cst) ->
+                              With_module_body (idl,c,t,cst) in 
 			  check_with_aux_def env' (type_of_mb env old) new_with_decl
                     | Some msb ->
 			error_a_generative_module_expected l
@@ -192,9 +192,9 @@ and check_with_aux_mod env mtb with_decl =
 	msid,msid',(subst_signature_msid msid (MPself(msid')) sig_b)
     | _ -> error_signature_expected mtb in
   let id,idl = match with_decl with 
-    | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_) ->
+    | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) ->
         id,idl
-    | With_definition_body ([],_) | With_module_body ([],_,_) -> assert false
+    | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false
   in
   let l = label_of_id id in
     try
@@ -206,11 +206,11 @@ and check_with_aux_mod env mtb with_decl =
       in 
       let env' = Modops.add_signature (MPself msid) before env in
 	match with_decl with
-          | With_module_body ([],_,_) -> assert false
-	  | With_module_body ([id], mp,_) ->
+          | With_module_body ([],_,_,_) -> assert false
+	  | With_module_body ([id], mp,_,_) ->
 	      let old,alias = match spec with
 		  SFBmodule msb -> Some msb,None
-		| SFBalias (mp',_) -> None,Some mp'
+		| SFBalias (mp',_,_) -> None,Some mp'
 		| _ -> error_not_a_module l
 	      in
 	      let mtb' = lookup_modtype mp env' in
@@ -223,7 +223,7 @@ and check_with_aux_mod env mtb with_decl =
 		      anomaly "Mod_typing:no implementation and no alias"
 	      in
 		join (map_mp (mp_rec [id]) mp) mtb'.typ_alias
-        | With_module_body (_::_,mp,_) -> 
+        | With_module_body (_::_,mp,_,_) -> 
 	    let old = match spec with
 		SFBmodule msb -> msb
 	      | _ -> error_not_a_module l
@@ -234,8 +234,8 @@ and check_with_aux_mod env mtb with_decl =
                       let new_with_decl = match with_decl with
 			  With_definition_body (_,c) -> 
 			    With_definition_body (idl,c)
-			| With_module_body (_,c,cst) ->
-                            With_module_body (idl,c,cst) in
+			| With_module_body (_,c,t,cst) ->
+                            With_module_body (idl,c,t,cst) in
 		      let sub =
 			check_with_aux_mod env' 
 			  (type_of_mb env old) new_with_decl in
@@ -290,7 +290,7 @@ and check_structure_field (s,env) mp lab = function
       let is_fun, sub = Modops.update_subst env msb mp1 in
       ((if is_fun then s else join s sub),
        Modops.add_module (MPdot(mp,lab)) msb env)
-  | SFBalias(mp2,cst) ->
+  | SFBalias(mp2,_,cst) ->
       (* cf Safe_typing.add_alias *)
       (try
         let mp' = MPdot(mp,lab) in
diff --git a/checker/modops.ml b/checker/modops.ml
index f79e52c2..27ea4d55 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -145,7 +145,7 @@ let rec eval_struct env = function
 			   (join sub_alias (map_mbid farg_id mp)) fbody_b)
   | SEBwith (mtb,(With_definition_body _ as wdb)) ->
       merge_with env mtb wdb empty_subst
-  | SEBwith (mtb, (With_module_body (_,mp,_) as wdb)) ->
+  | SEBwith (mtb, (With_module_body (_,mp,_,_) as wdb)) ->
       let alias_in_mp =
 	(lookup_modtype mp env).typ_alias in
 	merge_with env mtb wdb alias_in_mp
@@ -167,8 +167,8 @@ and merge_with env mtb with_decl alias=
     | _ -> error_signature_expected mtb
   in
   let id,idl = match with_decl with 
-    | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_) -> id,idl
-    | With_definition_body ([],_) | With_module_body ([],_,_) -> assert false
+    | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) -> id,idl
+    | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false
   in
   let l = label_of_id id in
     try
@@ -180,15 +180,15 @@ and merge_with env mtb with_decl alias=
       in 
       let new_spec,subst = match with_decl with
         | With_definition_body ([],_)
-        | With_module_body ([],_,_) -> assert false
+        | With_module_body ([],_,_,_) -> assert false
 	| With_definition_body ([id],c) -> 
 	    SFBconst c,None
-	| With_module_body ([id], mp,cst) ->
+	| With_module_body ([id], mp,typ_opt,cst) ->
 	    let mp' = scrape_alias mp env in
-	      SFBalias (mp,Some cst),
+	      SFBalias (mp,typ_opt,Some cst),
 	    Some(join (map_mp (mp_rec [id]) mp') alias)
 	| With_definition_body (_::_,_) 
-        | With_module_body (_::_,_,_) -> 
+        | With_module_body (_::_,_,_,_) -> 
 	    let old = match spec with
 		SFBmodule msb -> msb
 	      | _ -> error_not_a_module l
@@ -196,8 +196,8 @@ and merge_with env mtb with_decl alias=
             let new_with_decl,subst1 = 
 	      match with_decl with
                   With_definition_body (_,c) -> With_definition_body (idl,c),None
-		| With_module_body (idc,mp,cst) -> 
-		    With_module_body (idl,mp,cst),
+		| With_module_body (idc,mp,t,cst) -> 
+		    With_module_body (idl,mp,t,cst),
 		      Some(map_mp (mp_rec idc) mp) 
 	    in
 	    let subst = Option.fold_right join subst1 alias in
@@ -227,7 +227,7 @@ and add_signature mp sign env =
 	| SFBmodule mb -> 
 	    add_module (MPdot (mp,l)) mb env 
 	      (* adds components as well *)
-	| SFBalias (mp1,cst) -> 
+	| SFBalias (mp1,_,cst) -> 
 	    Environ.register_alias (MPdot(mp,l)) mp1 env
 	| SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l)) 
 	    mtb env
@@ -257,7 +257,7 @@ and  constants_of_specification env mp sign =
        let new_env =  add_module (MPdot (mp,l)) mb env in 
        new_env,(constants_of_modtype env (MPdot (mp,l))
 		   (type_of_mb env mb)) @ res
-   | SFBalias (mp1,cst) ->
+   | SFBalias (mp1,_,cst) ->
        let new_env =  register_alias (MPdot (mp,l)) mp1 env in 
        new_env,(constants_of_modtype env (MPdot (mp,l))
 		   (eval_struct env (SEBident mp1))) @ res
@@ -323,7 +323,7 @@ and strengthen_sig env msid sign mp = match sign with
 	  (MPdot (MPself msid,l)) mb env in
         let rest' = strengthen_sig env' msid rest mp in
 	item':: rest'
-  | ((l,SFBalias (mp1,cst)) as item) :: rest ->
+  | ((l,SFBalias (mp1,_,cst)) as item) :: rest ->
       let env' = register_alias (MPdot(MPself msid,l)) mp1 env in
       let rest' = strengthen_sig env' msid rest mp in
 	item::rest'
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index fb95b606..7a6868fe 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -32,7 +32,7 @@ type namedobject =
   | IndConstr of constructor * mutual_inductive_body
   | Module of module_body
   | Modtype of module_type_body
-  | Alias of module_path
+  | Alias of module_path * struct_expr_body option
 
 (* adds above information about one mutual inductive: all types and
    constructors *)
@@ -63,7 +63,7 @@ let make_label_map mp list =
        add_nameobjects_of_mib (make_kn mp empty_dirpath l) mib map
     | SFBmodule mb -> add_map (Module mb)
     | SFBmodtype mtb -> add_map (Modtype mtb)
-    | SFBalias (mp,cst) -> add_map (Alias mp)
+    | SFBalias (mp,t,cst) -> add_map (Alias (mp,t))
   in
     List.fold_right add_one list Labmap.empty
 
@@ -308,23 +308,23 @@ and check_signatures env (msid1,sig1) alias (msid2,sig2') =
 	    begin
 	      match info1 with
 		| Module msb -> check_modules env msid1 l msb msb2
-		| Alias mp ->let msb = 
+		| Alias (mp,typ_opt) ->let msb = 
 		    {mod_expr = Some (SEBident mp);
-		     mod_type = Some (eval_struct env (SEBident mp));
+		     mod_type = typ_opt;
 		     mod_constraints = Constraint.empty;
 		     mod_alias = (lookup_modtype mp env).typ_alias;
 		     mod_retroknowledge = []} in
 		    check_modules env msid1 l msb msb2
 		| _ -> error_not_match l spec2
 	    end
-	| SFBalias (mp,_) ->
+	| SFBalias (mp,typ_opt,_) ->
 	    begin	
 	      match info1 with
-		| Alias mp1 -> check_modpath_equiv env mp mp1
+		| Alias (mp1,_) -> check_modpath_equiv env mp mp1
 		| Module msb -> 
 		    let msb1 = 
 		      {mod_expr = Some (SEBident mp);
-		       mod_type = Some (eval_struct env (SEBident mp));
+		       mod_type = typ_opt;
 		       mod_constraints = Constraint.empty;
 		       mod_alias = (lookup_modtype mp env).typ_alias;
 		       mod_retroknowledge = []} in