Imported Upstream version 8.1+dfsgupstream/8.1+dfsg

24 files changed, 289 insertions, 207 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 70648b44..affcccb3 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -10,11 +10,11 @@
 
 #include <stdio.h>
 #include <stdlib.h> 
-#include "config.h"
-#include "misc.h"
-#include "mlvalues.h"
-#include "fail.h"
-#include "memory.h"
+#include <config.h>
+#include <misc.h>
+#include <mlvalues.h>
+#include <fail.h>
+#include <memory.h>
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
 
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
index 035d5b9b..d1dac80f 100644
--- a/kernel/byterun/coq_fix_code.h
+++ b/kernel/byterun/coq_fix_code.h
@@ -12,7 +12,7 @@
 #ifndef _COQ_FIX_CODE_
 #define _COQ_FIX_CODE_
 
-#include "mlvalues.h"
+#include <mlvalues.h>
 void * coq_stat_alloc (asize_t sz);
 
 #ifdef THREADED_CODE
diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
index 2f085326..ccccbe78 100644
--- a/kernel/byterun/coq_gc.h
+++ b/kernel/byterun/coq_gc.h
@@ -10,8 +10,8 @@
 
 #ifndef _COQ_CAML_GC_
 #define _COQ_CAML_GC_
-#include "mlvalues.h"
-#include "alloc.h"
+#include <mlvalues.h>
+#include <alloc.h>
 
 typedef void (*scanning_action) (value, value *);
 
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 0f91a7e3..8f9c10e6 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -44,11 +44,7 @@ sp is a local copy of the global variable extern_sp. */
 #  ifdef DEBUG
 #    define Next goto next_instr
 #  else
-#    ifdef __ia64__
-#      define Next goto *(void *)(coq_jumptbl_base + *((uint32 *) pc)++)
-#    else
-#      define Next goto *(void *)(coq_jumptbl_base + *pc++)
-#    endif
+#    define Next goto *(void *)(coq_jumptbl_base + *pc++)  
 #  endif
 #else 
 #  define Instruct(name) case name:
diff --git a/kernel/byterun/coq_interp.h b/kernel/byterun/coq_interp.h
index 76e68944..60865c32 100644
--- a/kernel/byterun/coq_interp.h
+++ b/kernel/byterun/coq_interp.h
@@ -19,5 +19,9 @@ value coq_push_vstack(value stk);
 
 value  coq_interprete_ml(value tcode, value a, value e, value ea);
 
+value coq_interprete
+    (code_t coq_pc, value coq_accu, value coq_env, long coq_extra_args);
+
 value coq_eval_tcode (value tcode, value e);
 
+
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index bfcb6812..91342108 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -14,6 +14,7 @@
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
 #include "coq_memory.h"
+#include "coq_interp.h"
 
 /* stack */
 
@@ -264,9 +265,3 @@ value coq_set_drawinstr(value unit)
   return Val_unit;
 }
 
-
-value coq_print_pointer(value p)
-{
-  printf("pointer = %X\n", p);
-  return Val_unit;
-}
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
index 0d866dc7..edd05948 100644
--- a/kernel/byterun/coq_memory.h
+++ b/kernel/byterun/coq_memory.h
@@ -11,11 +11,11 @@
 #ifndef _COQ_MEMORY_
 #define _COQ_MEMORY_
 
-#include "config.h"
-#include "fail.h"
-#include "misc.h"
-#include "memory.h"
-#include "mlvalues.h"
+#include <config.h>
+#include <fail.h>
+#include <misc.h>
+#include <memory.h>
+#include <mlvalues.h>
 
 
 #define Coq_stack_size (4096 * sizeof(value))
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
index 34b885e8..007f61b2 100644
--- a/kernel/byterun/coq_values.c
+++ b/kernel/byterun/coq_values.c
@@ -13,7 +13,7 @@
 #include "coq_instruct.h"
 #include "coq_memory.h"
 #include "coq_values.h"
-#include "memory.h"
+#include <memory.h>
 /* KIND OF VALUES */
 
 #define Setup_for_gc
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index a5176f3f..4c631fce 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -11,8 +11,8 @@
 #ifndef _COQ_VALUES_
 #define _COQ_VALUES_
 
-#include "alloc.h"
-#include "mlvalues.h"
+#include <alloc.h>
+#include <mlvalues.h>
 
 #define Default_tag 0
 #define Accu_tag 0
diff --git a/kernel/environ.ml b/kernel/environ.ml
index e73f5848..87a6e485 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: environ.ml 9201 2006-10-03 16:47:40Z notin $ *)
+(* $Id: environ.ml 9573 2007-01-31 20:18:18Z notin $ *)
 
 open Util
 open Names
@@ -241,9 +241,9 @@ let global_vars_set env constr =
   let rec filtrec acc c =
     let vl = vars_of_global env c in
     let acc = List.fold_right Idset.add vl acc in
-    fold_constr filtrec acc c
+      fold_constr filtrec acc c
   in 
-  filtrec Idset.empty constr
+    filtrec Idset.empty constr
 
 (* like [global_vars] but don't get through evars *)
 let global_vars_set_drop_evar env constr = 
@@ -339,18 +339,6 @@ type unsafe_type_judgment = {
 
 let compile_constant_body = Cbytegen.compile_constant_body  
 
-(*s Special functions for the refiner (logic.ml) *)
-
-let clear_hyps ids check (ctxt,vals) =
-  let ctxt,vals,rmv = 
-    List.fold_right2 (fun (id,_,_ as d) v (ctxt,vals,rmv) ->
-      if List.mem id ids then (ctxt,vals,id::rmv)
-      else begin
-	check rmv d;
-	(d::ctxt,v::vals,rmv)
-      end) ctxt vals ([],[],[])
-  in ((ctxt,vals),rmv)
-
 exception Hyp_not_found
 
 let rec apply_to_hyp (ctxt,vals) id f =
@@ -393,3 +381,16 @@ let insert_after_hyp (ctxt,vals) id d check =
     | [],[] -> raise Hyp_not_found
     | _, _ -> assert false
   in aux ctxt vals
+
+(* To be used in Logic.clear_hyps *)
+let remove_hyps ids check (ctxt, vals) =
+  let ctxt,vals,rmv = 
+    List.fold_right2 (fun (id,_,_ as d) v (ctxt,vals,rmv) ->
+      if List.mem id ids then 
+	(ctxt,vals,id::rmv)
+      else 	  
+	let nd = check d in
+	  (nd::ctxt,v::vals,rmv))
+		     ctxt vals ([],[],[])
+  in ((ctxt,vals),rmv)
+
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 3728eea3..478357d7 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 9310 2006-10-28 19:35:09Z herbelin $ i*)
+(*i $Id: environ.mli 9573 2007-01-31 20:18:18Z notin $ i*)
 
 (*i*)
 open Names
@@ -195,11 +195,6 @@ val compile_constant_body :
     env -> constr_substituted option -> bool -> bool -> Cemitcodes.body_code
                                  (* opaque *) (* boxed *)
 
-(*s Functions for proofs/logic.ml *)
-val clear_hyps : 
-    variable list -> (variable list -> named_declaration -> unit) -> 
-      named_context_val -> named_context_val * variable list
-
 exception Hyp_not_found
 
 (* [apply_to_hyp sign id f] split [sign] into [tail::(id,_,_)::head] and
@@ -221,3 +216,6 @@ val apply_to_hyp_and_dependent_on : named_context_val -> variable ->
 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) -> named_context_val -> named_context_val * identifier list
+
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 1520e009..4fe90ffd 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indtypes.ml 9310 2006-10-28 19:35:09Z herbelin $ *)
+(* $Id: indtypes.ml 9633 2007-02-09 18:40:26Z herbelin $ *)
 
 open Util
 open Names
@@ -97,19 +97,7 @@ let mind_check_arities env mie =
 
 (* Typing the arities and constructor types *)
 
-let is_info_arity env c =
-  match dest_arity env c with
-    | (_,Prop Null) -> false 
-    | (_,Prop Pos)  -> true 
-    | (_,Type _)    -> true
-
-let is_info_type env t =
-  let s = t.utj_type in
-  if s = mk_Set then true
-  else if s = mk_Prop then false
-  else
-    try is_info_arity env t.utj_val
-    with UserError _ -> true
+let is_logic_type t = (t.utj_type = mk_Prop)
 
 (* [infos] is a sequence of pair [islogic,issmall] for each type in
    the product of a constructor or arity *)
@@ -132,7 +120,7 @@ let rec infos_and_sort env t =
     | Prod (name,c1,c2) ->
         let (varj,_) = infer_type env c1 in
 	let env1 = Environ.push_rel (name,None,varj.utj_val) env in
-	let logic = not (is_info_type env varj) in
+	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
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index b7265e8c..2f17d659 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: inductive.ml 9323 2006-10-30 23:05:29Z herbelin $ *)
+(* $Id: inductive.ml 9421 2006-12-08 16:00:53Z barras $ *)
 
 open Util
 open Names
@@ -519,6 +519,35 @@ let lookup_subterms env ind =
 
 (*********************************)
 
+(* Propagation of size information through Cases: if the matched
+   object is a recursive subterm then compute the information
+   associated to its own subterms.
+   Rq: if branch is not eta-long, then the recursive information
+   is not propagated to the missing abstractions *)
+let case_branches_specif renv c_spec ind lbr = 
+  let rec push_branch_args renv lrec c = 
+    match lrec with
+        ra::lr ->
+          let c' = whd_betadeltaiota renv.env c in
+          (match kind_of_term c' with
+              Lambda(x,a,b) ->
+                let renv' = push_var renv (x,a,ra) in
+                push_branch_args renv' lr b
+            | _ -> (* branch not in eta-long form: cannot perform rec. calls *)
+                (renv,c'))
+      | [] -> (renv, c) in
+  match c_spec with
+      Subterm (_,t) ->
+        let sub_spec = Array.map (List.map spec_of_tree) (dest_subterms t) in
+        assert (Array.length sub_spec = Array.length lbr);
+        array_map2 (push_branch_args renv) sub_spec lbr
+    | Dead_code -> 
+        let t = dest_subterms (lookup_subterms renv.env ind) in
+        let sub_spec = Array.map (List.map (fun _ -> Dead_code)) t in
+        assert (Array.length sub_spec = Array.length lbr);
+        array_map2 (push_branch_args renv) sub_spec lbr
+    | Not_subterm -> Array.map (fun c -> (renv,c)) lbr
+
 (* [subterm_specif renv t] computes the recursive structure of [t] and
    compare its size with the size of the initial recursive argument of
    the fixpoint we are checking. [renv] collects such information
@@ -534,7 +563,8 @@ let rec subterm_specif renv t =
     | Case (ci,_,c,lbr) ->
         if Array.length lbr = 0 then Dead_code
         else
-          let lbr_spec = case_branches_specif renv c ci.ci_ind lbr in
+          let c_spec = subterm_specif renv c in
+          let lbr_spec = case_branches_specif renv c_spec ci.ci_ind lbr in
           let stl  =
             Array.map (fun (renv',br') -> subterm_specif renv' br')
               lbr_spec in
@@ -586,35 +616,6 @@ let rec subterm_specif renv t =
     (* Other terms are not subterms *)
     | _ -> Not_subterm
 
-(* Propagation of size information through Cases: if the matched
-   object is a recursive subterm then compute the information
-   associated to its own subterms.
-   Rq: if branch is not eta-long, then the recursive information
-   is not propagated to the missing abstractions *)
-and case_branches_specif renv c ind lbr = 
-  let c_spec = subterm_specif renv c in
-  let rec push_branch_args renv lrec c = 
-    match lrec with
-        ra::lr ->
-          let c' = whd_betadeltaiota renv.env c in
-          (match kind_of_term c' with
-              Lambda(x,a,b) ->
-                let renv' = push_var renv (x,a,ra) in
-                push_branch_args renv' lr b
-            | _ -> (* branch not in eta-long form: cannot perform rec. calls *)
-                (renv,c'))
-      | [] -> (renv, c) in
-  match c_spec with
-      Subterm (_,t) ->
-        let sub_spec = Array.map (List.map spec_of_tree) (dest_subterms t) in
-        assert (Array.length sub_spec = Array.length lbr);
-        array_map2 (push_branch_args renv) sub_spec lbr
-    | Dead_code -> 
-        let t = dest_subterms (lookup_subterms renv.env ind) in
-        let sub_spec = Array.map (List.map (fun _ -> Dead_code)) t in
-        assert (Array.length sub_spec = Array.length lbr);
-        array_map2 (push_branch_args renv) sub_spec lbr
-    | Not_subterm -> Array.map (fun c -> (renv,c)) lbr
 
 (* Check term c can be applied to one of the mutual fixpoints. *)
 let check_is_subterm renv c = 
@@ -652,10 +653,10 @@ let check_one_fix renv recpos def =
     (* if [t] does not make recursive calls, it is guarded: *)
     if noccur_with_meta renv.rel_min nfi t then ()
     else
-      (* Rq: why not try and expand some definitions ? *)
-      let f,l = decompose_app (whd_betaiotazeta renv.env t) in
+      let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in
       match kind_of_term f with
         | Rel p -> 
+            List.iter (check_rec_call renv) l;
             (* Test if [p] is a fixpoint (recursive call) *) 
 	    if renv.rel_min <= p & p < renv.rel_min+nfi then
               (* the position of the invoked fixpoint: *) 
@@ -668,87 +669,80 @@ let check_one_fix renv recpos def =
 		    (la,(z::lrest)) -> 
                       (* Check the decreasing arg is smaller *)
 	              if not (check_is_subterm renv z) then
-                        error_illegal_rec_call renv glob z;
-                      List.iter (check_rec_call renv) (la@lrest)
+                        error_illegal_rec_call renv glob z
 	          | _ -> assert false)
-            (* otherwise check the arguments are guarded: *)
-	    else List.iter (check_rec_call renv) l        
-
-      | Case (ci,p,c_0,lrest) ->
-          List.iter (check_rec_call renv) (c_0::p::l);
-          (* compute the recarg information for the arguments of
-             each branch *)
-          let lbr = case_branches_specif renv c_0 ci.ci_ind lrest in
-          Array.iter (fun (renv',br') -> check_rec_call renv' br') lbr
-
-  (* Enables to traverse Fixpoint definitions in a more intelligent
-     way, ie, the rule :
-
-     if - g = Fix g/1 := [y1:T1]...[yp:Tp]e &
-        - f is guarded with respect to the set of pattern variables S 
-          in a1 ... am        &
-        - f is guarded with respect to the set of pattern variables S 
-          in T1 ... Tp        &
-        - ap is a sub-term of the formal argument of f &
-        - f is guarded with respect to the set of pattern variables S+{yp}
-          in e
-     then f is guarded with respect to S in (g a1 ... am).
-
-     Eduardo 7/9/98 *)
-
-      | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
-          List.iter (check_rec_call renv) l;
-          Array.iter (check_rec_call renv) typarray;
-          let decrArg = recindxs.(i) in
-          let renv' = push_fix_renv renv recdef in 
-          if (List.length l < (decrArg+1)) then
+
+        | Case (ci,p,c_0,lrest) ->
+            List.iter (check_rec_call renv) (c_0::p::l);
+            (* compute the recarg information for the arguments of
+               each branch *)
+            let c_spec = subterm_specif renv c_0 in
+            let lbr = case_branches_specif renv c_spec ci.ci_ind lrest in
+            Array.iter (fun (renv',br') -> check_rec_call renv' br') lbr
+
+        (* Enables to traverse Fixpoint definitions in a more intelligent
+           way, ie, the rule :
+           if - g = Fix g/p := [y1:T1]...[yp:Tp]e &
+              - f is guarded with respect to the set of pattern variables S 
+                in a1 ... am        &
+              - f is guarded with respect to the set of pattern variables S 
+                in T1 ... Tp        &
+              - ap is a sub-term of the formal argument of f &
+              - f is guarded with respect to the set of pattern variables
+                S+{yp} in e
+           then f is guarded with respect to S in (g a1 ... am).
+           Eduardo 7/9/98 *)
+
+        | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
+            List.iter (check_rec_call renv) l;
+            Array.iter (check_rec_call renv) typarray;
+            let decrArg = recindxs.(i) in
+            let renv' = push_fix_renv renv recdef in 
+            if (List.length l < (decrArg+1)) then
+	      Array.iter (check_rec_call renv') bodies
+            else 
+              Array.iteri
+                (fun j body ->
+                  if i=j then
+                    let theDecrArg  = List.nth l decrArg in
+	            let arg_spec = subterm_specif renv theDecrArg in
+	            check_nested_fix_body renv' (decrArg+1) arg_spec body
+                  else check_rec_call renv' body)
+                bodies
+
+        | Const kn -> 
+            if evaluable_constant kn renv.env then 
+              try List.iter (check_rec_call renv) l
+              with (FixGuardError _ ) ->
+	        check_rec_call renv(applist(constant_value renv.env kn, l))
+	    else List.iter (check_rec_call renv) l
+
+        (* The cases below simply check recursively the condition on the
+           subterms *)
+        | Cast (a,_, b) -> 
+            List.iter (check_rec_call renv) (a::b::l)
+
+        | Lambda (x,a,b) ->
+            List.iter (check_rec_call renv) (a::l);
+            check_rec_call (push_var_renv renv (x,a)) b
+
+        | Prod (x,a,b) -> 
+            List.iter (check_rec_call renv) (a::l);
+            check_rec_call (push_var_renv renv (x,a)) b
+
+        | CoFix (i,(_,typarray,bodies as recdef)) ->
+            List.iter (check_rec_call renv) l;
+	    Array.iter (check_rec_call renv) typarray;
+	    let renv' = push_fix_renv renv recdef in
 	    Array.iter (check_rec_call renv') bodies
-          else 
-            Array.iteri
-              (fun j body ->
-                if i=j then
-                  let theDecrArg  = List.nth l decrArg in
-	          let arg_spec = subterm_specif renv theDecrArg in
-	          check_nested_fix_body renv' (decrArg+1) arg_spec body
-                else check_rec_call renv' body)
-              bodies
-
-      | Const kn -> 
-          if evaluable_constant kn renv.env then 
-            try List.iter (check_rec_call renv) l
-            with (FixGuardError _ ) ->
-	      check_rec_call renv(applist(constant_value renv.env kn, l))
-	  else List.iter (check_rec_call renv) l
-
-      (* The cases below simply check recursively the condition on the
-         subterms *)
-      | Cast (a,_, b) -> 
-          List.iter (check_rec_call renv) (a::b::l)
-
-      | Lambda (x,a,b) ->
-          check_rec_call (push_var_renv renv (x,a)) b;
-          List.iter (check_rec_call renv) (a::l)
-
-      | Prod (x,a,b) -> 
-          check_rec_call (push_var_renv renv (x,a)) b;
-          List.iter (check_rec_call renv) (a::l)
-
-      | CoFix (i,(_,typarray,bodies as recdef)) ->
-	  Array.iter (check_rec_call renv) typarray;
-          List.iter (check_rec_call renv) l;
-	  let renv' = push_fix_renv renv recdef in
-	  Array.iter (check_rec_call renv') bodies
-
-      | Evar _ -> 
-          List.iter (check_rec_call renv) l
-
-      (* l is not checked because it is considered as the meta's context *)
-      | Meta _ -> ()
-
-      | (Ind _ | Construct _ | Var _ | Sort _) ->
-          List.iter (check_rec_call renv) l
-
-      | (App _ | LetIn _) -> assert false (* beta zeta reduction *)
+
+        | (Ind _ | Construct _ | Var _ | Sort _) ->
+            List.iter (check_rec_call renv) l
+
+        (* l is not checked because it is considered as the meta's context *)
+        | (Evar _ | Meta _) -> ()
+
+        | (App _ | LetIn _) -> assert false (* beta zeta reduction *)
 
   and check_nested_fix_body renv decr recArgsDecrArg body =
     if decr = 0 then
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index b9d0f984..58343dab 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 9314 2006-10-29 20:11:08Z herbelin $ i*)
+(*i $Id: inductive.mli 9421 2006-12-08 16:00:53Z barras $ i*)
 
 (*i*)
 open Names
@@ -106,5 +106,5 @@ type guard_env =
   }
 
 val subterm_specif : guard_env -> constr -> subterm_spec
-val case_branches_specif : guard_env -> constr -> inductive ->
+val case_branches_specif : guard_env -> subterm_spec -> inductive ->
   constr array -> (guard_env * constr) array
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 663434ec..352a1e46 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: mod_typing.ml 9310 2006-10-28 19:35:09Z herbelin $ i*)
+(*i $Id: mod_typing.ml 9558 2007-01-30 14:58:42Z soubiran $ i*)
 
 open Util
 open Names
@@ -123,7 +123,7 @@ and merge_with env mtb with_decl =
 		let _ = subst_modtype (map_msid msid (MPself msid)) mtb in
 		  ()
 	      with
-		  Failure _ -> error_circular_with_module id
+		  Circularity _ -> error_circular_with_module id
 	    end;
 	    let cst =
               try check_subtypes env' mtb old.msb_modtype
@@ -247,10 +247,8 @@ and translate_module env is_definition me =
 	    | None -> mtb1, None, Constraint.empty
 	    | Some mte -> 
 		let mtb2 = translate_modtype env mte in
-                let cst =
-                  try check_subtypes env mtb1 mtb2
-                  with Failure _ -> error "not subtype" in
-		mtb2, Some mtb2, cst
+                let cst = check_subtypes env mtb1 mtb2 in
+		    mtb2, Some mtb2, cst
 	in
 	  { mod_type = mtb;
 	    mod_user_type = mod_user_type;
@@ -274,10 +272,7 @@ and translate_mexpr env mexpr = match mexpr with
       let ftb = scrape_modtype env ftb in
       let farg_id, farg_b, fbody_b = destr_functor ftb in
       let meb,mtb = translate_mexpr env mexpr in
-      let cst =
-        try check_subtypes env mtb farg_b
-        with Failure _ ->
-          error "" in
+      let cst = check_subtypes env mtb farg_b in
       let mp = 
 	try
 	  path_of_mexpr mexpr 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 5cc2a84d..8bab3c9d 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 9138 2006-09-14 15:20:45Z jforest $ i*)
+(*i $Id: modops.ml 9558 2007-01-30 14:58:42Z soubiran $ i*)
 
 (*i*)
 open Util
@@ -20,6 +20,8 @@ open Entries
 open Mod_subst
 (*i*)
 
+exception Circularity of string
+
 let error_existing_label l = 
   error ("The label "^string_of_label l^" is already declared")
 
@@ -83,6 +85,13 @@ let error_local_context lo =
 let error_circular_with_module l =
   error ("The construction \"with Module "^(string_of_id l)^":=...\" is about to create\na circular module type. Their resolution is not implemented yet.\nIf you really need that feature, please report.")
 
+let error_circularity_in_subtyping l l1 l2 =
+  error ("An occurrence of "^l^" creates a circularity\n during the subtyping verification between "^l1^" and "^l2^".")
+
+let error_no_such_label_sub l l1 l2 =
+  error (l1^" is not a subtype of "^l2^".\nThe field "^(string_of_label l)^" is missing (or invisible) in "^l1^".")
+
+
 let rec scrape_modtype env = function
   | MTBident kn -> scrape_modtype env (lookup_modtype kn env)
   | mtb -> mtb
@@ -134,12 +143,12 @@ let rec subst_modtype sub = function
        M to M' I must substitute M' for X in "Module N := X". *)
   | MTBident ln -> MTBident (subst_kn sub ln)
   | MTBfunsig (arg_id, arg_b, body_b) ->
-      if occur_mbid arg_id sub then failwith "capture";
+      if occur_mbid arg_id sub then raise (Circularity (string_of_mbid arg_id));
       MTBfunsig (arg_id, 
 		 subst_modtype sub arg_b, 
 		 subst_modtype sub body_b)
   | MTBsig (sid1, msb) -> 
-      if occur_msid sid1 sub then failwith "capture";
+      if occur_msid sid1 sub then raise (Circularity (string_of_msid sid1));
       MTBsig (sid1, subst_signature sub msb)
 
 and subst_signature sub sign = 
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 2aca6511..55f81079 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modops.mli 8721 2006-04-15 15:30:04Z herbelin $ i*)
+(*i $Id: modops.mli 9558 2007-01-30 14:58:42Z soubiran $ i*)
 
 (*i*)
 open Util
@@ -20,6 +20,8 @@ open Mod_subst
 
 (* Various operations on modules and module types *)
 
+exception Circularity of string
+
 (* recursively unfold MTBdent module types *)
 val scrape_modtype : env -> module_type_body -> module_type_body
 
@@ -98,5 +100,9 @@ val error_local_context : label option -> 'a
 
 val error_circular_with_module : identifier -> 'a
 
+val error_circularity_in_subtyping : string->string->string-> 'a
+
+val error_no_such_label_sub : label->string->string->'a
+
 val resolver_of_environment :
  mod_bound_id -> module_type_body -> module_path -> env -> resolver
diff --git a/kernel/names.ml b/kernel/names.ml
index ae5afebd..383d7879 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: names.ml 8852 2006-05-23 17:52:43Z notin $ *)
+(* $Id: names.ml 9558 2007-01-30 14:58:42Z soubiran $ *)
 
 open Pp
 open Util
@@ -73,8 +73,10 @@ let string_of_dirpath = function
 let u_number = ref 0 
 type uniq_ident = int * string * dir_path
 let make_uid dir s = incr u_number;(!u_number,String.copy s,dir)
-let string_of_uid (i,s,p) = 
+let debug_string_of_uid (i,s,p) = 
   "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">"
+let string_of_uid (i,s,p) = 
+  string_of_dirpath p ^"."^s
 
 module Umap = Map.Make(struct 
 			 type t = uniq_ident 
@@ -84,12 +86,14 @@ module Umap = Map.Make(struct
 
 type mod_self_id = uniq_ident
 let make_msid = make_uid
-let debug_string_of_msid = string_of_uid
+let debug_string_of_msid = debug_string_of_uid
+let string_of_msid = string_of_uid
 let id_of_msid (_,s,_) = s
 
 type mod_bound_id = uniq_ident
 let make_mbid = make_uid
-let debug_string_of_mbid = string_of_uid
+let debug_string_of_mbid = debug_string_of_uid
+let string_of_mbid = string_of_uid
 let id_of_mbid (_,s,_) = s
 
 type label = string
diff --git a/kernel/names.mli b/kernel/names.mli
index 82a638c0..c9fef60a 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: names.mli 8852 2006-05-23 17:52:43Z notin $ i*)
+(*i $Id: names.mli 9558 2007-01-30 14:58:42Z soubiran $ i*)
 
 (*s Identifiers *)
 
@@ -50,6 +50,7 @@ type mod_self_id
 val make_msid : dir_path -> string -> mod_self_id
 val id_of_msid : mod_self_id -> identifier
 val debug_string_of_msid : mod_self_id -> string
+val string_of_msid : mod_self_id -> string
 
 (*s Unique names for bound modules *)
 type mod_bound_id
@@ -57,12 +58,14 @@ type mod_bound_id
 val make_mbid : dir_path -> string -> mod_bound_id
 val id_of_mbid : mod_bound_id -> identifier
 val debug_string_of_mbid : mod_bound_id -> string
+val string_of_mbid : mod_bound_id -> string
 
 (*s Names of structure elements *)
 type label
 val mk_label : string -> label
 val string_of_label : label -> string
 
+
 val label_of_id : identifier -> label
 val id_of_label : label -> identifier
 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 9a8de5a9..d1a10651 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: subtyping.ml 9310 2006-10-28 19:35:09Z herbelin $ i*)
+(*i $Id: subtyping.ml 9558 2007-01-30 14:58:42Z soubiran $ i*)
 
 (*i*)
 open Util
@@ -81,6 +81,41 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
       | IndType ((_,0), mib) -> mib
       | _ -> error ()
   in
+  let check_inductive_type cst env t1 t2 =
+
+    (* Due to sort-polymorphism in inductive types, the conclusions of
+       t1 and t2, if in Type, are generated as the least upper bounds
+       of the types of the constructors. 
+
+       By monotonicity of the infered l.u.b.  wrt subtyping (i.e.  if X:U
+       |- T(X):s and |- M:U' and U'<=U then infer_type(T(M))<=s), each
+       universe in the conclusion of t1 has an bounding universe in
+       the conclusion of t2, so that we don't need to check the
+       subtyping of the conclusions of t1 and t2.
+
+       Even if we'd like to recheck it, the inference of constraints
+       is not designed to deal with algebraic constraints of the form
+       max-univ(u1..un) <= max-univ(u'1..u'n), so that it is not easy
+       to recheck it (in short, we would need the actual graph of
+       constraints as input while type checking is currently designed
+       to output a set of constraints instead) *)
+
+    (* So we cheat and replace the subtyping problem on algebraic
+       constraints of the form max-univ(u1..un) <= max-univ(u'1..u'n)
+       (that we know are necessary true) by trivial constraints that
+       the constraint generator knows how to deal with *)
+
+    let (ctx1,s1) = dest_arity env t1 in
+    let (ctx2,s2) = dest_arity env t2 in
+    let s1,s2 =
+      match s1, s2 with
+      | Type _, Type _ -> (* shortcut here *) mk_Prop, mk_Prop
+      | (Prop _, Type _) | (Type _,Prop _) -> error ()
+      | _ -> (s1, s2) in
+    check_conv cst conv_leq env 
+      (Sign.mkArity (ctx1,s1)) (Sign.mkArity (ctx2,s2))
+  in
+
   let check_packet cst p1 p2 =
     let check f = if f p1 <> f p2 then error () in
       check (fun p -> p.mind_consnames);
@@ -96,7 +131,7 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
       (* nparams done *)
       (* params_ctxt done because part of the inductive types *)
       (* Don't check the sort of the type if polymorphic *)
-      let cst = check_conv cst conv env (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2))
+      let cst = check_inductive_type cst env (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2))
       in
 	cst
   in
@@ -160,13 +195,60 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
 let check_constant cst env msid1 l info1 cb2 spec2 = 
   let error () = error_not_match l spec2 in
   let check_conv cst f = check_conv_error error cst f in
+  let check_type cst env t1 t2 = 
+
+    (* If the type of a constant is generated, it may mention
+       non-variable algebraic universes that the general conversion
+       algorithm is not ready to handle. Anyway, generated types of
+       constants are functions of the body of the constant. If the
+       bodies are the same in environments that are subtypes one of
+       the other, the types are subtypes too (i.e. if Gamma <= Gamma',
+       Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T').
+       Hence they don't have to be checked again *)
+
+    let t1,t2 = 
+      if Sign.isArity t2 then
+        let (ctx2,s2) = Sign.destArity t2 in
+        match s2 with
+        | Type v when not (is_univ_variable v) ->
+          (* The type in the interface is inferred and is made of algebraic
+             universes *)
+          begin try
+            let (ctx1,s1) = dest_arity env t1 in
+            match s1 with
+            | Type u when not (is_univ_variable u) ->
+              (* Both types are inferred, no need to recheck them. We
+                 cheat and collapse the types to Prop *)
+                Sign.mkArity (ctx1,mk_Prop), Sign.mkArity (ctx2,mk_Prop)
+            | Prop _ ->
+              (* The type in the interface is inferred, it may be the case
+                 that the type in the implementation is smaller because
+                 the body is more reduced. We safely collapse the upper
+                 type to Prop *)
+                Sign.mkArity (ctx1,mk_Prop), Sign.mkArity (ctx2,mk_Prop)
+            | Type _ ->
+              (* The type in the interface is inferred and the type in the
+                 implementation is not inferred or is inferred but from a
+                 more reduced body so that it is just a variable. Since
+                 constraints of the form "univ <= max(...)" are not
+                 expressible in the system of algebraic universes: we fail
+                 (the user has to use an explicit type in the interface *)
+                error ()
+          with UserError _ (* "not an arity" *) ->
+            error () end
+        | _ -> t1,t2
+      else
+        (t1,t2) in
+    check_conv cst conv_leq env t1 t2
+  in
+
   match info1 with
    | Constant cb1 ->
       assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
       (*Start by checking types*)
       let typ1 = Typeops.type_of_constant_type env cb1.const_type in
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
-      let cst = check_conv cst conv_leq env typ1 typ2 in
+      let cst = check_type cst env typ1 typ2 in
       let con = make_con (MPself msid1) empty_dirpath l in
       let cst =
        match cb2.const_body with
@@ -222,14 +304,18 @@ let rec check_modules cst env msid1 l msb1 msb2 =
 and check_signatures cst env (msid1,sig1) (msid2,sig2') = 
   let mp1 = MPself msid1 in
   let env = add_signature mp1 sig1 env in 
-  let sig2 = subst_signature_msid msid2 mp1 sig2' in
+  let sig2 = try
+    subst_signature_msid msid2 mp1 sig2' 
+    with
+    | Circularity l -> 
+	error_circularity_in_subtyping l (string_of_msid msid1) (string_of_msid msid2) in
   let map1 = make_label_map mp1 sig1 in
   let check_one_body cst (l,spec2) = 
     let info1 = 
       try 
 	Labmap.find l map1 
       with 
-	  Not_found -> error_no_such_label l 
+	  Not_found -> error_no_such_label_sub l (string_of_msid msid1) (string_of_msid msid2)
     in
       match spec2 with
 	| SPBconst cb2 ->
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 64a2f650..1e73725f 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: typeops.mli 9314 2006-10-29 20:11:08Z herbelin $ i*)
+(*i $Id: typeops.mli 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 (*i*)
 open Names
@@ -106,3 +106,4 @@ val type_of_constant_knowing_parameters :
 
 (* Make a type polymorphic if an arity *)
 val make_polymorphic_if_arity : env -> types -> constant_type
+
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 775e505f..df06e9af 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: univ.ml 9314 2006-10-29 20:11:08Z herbelin $ *)
+(* $Id: univ.ml 9507 2007-01-20 08:09:54Z herbelin $ *)
 
 (* Initial Caml version originates from CoC 4.8 [Dec 1988] *)
 (* Extension with algebraic universes by HH [Sep 2001] *)
@@ -134,6 +134,10 @@ let is_base_univ = function
   | Max ([Base],[]) -> warning "Non canonical Set"; true
   | u -> false
 
+let is_univ_variable = function
+  | Atom a when a<>Base -> true
+  | _ -> false
+
 (* When typing [Prop] and [Set], there is no constraint on the level,
    hence the definition of [prop_univ], the type of [Prop] *)
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index f3af0861..5f562a1d 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 8845 2006-05-23 07:41:58Z herbelin $ i*)
+(*i $Id: univ.mli 9507 2007-01-20 08:09:54Z herbelin $ i*)
 
 (* Universes. *)
 
@@ -18,6 +18,7 @@ val neutral_univ : universe
 val make_univ : Names.dir_path * int -> universe
 
 val is_base_univ : universe -> bool
+val is_univ_variable : universe -> bool
 
 (* The type of a universe *)
 val super : universe -> universe
diff --git a/kernel/vm.ml b/kernel/vm.ml
index de9bd753..c1d3ca56 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -469,8 +469,6 @@ let check_cofix vcf1 vcf2 =
   (current_cofix vcf1 = current_cofix vcf2) &&
   (Obj.size (last (Obj.repr vcf1)) = Obj.size (last (Obj.repr vcf2)))
 
-external print_point : Obj.t -> unit = "coq_print_pointer"
-
 let reduce_cofix k vcf =
   let fc_typ = ((Obj.obj (last (Obj.repr vcf))) : tcode array) in
   let ndef = Array.length fc_typ in
@@ -478,7 +476,6 @@ let reduce_cofix k vcf =
     Array.map (fun c -> interprete c crasy_val (Obj.magic vcf) 0) fc_typ in
   (* Construction de l'environnement des corps des cofix *)
 
-  let max = k + ndef - 1 in 
   let e = Obj.dup (Obj.repr vcf) in 
   for i = 0 to ndef - 1 do
     Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i)))