Imported Upstream version 8.1.pl3+dfsgupstream/8.1.pl3+dfsg

2 files changed, 51 insertions, 7 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 4fe90ffd..a6fd6d04 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indtypes.ml 9633 2007-02-09 18:40:26Z herbelin $ *)
+(* $Id: indtypes.ml 10297 2007-11-07 11:05:53Z barras $ *)
 
 open Util
 open Names
@@ -29,6 +29,9 @@ let weaker_noccur_between env x nvars t =
    if noccur_between x nvars t' then Some t'
    else None
 
+let is_constructor_head t =
+  isRel(fst(decompose_app t))
+
 (************************************************************************)
 (* Various well-formedness check for inductive declarations            *)
 
@@ -116,6 +119,7 @@ let is_unit constrsinfos =
    | _ -> false
 
 let rec infos_and_sort env t =
+  let t = whd_betadeltaiota env t in
   match kind_of_term t with
     | Prod (name,c1,c2) ->
         let (varj,_) = infer_type env c1 in
@@ -123,8 +127,8 @@ let rec infos_and_sort env t =
 	let logic = is_logic_type varj in
 	let small = Term.is_small varj.utj_type in
 	(logic,small) :: (infos_and_sort env1 c2)
-    | Cast (c,_,_) -> infos_and_sort env c
-    | _ -> []
+    | _ when is_constructor_head t -> []
+    | _ -> anomaly "infos_and_sort: not a positive constructor"
 
 let small_unit constrsinfos =
   let issmall = List.for_all is_small constrsinfos 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index c4d9c991..5f01613c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: safe_typing.ml 9310 2006-10-28 19:35:09Z herbelin $ *)
+(* $Id: safe_typing.ml 10276 2007-10-30 11:37:54Z barras $ *)
 
 open Util
 open Names
@@ -42,6 +42,11 @@ type module_info =
 let check_label l labset = 
   if Labset.mem l labset then error_existing_label l
 
+let set_engagement_opt oeng env =
+  match oeng with
+      Some eng -> set_engagement eng env
+    | _ -> env
+
 type library_info = dir_path * Digest.t
 
 type safe_environment = 
@@ -51,6 +56,8 @@ type safe_environment =
       labset : Labset.t;
       revsign : module_signature_body;
       revstruct : module_structure_body;
+      univ : Univ.constraints;
+      engagement : engagement option;
       imports : library_info list;
       loads : (module_path * module_body) list }
 
@@ -78,6 +85,8 @@ let rec empty_environment =
     labset = Labset.empty;
     revsign = [];
     revstruct = [];
+    univ = Univ.Constraint.empty;
+    engagement = None;
     imports = [];
     loads = [] }
 
@@ -153,6 +162,8 @@ let add_constant dir l decl senv =
 	  labset = Labset.add l senv.labset;
 	  revsign = (l,SPBconst cb)::senv.revsign;
 	  revstruct = (l,SEBconst cb)::senv.revstruct;
+          univ = senv.univ;
+          engagement = senv.engagement;
 	  imports = senv.imports;
 	  loads = senv.loads }
     
@@ -180,6 +191,8 @@ let add_mind dir l mie senv =
 	labset = Labset.add l senv.labset;  (* TODO: the same as above *)
 	revsign = (l,SPBmind mib)::senv.revsign;
 	revstruct = (l,SEBmind mib)::senv.revstruct;
+        univ = senv.univ;
+        engagement = senv.engagement;
 	imports = senv.imports;
 	loads = senv.loads }
 
@@ -198,6 +211,8 @@ let add_modtype l mte senv =
 	labset = Labset.add l senv.labset;
 	revsign = (l,SPBmodtype mtb)::senv.revsign;
 	revstruct = (l,SEBmodtype mtb)::senv.revstruct;
+        univ = senv.univ;
+        engagement = senv.engagement;
 	imports = senv.imports;
 	loads = senv.loads }
 
@@ -223,6 +238,8 @@ let add_module l me senv =
 	labset = Labset.add l senv.labset;
 	revsign = (l,SPBmodule mspec)::senv.revsign;
 	revstruct = (l,SEBmodule mb)::senv.revstruct;
+        univ = senv.univ;
+        engagement = senv.engagement;
 	imports = senv.imports;
 	loads = senv.loads }
 
@@ -245,6 +262,8 @@ let start_module l senv =
 	labset = Labset.empty;
 	revsign = [];
 	revstruct = [];
+        univ = Univ.Constraint.empty;
+        engagement = None;
 	imports = senv.imports;
 	loads = [] }
 
@@ -274,6 +293,7 @@ let end_module l restype senv =
 	  let mtb = functorize_type res_tb in
 	    mtb, Some mtb, cst
   in
+  let cst = Constraint.union cst senv.univ in
   let mexpr = 
     List.fold_left
       (fun mtb (arg_id,arg_b) -> MEBfunctor (arg_id,arg_b,mtb))
@@ -294,6 +314,7 @@ let end_module l restype senv =
   in
   let mp = MPdot (oldsenv.modinfo.modpath, l) in
   let newenv = oldsenv.env in
+  let newenv = set_engagement_opt senv.engagement newenv in
   let newenv = 
     List.fold_left
       (fun env (mp,mb) -> full_add_module mp mb env) 
@@ -309,6 +330,9 @@ let end_module l restype senv =
 	labset = Labset.add l oldsenv.labset;
 	revsign = (l,SPBmodule mspec)::oldsenv.revsign;
 	revstruct = (l,SEBmodule mb)::oldsenv.revstruct;
+        univ = oldsenv.univ;
+        (* engagement is propagated to the upper level *)
+        engagement = senv.engagement;
 	imports = senv.imports;
 	loads = senv.loads@oldsenv.loads }
 
@@ -333,6 +357,8 @@ let add_module_parameter mbid mte senv =
     labset = senv.labset;
     revsign = [];
     revstruct = [];
+    univ = senv.univ;
+    engagement = senv.engagement;
     imports = senv.imports;
     loads = [] }
 
@@ -355,6 +381,8 @@ let start_modtype l senv =
 	labset = Labset.empty;
 	revsign = [];
 	revstruct = [];
+        univ = Univ.Constraint.empty;
+        engagement = None;
 	imports = senv.imports;
 	loads = [] }
 
@@ -377,6 +405,10 @@ let end_modtype l senv =
   in
   let kn = make_kn oldsenv.modinfo.modpath empty_dirpath l in
   let newenv = oldsenv.env in
+  (* since universes constraints cannot be stored in the modtype,
+     they are propagated to the upper level *)
+  let newenv = add_constraints senv.univ  newenv in
+  let newenv = set_engagement_opt senv.engagement newenv in
   let newenv = 
     List.fold_left
       (fun env (mp,mb) -> full_add_module mp mb env) 
@@ -395,6 +427,8 @@ let end_modtype l senv =
 	labset = Labset.add l oldsenv.labset;
 	revsign = (l,SPBmodtype mtb)::oldsenv.revsign;
 	revstruct = (l,SEBmodtype mtb)::oldsenv.revstruct;
+        univ = Univ.Constraint.union senv.univ oldsenv.univ;
+        engagement = senv.engagement;
 	imports = senv.imports;
 	loads = senv.loads@oldsenv.loads }
   
@@ -404,7 +438,9 @@ let current_msid senv = senv.modinfo.msid
 
 
 let add_constraints cst senv = 
-  {senv with env = Environ.add_constraints cst senv.env}
+  {senv with
+    env = Environ.add_constraints cst senv.env;
+    univ = Univ.Constraint.union cst senv.univ }
 
 (* Check that the engagement expected by a library matches the initial one *)
 let check_engagement env c =
@@ -415,7 +451,9 @@ let check_engagement env c =
         error "Needs option -impredicative-set"
 
 let set_engagement c senv =
-  {senv with env = Environ.set_engagement c senv.env}
+  {senv with
+    env = Environ.set_engagement c senv.env;
+    engagement = Some c }
 
 (* Libraries = Compiled modules *)
 
@@ -454,6 +492,8 @@ let start_library dir senv =
 	labset = Labset.empty;
 	revsign = [];
 	revstruct = [];
+        univ = Univ.Constraint.empty;
+        engagement = None;
 	imports = senv.imports;
 	loads = [] }
 
@@ -475,7 +515,7 @@ let export senv dir =
       mod_type = MTBsig (modinfo.msid, List.rev senv.revsign);
       mod_user_type = None;
       mod_equiv = None;
-      mod_constraints = Constraint.empty }
+      mod_constraints = senv.univ }
   in
     modinfo.msid, (dir,mb,senv.imports,engagement senv.env)