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

13 files changed, 81 insertions, 58 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index ad435eb5..86e02623 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: environ.ml 11001 2008-05-27 16:56:07Z aspiwack $ *)
+(* $Id: environ.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Util
 open Names
@@ -379,17 +379,14 @@ let insert_after_hyp (ctxt,vals) id d check =
 
 (* To be used in Logic.clear_hyps *)
 let remove_hyps ids check_context check_value (ctxt, vals) =
-  let ctxt,vals,rmv = 
-    List.fold_right2 (fun (id,_,_ as d) (id',v) (ctxt,vals,rmv) ->
+  List.fold_right2 (fun (id,_,_ as d) (id',v) (ctxt,vals) ->
       if List.mem id ids then 
-	(ctxt,vals,id::rmv)
+	(ctxt,vals)
       else 	  
 	let nd = check_context d in
 	let nv = check_value v in
-	  (nd::ctxt,(id',nv)::vals,rmv))
-		     ctxt vals ([],[],[])
-  in ((ctxt,vals),rmv)
-
+	  (nd::ctxt,(id',nv)::vals))
+		     ctxt vals ([],[])
 
 
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 30f555a4..97e19782 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: environ.mli 11001 2008-05-27 16:56:07Z aspiwack $ i*)
+(*i $Id: environ.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -222,7 +222,7 @@ val insert_after_hyp : named_context_val -> variable ->
   named_declaration -> 
     (named_context -> unit) -> named_context_val
 
-val remove_hyps : identifier list -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val * identifier list
+val remove_hyps : identifier list -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val
 
 
 (* spiwack: functions manipulating the retroknowledge *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 7cedebbd..01b8aca1 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indtypes.ml 10920 2008-05-12 10:19:32Z herbelin $ *)
+(* $Id: indtypes.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Util
 open Names
@@ -254,16 +254,19 @@ let typecheck_inductive env mie =
     array_fold_map2' (fun ((id,full_arity,ar_level),cn,info,lc,_) lev cst ->
       let sign, s = dest_arity env full_arity in
       let status,cst = match s with
-      | Type _ when ar_level <> None (* Explicitly polymorphic *) ->
+      | Type u when ar_level <> None (* Explicitly polymorphic *) 
+            && no_upper_constraints u cst ->
 	  (* The polymorphic level is a function of the level of the *)
 	  (* conclusions of the parameters *)
-	  Inr (param_ccls, lev), cst
+          (* We enforce [u >= lev] in case [lev] has a strict upper *)
+          (* constraints over [u] *)
+	  Inr (param_ccls, lev), enforce_geq u lev cst
       | Type u (* Not an explicit occurrence of Type *) ->
 	  Inl (info,full_arity,s), enforce_geq u lev cst
       | Prop Pos when engagement env <> Some ImpredicativeSet ->
 	  (* Predicative set: check that the content is indeed predicative *)
 	  if not (is_type0m_univ lev) & not (is_type0_univ lev) then
-	    error "Large non-propositional inductive types must be in Type";
+	    error "Large non-propositional inductive types must be in Type.";
 	  Inl (info,full_arity,s), cst
       | Prop _ ->
 	  Inl (info,full_arity,s), cst in
@@ -598,7 +601,6 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
 	      poly_level = lev; 
 	    }, all_sorts
       | Inl ((issmall,isunit),ar,s) ->
-	  let isunit = isunit && ntypes = 1 && not (is_recursive recargs.(0)) in
 	  let kelim = allowed_sorts issmall isunit s in
 	    Monomorphic {
 		mind_user_arity = ar;
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 9415941d..4bb8e9d6 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: inductive.ml 10920 2008-05-12 10:19:32Z herbelin $ *)
+(* $Id: inductive.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Util
 open Names
@@ -218,7 +218,7 @@ let type_of_constructor cstr (mib,mip) =
   let specif = mip.mind_user_lc in
   let i = index_of_constructor cstr in
   let nconstr = Array.length mip.mind_consnames in
-  if i > nconstr then error "Not enough constructors in the type";
+  if i > nconstr then error "Not enough constructors in the type.";
   constructor_instantiate (fst ind) mib specif.(i-1)
 
 let arities_of_specif kn (mib,mip) = 
@@ -228,7 +228,9 @@ let arities_of_specif kn (mib,mip) =
 let arities_of_constructors ind specif = 
   arities_of_specif (fst ind) specif
 
-
+let type_of_constructors ind (mib,mip) =
+  let specif = mip.mind_user_lc in
+  Array.map (constructor_instantiate (fst ind) mib) specif
 
 (************************************************************************)
 
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index c2c38d8d..8059051b 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: inductive.mli 9420 2006-12-08 15:34:09Z barras $ i*)
+(*i $Id: inductive.mli 11301 2008-08-04 19:41:18Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -47,6 +47,9 @@ val type_of_constructor : constructor -> mind_specif -> types
 (* Return constructor types in normal form *)
 val arities_of_constructors : inductive -> mind_specif -> types array
 
+(* Return constructor types in user form *)
+val type_of_constructors : inductive -> mind_specif -> types array
+
 (* Transforms inductive specification into types (in nf) *)
 val arities_of_specif : mutual_inductive -> mind_specif -> types array 
 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 9242a757..7bed3254 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modops.ml 11142 2008-06-18 15:37:31Z soubiran $ i*)
+(*i $Id: modops.ml 11309 2008-08-06 10:30:35Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -22,51 +22,51 @@ open Mod_subst
 
 
 let error_existing_label l = 
-  error ("The label "^string_of_label l^" is already declared")
+  error ("The label "^string_of_label l^" is already declared.")
 
-let error_declaration_not_path _ = error "Declaration is not a path"
+let error_declaration_not_path _ = error "Declaration is not a path."
 
-let error_application_to_not_path _ = error "Application to not path"
+let error_application_to_not_path _ = error "Application to not path."
 
-let error_not_a_functor _ = error "Application of not a functor"
+let error_not_a_functor _ = error "Application of not a functor."
 
-let error_incompatible_modtypes _ _ = error "Incompatible module types"
+let error_incompatible_modtypes _ _ = error "Incompatible module types."
 
-let error_not_equal _ _ = error "Not equal modules"
+let error_not_equal _ _ = error "Non equal modules."
 
-let error_not_match l _ = error ("Signature components for label "^string_of_label l^" do not match")
+let error_not_match l _ = error ("Signature components for label "^string_of_label l^" do not match.")
 
-let error_no_such_label l = error ("No such label "^string_of_label l)
+let error_no_such_label l = error ("No such label "^string_of_label l^".")
 
 let error_incompatible_labels l l' = 
   error ("Opening and closing labels are not the same: "
 	 ^string_of_label l^" <> "^string_of_label l'^" !")
 
 let error_result_must_be_signature () = 
-  error "The result module type must be a signature"
+  error "The result module type must be a signature."
 
 let error_signature_expected mtb =
-  error "Signature expected"
+  error "Signature expected."
 
 let error_no_module_to_end _ = 
-  error "No open module to end"
+  error "No open module to end."
 
 let error_no_modtype_to_end _ =
-  error "No open module type to end"
+  error "No open module type to end."
 
 let error_not_a_modtype_loc loc s = 
-  user_err_loc (loc,"",str ("\""^s^"\" is not a module type"))
+  user_err_loc (loc,"",str ("\""^s^"\" is not a module type."))
 
 let error_not_a_module_loc loc s = 
-  user_err_loc (loc,"",str ("\""^s^"\" is not a module"))
+  user_err_loc (loc,"",str ("\""^s^"\" is not a module."))
 
 let error_not_a_module s = error_not_a_module_loc dummy_loc s
 
 let error_not_a_constant l = 
-  error ("\""^(string_of_label l)^"\" is not a constant")
+  error ("\""^(string_of_label l)^"\" is not a constant.")
 
 let error_with_incorrect l =
-  error ("Incorrect constraint for label \""^(string_of_label l)^"\"")
+  error ("Incorrect constraint for label \""^(string_of_label l)^"\".")
 
 let error_a_generative_module_expected l =
   error ("The module " ^ string_of_label l ^ " is not generative. Only " ^
@@ -79,7 +79,7 @@ let error_local_context lo =
 	error ("The local context is not empty.")
     | (Some l) ->
 	error ("The local context of the component "^
-	       (string_of_label l)^" is not empty")
+	       (string_of_label l)^" is not empty.")
 
 
 let error_no_such_label_sub l l1 l2 =
diff --git a/kernel/names.ml b/kernel/names.ml
index 26bcc2eb..25f03495 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: names.ml 10919 2008-05-11 22:04:26Z msozeau $ *)
+(* $Id: names.ml 11238 2008-07-19 09:34:03Z herbelin $ *)
 
 open Pp
 open Util
@@ -101,7 +101,7 @@ let label_of_mbid (_,s,_) = s
 
 
 let mk_label l = l
-let string_of_label l = l
+let string_of_label = string_of_id
 
 let id_of_label l = l
 let label_of_id id = id
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 6906fb29..3c7461b2 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 11170 2008-06-25 08:31:04Z soubiran $ *)
+(* $Id: safe_typing.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Util
 open Names
@@ -163,7 +163,7 @@ let safe_push_named (id,_,_ as d) env =
   let _ =
     try
       let _ = lookup_named id env in 
-      error ("identifier "^string_of_id id^" already defined")
+      error ("Identifier "^string_of_id id^" already defined.")
     with Not_found -> () in
   Environ.push_named d env
 
@@ -446,7 +446,7 @@ let end_module l restype senv =
    let senv = add_constraints (struct_expr_constraints struct_expr) senv in
    let msid,str = match (eval_struct senv.env struct_expr) with
      | SEBstruct(msid,str_l) -> msid,str_l
-     | _ -> error ("You cannot Include a higher-order Module or Module Type" )
+     | _ -> error ("You cannot Include a higher-order Module or Module Type.")
    in
    let mp_sup = senv.modinfo.modpath in
    let str1 = subst_signature_msid msid mp_sup str in
@@ -660,7 +660,7 @@ let check_engagement env c =
     | Some ImpredicativeSet, Some ImpredicativeSet -> ()
     | _, None -> ()
     | _, Some ImpredicativeSet ->
-        error "Needs option -impredicative-set"
+        error "Needs option -impredicative-set."
 
 let set_engagement c senv =
   {senv with
@@ -739,9 +739,10 @@ let check_imports senv needed =
     try
       let actual_stamp = List.assoc id imports in
       if stamp <> actual_stamp then
-	error ("Inconsistent assumptions over module " ^(string_of_dirpath id))
+	error
+	  ("Inconsistent assumptions over module "^(string_of_dirpath id)^".")
     with Not_found -> 
-      error ("Reference to unknown module " ^ (string_of_dirpath id))
+      error ("Reference to unknown module "^(string_of_dirpath id)^".")
   in
   List.iter check needed
 
diff --git a/kernel/term.ml b/kernel/term.ml
index c920c80b..1f3d2635 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: term.ml 10859 2008-04-27 16:46:15Z herbelin $ *)
+(* $Id: term.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 (* This module instantiates the structure of generic deBruijn terms to Coq *)
 
@@ -370,16 +370,22 @@ let destProd c = match kind_of_term c with
   | Prod (x,t1,t2) -> (x,t1,t2) 
   | _ -> invalid_arg "destProd"
 
+let isProd c = match kind_of_term c with | Prod _ -> true | _ -> false
+
 (* Destructs the abstraction [x:t1]t2 *)
 let destLambda c = match kind_of_term c with 
   | Lambda (x,t1,t2) -> (x,t1,t2) 
   | _ -> invalid_arg "destLambda"
 
+let isLambda c = match kind_of_term c with | Lambda _ -> true | _ -> false
+
 (* Destructs the let [x:=b:t1]t2 *)
 let destLetIn c = match kind_of_term c with 
   | LetIn (x,b,t1,t2) -> (x,b,t1,t2) 
   | _ -> invalid_arg "destProd"
 
+let isLetIn c =  match kind_of_term c with LetIn _ -> true | _ -> false
+
 (* Destructs an application *)
 let destApp c = match kind_of_term c with
   | App (f,a) -> (f, a)
@@ -389,10 +395,6 @@ let destApplication = destApp
 
 let isApp c = match kind_of_term c with App _ -> true | _ -> false
 
-let isProd c = match kind_of_term c with | Prod _ -> true | _ -> false
-
-let isLambda c = match kind_of_term c with | Lambda _ -> true | _ -> false
-
 (* Destructs a constant *)
 let destConst c = match kind_of_term c with
   | Const kn -> kn
@@ -419,22 +421,27 @@ let destConstruct c = match kind_of_term c with
   | Construct (kn, a as r) -> r
   | _ -> invalid_arg "dest"
 
-let isConstruct c = match kind_of_term c with
-    Construct _ -> true | _ -> false
+let isConstruct c = match kind_of_term c with Construct _ -> true | _ -> false
 
 (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
 let destCase c = match kind_of_term c with
   | Case (ci,p,c,v) -> (ci,p,c,v)
   | _ -> anomaly "destCase"
 
+let isCase c =  match kind_of_term c with Case _ -> true | _ -> false
+
 let destFix c = match kind_of_term c with 
   | Fix fix -> fix
   | _ -> invalid_arg "destFix"
-	
+
+let isFix c =  match kind_of_term c with Fix _ -> true | _ -> false
+
 let destCoFix c = match kind_of_term c with 
   | CoFix cofix -> cofix
   | _ -> invalid_arg "destCoFix"
 
+let isCoFix c =  match kind_of_term c with CoFix _ -> true | _ -> false
+
 (******************************************************************)
 (* Cast management                                                *)
 (******************************************************************)
diff --git a/kernel/term.mli b/kernel/term.mli
index 6236dc39..3b5a2bc1 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: term.mli 10859 2008-04-27 16:46:15Z herbelin $ i*)
+(*i $Id: term.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -230,9 +230,13 @@ val isSort : constr -> bool
 val isCast : constr -> bool
 val isApp : constr -> bool
 val isLambda : constr -> bool
+val isLetIn : constr -> bool
 val isProd : constr -> bool
 val isConst : constr -> bool
 val isConstruct : constr -> bool
+val isFix : constr -> bool
+val isCoFix : constr -> bool
+val isCase : constr -> bool
 
 val is_Prop : constr -> bool
 val is_Set  : constr -> bool
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 0f649057..f50a0b83 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: term_typing.ml 10877 2008-04-30 21:58:41Z herbelin $ *)
+(* $Id: term_typing.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Util
 open Names
@@ -60,7 +60,7 @@ let safe_push_named (id,_,_ as d) env =
   let _ =
     try
       let _ = lookup_named id env in 
-      error ("identifier "^string_of_id id^" already defined")
+      error ("Identifier "^string_of_id id^" already defined.")
     with Not_found -> () in
   push_named d env
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 3791c3e1..11a5452c 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: univ.ml 11063 2008-06-06 16:03:45Z soubiran $ *)
+(* $Id: univ.ml 11301 2008-08-04 19:41:18Z herbelin $ *)
 
 (* Initial Caml version originates from CoC 4.8 [Dec 1988] *)
 (* Extension with algebraic universes by HH [Sep 2001] *)
@@ -550,6 +550,11 @@ let subst_large_constraint u u' v =
 let subst_large_constraints =
   List.fold_right (fun (u,u') -> subst_large_constraint u u')
 
+let no_upper_constraints u cst =
+  match u with
+  | Atom u -> Constraint.for_all (fun (u1,_,_) -> u1 <> u) cst
+  | Max _ -> anomaly "no_upper_constraints"
+
 (* Pretty-printing *)
 
 let num_universes g =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 0a1a8328..668e99a0 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: univ.mli 11063 2008-06-06 16:03:45Z soubiran $ i*)
+(*i $Id: univ.mli 11301 2008-08-04 19:41:18Z herbelin $ i*)
 
 (* Universes. *)
 
@@ -76,6 +76,8 @@ val subst_large_constraint : universe -> universe -> universe -> universe
 val subst_large_constraints : 
   (universe * universe) list -> universe -> universe
 
+val no_upper_constraints : universe -> constraints -> bool
+
 (*s Pretty-printing of universes. *)
 
 val pr_uni : universe -> Pp.std_ppcmds