suppression champs inutiles dans constantes et inductifs; verification definitions inductives

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

16 files changed, 254 insertions, 476 deletions

diff --git a/kernel/constant.ml b/kernel/constant.ml
index 766fbb735..9699d68a7 100644
--- a/kernel/constant.ml
+++ b/kernel/constant.ml
@@ -25,9 +25,7 @@ type constant_body = {
   const_body : recipe ref option;
   const_type : typed_type;
   const_hyps : typed_type signature;
-  mutable const_opaque : bool;
-  mutable const_eval : ((int * constr) list * int * bool) option option;
-}
+  mutable const_opaque : bool }
 
 let is_defined cb = 
   match cb.const_body with Some _ -> true | _ -> false
diff --git a/kernel/constant.mli b/kernel/constant.mli
index d33dc5a85..7b6589ca5 100644
--- a/kernel/constant.mli
+++ b/kernel/constant.mli
@@ -20,9 +20,7 @@ type constant_body = {
   const_body : recipe ref option;
   const_type : typed_type;
   const_hyps : typed_type signature;
-  mutable const_opaque : bool;
-  mutable const_eval : ((int * constr) list * int * bool) option option;
-}
+  mutable const_opaque : bool }
 
 val is_defined : constant_body -> bool
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 2b00e90d2..5cd8cc801 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -220,4 +220,6 @@ type unsafe_judgment = {
   uj_type : constr;
   uj_kind : constr }
 
-
+let cast_of_judgment = function
+  | { uj_val = DOP2 (Cast,_,_) as c } -> c
+  | { uj_val = c; uj_type = ty } -> mkCast c ty
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 4c1e23d03..34d889897 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -55,3 +55,4 @@ type unsafe_judgment = {
   uj_type : constr;
   uj_kind : constr }
 
+val cast_of_judgment : unsafe_judgment -> constr
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
new file mode 100644
index 000000000..82da97329
--- /dev/null
+++ b/kernel/indtypes.ml
@@ -0,0 +1,13 @@
+
+(* $Id$ *)
+
+open Inductive
+open Environ
+open Reduction
+
+let mind_check_arities env mie =
+  let check_arity id c =
+    if not (is_arity env c) then raise (InductiveError (NotAnArity id))
+  in
+  List.iter (fun (id,ar,_,_) -> check_arity id ar) mie.mind_entry_inds
+
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
new file mode 100644
index 000000000..20a0adfc1
--- /dev/null
+++ b/kernel/indtypes.mli
@@ -0,0 +1,10 @@
+
+(* $Id$ *)
+
+open Inductive
+open Environ
+
+(* [mind_check_arities] checks that the types declared for all the
+   inductive types are some arities. *)
+
+val mind_check_arities : 'a unsafe_env -> mutual_inductive_entry -> unit
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index cb4b3f655..5617358a1 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1,7 +1,9 @@
 
 (* $Id$ *)
 
+open Util
 open Names
+open Generic
 open Term
 open Sign
 
@@ -15,11 +17,8 @@ type mutual_inductive_packet = {
   mind_consnames : identifier array;
   mind_typename : identifier;
   mind_lc : constr;
-  mind_stamp : name;
   mind_arity : typed_type;
-  mind_lamexp : constr option;
-  mind_kd : sorts list;
-  mind_kn : sorts list;
+  mind_kelim : sorts list;
   mind_listrec : (recarg list) array;
   mind_finite : bool }
 
@@ -31,10 +30,6 @@ type mutual_inductive_body = {
   mind_singl : constr option;
   mind_nparams : int }
 
-type mutual_inductive_entry = {
-  mind_entry_params : (identifier * constr) list;
-  mind_entry_inds : (identifier * constr * (identifier * constr) list) list }
-
 let mind_type_finite mib i = mib.mind_packets.(i).mind_finite
 
 type mind_specif = {
@@ -47,9 +42,94 @@ type mind_specif = {
 let mis_ntypes mis = mis.mis_mib.mind_ntypes
 let mis_nconstr mis = Array.length (mis.mis_mip.mind_consnames)
 let mis_nparams mis = mis.mis_mib.mind_nparams
-let mis_kd mis = mis.mis_mip.mind_kd
-let mis_kn mis = mis.mis_mip.mind_kn
+let mis_kelim mis = mis.mis_mip.mind_kelim
 let mis_recargs mis =
   Array.map (fun mip -> mip.mind_listrec) mis.mis_mib.mind_packets
 
 let mind_nth_type_packet mib n = mib.mind_packets.(n)
+
+(*s Declaration. *)
+
+type mutual_inductive_entry = {
+  mind_entry_nparams : int;
+  mind_entry_finite : bool;
+  mind_entry_inds : (identifier * constr * identifier list * constr) list }
+
+type inductive_error =
+  | NonPos of int   
+  | NotEnoughArgs of int
+  | NotConstructor  
+  | NonPar of int * int
+  | SameNamesTypes of identifier
+  | SameNamesConstructors of identifier * identifier
+  | NotAnArity of identifier
+  | BadEntry
+
+exception InductiveError of inductive_error
+
+(* [check_constructors_names id s cl] checks that all the constructors names
+   appearing in [l] are not present in the set [s], and returns the new set
+   of names. The name [id] is the name of the current inductive type, used
+   when reporting the error. *)
+
+let check_constructors_names id =
+  let rec check idset = function
+    | [] -> idset
+    | c::cl -> 
+	if Idset.mem c idset then 
+	  raise (InductiveError (SameNamesConstructors (id,c)))
+	else
+	  check (Idset.add c idset) cl
+  in
+  check
+
+(* [mind_check_names mie] checks the names of an inductive types declaration,
+   and raises the corresponding exceptions when two types or two constructors
+   have the same name. *)
+
+let mind_check_names mie =
+  let rec check indset cstset = function
+    | [] -> ()
+    | (id,_,cl,_)::inds -> 
+	if Idset.mem id indset then
+	  raise (InductiveError (SameNamesTypes id))
+	else
+	  let cstset' = check_constructors_names id cstset cl in
+	  check (Idset.add id indset) cstset' inds
+  in
+  check Idset.empty Idset.empty mie.mind_entry_inds
+
+(* [mind_extract_params mie] extracts the params from an inductive types
+   declaration, and checks that they are all present (and all the same)
+   for all the given types. *)
+
+let mind_extract_params = decompose_prod_n
+  
+let extract nparams c =
+  try mind_extract_params nparams c 
+  with UserError _ -> raise (InductiveError (NotEnoughArgs nparams))
+
+let check_params nparams params c = 
+  if not (fst (extract nparams c) = params) then 
+    raise (InductiveError BadEntry)
+
+let mind_extract_and_check_params mie =
+  let nparams = mie.mind_entry_nparams in
+  match mie.mind_entry_inds with
+    | [] -> anomaly "empty inductive types declaration"
+    | (_,ar,_,_)::l -> 
+	let (params,_) = extract nparams ar in
+	List.iter (fun (_,c,_,_) -> check_params nparams params c) l;
+	params
+
+let mind_check_lc params mie =
+  let ntypes = List.length mie.mind_entry_inds in
+  let nparams = List.length params in
+  let check_lc (_,_,_,lc) =
+    let (lna,c) = decomp_all_DLAMV_name lc in
+    Array.iter (check_params nparams params) c;
+    if not (List.length lna = ntypes) then
+      raise (InductiveError BadEntry)
+  in
+  List.iter check_lc mie.mind_entry_inds
+
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index e57c4d295..c60c3cf4e 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -5,6 +5,8 @@ open Names
 open Term
 open Sign
 
+(* Inductive types (internal representation). *)
+
 type recarg = 
   | Param of int 
   | Norec 
@@ -15,11 +17,8 @@ type mutual_inductive_packet = {
   mind_consnames : identifier array;
   mind_typename : identifier;
   mind_lc : constr;
-  mind_stamp : name;
   mind_arity : typed_type;
-  mind_lamexp : constr option;
-  mind_kd : sorts list;
-  mind_kn : sorts list;
+  mind_kelim : sorts list;
   mind_listrec : (recarg list) array;
   mind_finite : bool }
 
@@ -31,12 +30,14 @@ type mutual_inductive_body = {
   mind_singl : constr option;
   mind_nparams : int }
 
-type mutual_inductive_entry = {
-  mind_entry_params : (identifier * constr) list;
-  mind_entry_inds : (identifier * constr * (identifier * constr) list) list }
-
 val mind_type_finite : mutual_inductive_body -> int -> bool
 
+
+(*s To give a more efficient access to the informations related to a given
+  inductive type, we introduce the following type [mind_specif], which
+  contains all the informations about the inductive type, including its
+  instanciation arguments. *)
+
 type mind_specif = {
   mis_sp : section_path;
   mis_mib : mutual_inductive_body;
@@ -47,9 +48,36 @@ type mind_specif = {
 val mis_ntypes : mind_specif -> int
 val mis_nconstr : mind_specif -> int
 val mis_nparams : mind_specif -> int
-val mis_kd : mind_specif -> sorts list
-val mis_kn : mind_specif -> sorts list
+val mis_kelim : mind_specif -> sorts list
 val mis_recargs : mind_specif -> (recarg list) array array
 
 val mind_nth_type_packet : 
   mutual_inductive_body -> int -> mutual_inductive_packet
+
+
+(*s Declaration of inductive types. *)
+
+type mutual_inductive_entry = {
+  mind_entry_nparams : int;
+  mind_entry_finite : bool;
+  mind_entry_inds : (identifier * constr * identifier list * constr) list }
+
+type inductive_error =
+  | NonPos of int   
+  | NotEnoughArgs of int
+  | NotConstructor  
+  | NonPar of int * int
+  | SameNamesTypes of identifier
+  | SameNamesConstructors of identifier * identifier
+  | NotAnArity of identifier
+  | BadEntry
+
+exception InductiveError of inductive_error
+
+val mind_check_names : mutual_inductive_entry -> unit
+
+val mind_extract_params : int -> constr -> (name * constr) list * constr
+val mind_extract_and_check_params : 
+  mutual_inductive_entry -> (name * constr) list
+
+val mind_check_lc : (name * constr) list -> mutual_inductive_entry -> unit
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c2309f8ed..7e8108945 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1165,265 +1165,6 @@ let compute_consteval env c =
   in
   try Some (srec 0 [] c) with Elimconst -> None
 
-let is_elim env c =
-  let (sp, cl) = destConst c in
-  if evaluable_const env c && defined_const env c && (not (is_existential c))
-  then
-    let cb = lookup_constant sp env in 
-    begin match cb.const_eval with
-      | Some _ -> ()
-      | None -> 
-	  (match cb.const_body with
-	     | Some {contents = Cooked b} ->
-		 cb.const_eval <- Some (compute_consteval env b)
-	     | Some {contents = Recipe _} ->
-		 anomalylabstrm "Reduction.is_elim"
-		   [< 'sTR"Found an uncooked transparent constant," ; 'sPC ;
-		      'sTR"which is supposed to be impossible" >]
-	     | _ -> assert false)
-    end;
-    match (cb.const_eval) with
-      | Some (Some x) -> x
-      | Some None -> raise Elimconst
-      | _ -> assert false
-  else 
-    raise Elimconst
-
-(* takes the fn first elements of the list and gives them back lifted by ln 
-   and in reverse order *)
-
-let rev_firstn_liftn fn ln = 
-  let rec rfprec p res l = 
-    if p = 0 then 
-      res 
-    else
-      match l with
-        | [] -> invalid_arg "Reduction.rev_firstn_liftn"
-        | a::rest -> rfprec (p-1) ((lift ln a)::res) rest
-  in 
-  rfprec fn [] 
-
-let make_elim_fun env f largs =
-  try 
-    let (lv,n,b) = is_elim env f 
-    and ll = List.length largs in
-    if ll < n then 
-      raise Redelimination 
-    else
-      if b then
-	let labs,_ = list_chop n largs in
-	let p = List.length lv in
-        let la' = 
-	  list_map_i 
-	    (fun q aq ->
-	       try (Rel (p+1-(list_index (n+1-q) (List.map fst lv)))) 
-	       with Failure _ -> aq) 
-	    1
-            (List.map (lift p) labs) 
-	in
-        list_fold_left_i 
-	  (fun i c (k,a) -> 
-             DOP2(Lambda,(substl (rev_firstn_liftn (n-k) (-i) la') a),
-		  DLAM(Name(id_of_string"x"),c))) 
-	  0 (applistc f la') lv
-      else 
-	f
-  with 
-    | Elimconst | Failure _ -> raise Redelimination
-
-let rec red_elim_const env k largs =
-  if not(evaluable_const env k) then raise Redelimination else
-    let f = make_elim_fun env k largs in
-    match whd_betadeltaeta_stack env (const_or_ex_value env k) largs with
-      | (DOPN(MutCase _,_) as mc,lrest) ->
-          let (ci,p,c,lf) = destCase mc in
-          (special_red_case env (construct_const env) p c ci lf, lrest)
-      | (DOPN(Fix _,_) as fix,lrest) -> 
-          let (b,(c,rest)) = 
-	    reduce_fix_use_function f (construct_const env) fix lrest
-          in 
-	  if b then (nf_beta env c, rest) else raise Redelimination
-      | _ -> assert false
-
-and construct_const env c stack = 
-  let rec hnfstack x stack =
-    match x with
-      | (DOPN(Const _,_)) as k  ->
-          (try
-             let (c',lrest) = red_elim_const env k stack in
-             hnfstack c' lrest
-           with 
-	     | Redelimination ->
-		 if evaluable_const env k then
-		   let cval = const_or_ex_value env k in
-		   (match cval with
-		      | DOPN (CoFix _,_) -> (k,stack)
-                      | _                -> hnfstack cval stack) 
-		 else 
-		   raise Redelimination)
-      | (DOPN(Abst _,_) as a) ->
-          if evaluable_abst env a then 
-	    hnfstack (abst_value env a) stack
-          else 
-	    raise Redelimination
-      | DOP2(Cast,c,_) -> hnfstack c stack
-      | DOPN(AppL,cl) -> hnfstack (array_hd cl) (array_app_tl cl stack)
-      | DOP2(Lambda,_,DLAM(_,c)) ->
-          (match stack with 
-             | [] -> assert false
-             | c'::rest -> stacklam hnfstack [c'] c rest)
-      | DOPN(MutCase _,_) as c_0 ->
-          let (ci,p,c,lf) = destCase c_0 in
-          hnfstack (special_red_case env (construct_const env) p c ci lf) stack
-      | DOPN(MutConstruct _,_) as c_0 -> c_0,stack
-      | DOPN(CoFix _,_) as c_0 -> c_0,stack
-      | DOPN(Fix (_) ,_) as fix -> 
-          let (reduced,(fix,stack')) = reduce_fix hnfstack fix stack in
-          if reduced then hnfstack fix stack' else raise Redelimination
-      | _ -> raise Redelimination
-  in 
-  hnfstack c stack
-
-(* Hnf reduction tactic: *)
-let hnf_constr env c = 
-  let rec redrec x largs =
-    match x with
-      | DOP2(Lambda,t,DLAM(n,c)) ->
-          (match largs with
-             | []      -> applist(x,largs)
-             | a::rest -> stacklam redrec [a] c rest)
-      | DOPN(AppL,cl)   -> redrec (array_hd cl) (array_app_tl cl largs)
-      | DOPN(Const _,_) ->
-          (try
-             let (c',lrest) = red_elim_const env x largs in
-             redrec c' lrest
-           with Redelimination ->
-             if evaluable_const env x then
-               let c = const_or_ex_value env x in
-               match c with 
-                 | DOPN(CoFix _,_) -> x
-                 | _ ->  redrec c largs
-             else 
-	       applist(x,largs))
-      | DOPN(Abst _,_) ->
-          if evaluable_abst env x then 
-	    redrec (abst_value env x) largs
-          else 
-	    applist(x,largs)
-      | DOP2(Cast,c,_) -> redrec c largs
-      | DOPN(MutCase _,_) ->
-          let (ci,p,c,lf) = destCase x in
-          (try
-             redrec (special_red_case env (whd_betadeltaiota_stack env)
-		       p c ci lf) largs
-           with Redelimination -> 
-	     applist(x,largs))
-      | (DOPN(Fix _,_)) ->
-          let (reduced,(fix,stack)) = 
-            reduce_fix (whd_betadeltaiota_stack env) x largs
-          in 
-	  if reduced then redrec fix stack else applist(x,largs)
-      | _ -> applist(x,largs)
-  in 
-  redrec c []
-
-
-(* Simpl reduction tactic: same as simplify, but also reduces elimination constants *)
-let whd_nf env c = 
-  let rec nf_app c stack =
-    match c with
-      | DOP2(Lambda,c1,DLAM(name,c2))    ->
-          (match stack with
-             | [] -> (c,[])
-             | a1::rest -> stacklam nf_app [a1] c2 rest)
-      | DOPN(AppL,cl)      -> nf_app (array_hd cl) (array_app_tl cl stack)
-      | DOP2(Cast,c,_) -> nf_app c stack
-      | DOPN(Const _,_) ->
-          (try
-             let (c',lrest) = red_elim_const env c stack in
-             nf_app c' lrest
-           with Redelimination -> 
-	     (c,stack))
-      | DOPN(MutCase _,_) ->
-          let (ci,p,d,lf) = destCase c in
-          (try
-             nf_app (special_red_case env nf_app p d ci lf) stack
-           with Redelimination -> 
-	     (c,stack))
-      | DOPN(Fix _,_) ->
-          let (reduced,(fix,rest)) = reduce_fix nf_app c stack in
-          if reduced then nf_app fix rest else (fix,stack)
-      | _ -> (c,stack)
-  in 
-  applist (nf_app c [])
-
-let nf env c = strong (whd_nf env) env c
-
-
-(* Generic reduction: reduction functions used in reduction tactics *)
-type red_expr =
-  | Red
-  | Hnf
-  | Simpl
-  | Cbv of flags
-  | Lazy of flags
-  | Unfold of (int list * section_path) list
-  | Fold of constr list
-  | Change of constr
-  | Pattern of (int list * constr * constr) list
-
-let reduction_of_redexp = function
-  | Red -> red_product
-  | Hnf -> hnf_constr
-  | Simpl -> nf
-  | Cbv f -> cbv_norm_flags f
-  | Lazy f -> clos_norm_flags f
-  | Unfold ubinds -> unfoldn ubinds
-  | Fold cl -> fold_commands cl
-  | Change t -> (fun _ _ -> t)
-  | Pattern lp -> pattern_occs lp
-
-(* Other reductions *)
-
-let one_step_reduce env = 
-  let rec redrec largs x =
-    match x with
-      | DOP2(Lambda,t,DLAM(n,c))  ->
-          (match largs with
-             | []      -> error "Not reducible 1"
-             | a::rest -> applistc (subst1 a c) rest)
-      | DOPN(AppL,cl) -> redrec (array_app_tl cl largs) (array_hd cl)
-      | DOPN(Const _,_) ->
-          (try
-             let (c',l) = red_elim_const env x largs in
-             applistc c' l
-           with Redelimination ->
-	     if evaluable_const env x then
-	       applistc (const_or_ex_value env x) largs
-	     else 
-	       error "Not reductible 1")
-      | DOPN(Abst _,_) ->
-          if evaluable_abst env x then 
-	    applistc (abst_value env x) largs
-          else 
-	    error "Not reducible 0"
-      | DOPN(MutCase _,_) ->
-          let (ci,p,c,lf) = destCase x in
-          (try  
-	     applistc (special_red_case env 
-			 (whd_betadeltaiota_stack env) p c ci lf) largs 
-           with Redelimination -> 
-	     error "Not reducible 2")
-      | DOPN(Fix _,_) ->
-          let (reduced,(fix,stack)) = 
-	    reduce_fix (whd_betadeltaiota_stack env) x largs
-          in 
-	  if reduced then applistc fix stack else error "Not reducible 3"
-      | DOP2(Cast,c,_) -> redrec largs c
-      | _ -> error "Not reducible 3"
-  in 
-  redrec []
-
 (* One step of approximation *)
 
 let rec apprec env c stack =
@@ -1446,7 +1187,6 @@ let rec apprec env c stack =
 
 let hnf env c = apprec env c []
 
-
 (* A reduction function like whd_betaiota but which keeps casts
  * and does not reduce redexes containing meta-variables.
  * ASSUMES THAT APPLICATIONS ARE BINARY ONES.
@@ -1486,39 +1226,6 @@ let whd_programs_stack env =
 
 let whd_programs env x = applist (whd_programs_stack env x [])
 
-
-(* Used in several tactics, moved from tactics.ml *)
-(* -- Eduardo                                     *)
-
-(* 
- * put t as t'=(x1:A1)..(xn:An)B with B an inductive definition of name name
- * return name, B and t' 
-*)
-
-let reduce_to_mind env t = 
-  let rec elimrec t l = 
-    match whd_castapp_stack t [] with
-      | (DOPN(MutInd _,_) as mind,_) -> (mind,t,prod_it t l)
-      | (DOPN(Const _,_),_) -> 
-          (try 
-	     let t' = nf_betaiota env (one_step_reduce env t) in
-             elimrec t' l
-           with UserError _ -> 
-	     errorlabstrm "tactics__reduce_to_mind"
-               [< 'sTR"Not an inductive product: it is a constant." >])
-      | (DOPN(MutCase _,_),_) ->
-          (try 
-	     let t' = nf_betaiota env (one_step_reduce env t) in
-             elimrec t' l
-           with UserError _ -> 
-	     errorlabstrm "tactics__reduce_to_mind"
-               [< 'sTR"Not an inductive product: it is a case analysis." >])
-      | (DOP2(Cast,c,_),[]) -> elimrec c l
-      | (DOP2(Prod,ty,DLAM(n,t')),[]) -> elimrec t' ((n,ty)::l)
-      | _ -> error "Not an inductive product"
-  in 
-  elimrec t []
-    
 let find_mrectype env c =
   let (t,l) = whd_betadeltaiota_stack env c [] in
   match t with
@@ -1563,24 +1270,24 @@ let check_mrectype_spec env c =
 
 exception IsType
 
-let info_arity env = 
+let is_arity env = 
   let rec srec c = 
     match whd_betadeltaiota env c with 
-      | DOP0(Sort(Prop(Null)))  -> false 
-      | DOP0(Sort(Prop(Pos)))  -> true 
+      | DOP0(Sort _) -> true
       | DOP2(Prod,_,DLAM(_,c')) -> srec c' 
       | DOP2(Lambda,_,DLAM(_,c')) -> srec c' 
-      | _ -> raise IsType
+      | _ -> false
   in 
   srec 
-    
-let is_type_arity env = 
+ 
+let info_arity env = 
   let rec srec c = 
     match whd_betadeltaiota env c with 
-      | DOP0(Sort(Type(_)))  -> true
+      | DOP0(Sort(Prop Null)) -> false 
+      | DOP0(Sort(Prop Pos)) -> true 
       | DOP2(Prod,_,DLAM(_,c')) -> srec c' 
       | DOP2(Lambda,_,DLAM(_,c')) -> srec c' 
-      | _ -> false
+      | _ -> raise IsType
   in 
   srec 
     
@@ -1590,6 +1297,16 @@ let is_logic_arity env c =
 let is_info_arity env c = 
   try (info_arity env c) with IsType -> true
    
+let is_type_arity env = 
+  let rec srec c = 
+    match whd_betadeltaiota env c with 
+      | DOP0(Sort(Type _)) -> true
+      | DOP2(Prod,_,DLAM(_,c')) -> srec c' 
+      | DOP2(Lambda,_,DLAM(_,c')) -> srec c' 
+      | _ -> false
+  in 
+  srec 
+    
 let is_info_cast_type env c = 
   match c with  
     | DOP2(Cast,c,t) -> 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index cc5bfba3e..0f53d600b 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -83,9 +83,6 @@ val whd_ise1 : 'a reduction_function
 val nf_ise1 : 'a reduction_function
 val whd_ise1_metas : 'a reduction_function
 
-val red_elim_const : 'a stack_reduction_function
-val one_step_reduce : 'a reduction_function
-
 val hnf_prod_app : 'c unsafe_env -> string -> constr -> constr -> constr
 val hnf_prod_appvect : 
   'c unsafe_env -> string -> constr -> constr array -> constr
@@ -102,6 +99,7 @@ val decomp_prod : 'c unsafe_env -> constr -> int * constr
 val decomp_n_prod : 
   'c unsafe_env -> int -> constr -> ((name * constr) list) * constr
 
+val is_arity : 'c unsafe_env -> constr -> bool
 val is_info_arity : 'c unsafe_env -> constr -> bool
 val is_info_sort : 'c unsafe_env -> constr -> bool
 val is_logic_arity : 'c unsafe_env -> constr -> bool
@@ -109,34 +107,16 @@ val is_type_arity : 'c unsafe_env -> constr -> bool
 val is_info_cast_type : 'c unsafe_env -> constr -> bool
 val contents_of_cast_type : 'c unsafe_env -> constr -> contents
 val poly_args : 'a unsafe_env -> constr -> int list
-val reduce_to_mind : 'c unsafe_env -> constr -> constr * constr * constr
-
 
 val whd_programs : 'a reduction_function
 
-
-(*s Generic reduction: reduction functions associated to tactics *)
-type red_expr =
-  | Red
-  | Hnf
-  | Simpl
-  | Cbv of flags
-  | Lazy of flags
-  | Unfold of (int list * section_path) list
-  | Fold of constr list
-  | Change of constr
-  | Pattern of (int list * constr * constr) list
-
-val nf : 'a reduction_function
 val unfoldn : 
   (int list * section_path) list -> 'a reduction_function
 val fold_one_com : constr -> 'a reduction_function
 val fold_commands : constr list -> 'a reduction_function
 val subst_term_occ : int list -> constr -> constr -> constr
 val pattern_occs : (int list * constr * constr) list -> 'a reduction_function
-val hnf_constr : 'a reduction_function
 val compute : 'a reduction_function
-val reduction_of_redexp : red_expr -> 'a reduction_function
 
 
 (*s Conversion Functions (uses closures, lazy strategy) *)
diff --git a/kernel/sosub.ml b/kernel/sosub.ml
index e2f269899..904d089d3 100644
--- a/kernel/sosub.ml
+++ b/kernel/sosub.ml
@@ -40,13 +40,13 @@ let propagate_name smap argt new_na =
     | (_, _) -> smap
 	  
 let is_soapp_operator = function
-  | DOPN(XTRA("$SOAPP",[]),cl) -> true
-  | DOP2(XTRA("$SOAPP",[]),_,_) -> true
+  | DOPN(XTRA "$SOAPP",cl) -> true
+  | DOP2(XTRA "$SOAPP",_,_) -> true
   | _ -> false
 	
 let dest_soapp_operator = function
-  | DOPN(XTRA("$SOAPP",[]),cl) -> (array_hd cl,array_list_of_tl cl)
-  | DOP2(XTRA("$SOAPP",[]),c1,c2) -> (c1,[c2])
+  | DOPN(XTRA "$SOAPP",cl) -> (array_hd cl,array_list_of_tl cl)
+  | DOP2(XTRA "$SOAPP",c1,c2) -> (c1,[c2])
   | _ -> failwith "dest_soapp_operator"
 	
 let solam_names = 
diff --git a/kernel/term.ml b/kernel/term.ml
index a662f7439..94ce20615 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -26,7 +26,7 @@ type 'a oper =
   | Fix of int array * int
   | CoFix of int
 
-  | XTRA of string * Coqast.t list
+  | XTRA of string
       (* an extra slot, for putting in whatever sort of
          operator we need for whatever sort of application *)
 
@@ -77,7 +77,7 @@ let incast_type tty = DOP2 (Cast, tty.body, (DOP0 (Sort tty.typ)))
 let mkRel   n = (Rel n)
 
 (* Constructs an existential variable named "?" *)
-let mkExistential = (DOP0 (XTRA ("ISEVAR",[])))
+let mkExistential = (DOP0 (XTRA "ISEVAR"))
 
 (* Constructs an existential variable named "?n" *)
 let mkMeta  n =  DOP0 (Meta n)
@@ -86,7 +86,7 @@ let mkMeta  n =  DOP0 (Meta n)
 let mkVar id = VAR id
 
 (* Construct an XTRA term (XTRA is an extra slot for whatever you want) *)
-let mkXtra s astlist = (DOP0 (XTRA (s, astlist)))
+let mkXtra s = (DOP0 (XTRA s))
 
 (* Construct a type *)
 let mkSort s = DOP0 (Sort s)
@@ -243,7 +243,7 @@ let destVar = function
 
 (* Destructs an XTRA *)
 let destXtra = function
-  | DOP0 (XTRA (s,astlist)) -> (s,astlist)
+  | DOP0 (XTRA s) -> s
   | _ -> invalid_arg "destXtra"
 
 (* Destructs a type *)
@@ -468,7 +468,7 @@ type kindOfTerm =
   | IsRel            of int
   | IsMeta           of int
   | IsVar            of identifier
-  | IsXtra           of string * (Coqast.t list)
+  | IsXtra           of string
   | IsSort           of sorts
   | IsImplicit       
   | IsCast           of constr*constr
@@ -498,7 +498,7 @@ let kind_of_term c =
     | VAR id                               -> IsVar id 
     | DOP0 (Meta n)                        -> IsMeta  n
     | DOP0 (Sort s)                        -> IsSort  s
-    | DOP0 (XTRA (s, astlist))             -> IsXtra (s,astlist)
+    | DOP0 (XTRA s)                        -> IsXtra s
     | DOP0 Implicit                        -> IsImplicit
     | DOP2 (Cast, t1, t2)                  -> IsCast   (t1,t2)
     | DOP2 (Prod, t1, (DLAM (x,t2)))       -> IsProd (x,t1,t2) 
@@ -807,7 +807,7 @@ let lam_and_popl_named  n env t l =
   poprec (n,(env,t,l,[]))
 
 (* [lambda_ize n T endpt]
- * will pop off the first n products in T, then stick in endpt,
+ * will pop off the first [n] products in [T], then stick in [endpt],
  * properly lifted, and then push back the products, but as lambda-
  * abstractions *)
 let lambda_ize n t endpt =
@@ -1169,59 +1169,6 @@ let rec occur_meta = function
 
 let rel_vect = (Generic.rel_vect : int -> int -> constr array)
 		 
-(* Transforms a constr into a matchable constr*)
-let rec matchable=function
-  | DOP1(op,t) ->
-      DOP1(op,matchable t)
-  | DOP2(op,t1,t2) ->
-      DOP2(op,matchable t1,matchable t2)
-  | DOPN(op,tab) ->
-      (match op with
-         | MutInd(sp,rk) ->
-             DOPL(XTRA("IT",[Coqast.Id((rk,0),string_of_path sp)]),
-		  Array.to_list (Array.map matchable tab))
-         | MutConstruct((sp,rkt),rkc) ->
-             DOPL(XTRA("IC",[Coqast.Id((rkt,rkc),string_of_path sp)]),
-		  Array.to_list (Array.map matchable tab))
-         | Const sp ->
-             DOPL(XTRA("C",[Coqast.Id((0,0),string_of_path sp)]),
-		  Array.to_list (Array.map matchable tab))
-         | a ->
-             DOPL(a,Array.to_list (Array.map matchable tab)))
-  | DOPL(op,lst) ->
-      DOPL(op,List.map matchable lst)
-  | DLAM(ne,t) ->
-      DLAM(ne,matchable t)
-  | DLAMV(ne,tab) ->
-      DLAMV(ne,(Array.map matchable tab))
-  | a -> a
-
-let rec unmatchable=function
-  | DOP1(op,t) ->
-      DOP1(op,unmatchable t)
-  | DOP2(op,t1,t2) ->
-      DOP2(op,unmatchable t1,unmatchable t2)
-  | DOPN(op,tab) ->
-      DOPN(op,Array.map unmatchable tab)
-  | DOPL(op,lst) ->
-      (match op with
-         | XTRA("IT",[Coqast.Id((rk,0),str)]) ->
-             DOPN(MutInd(path_of_string str,rk),
-		  Array.of_list (List.map unmatchable lst))
-         | XTRA("IC",[Coqast.Id((rkt,rkc),str)]) ->
-             DOPN(MutConstruct((path_of_string str,rkt),rkc),
-		  Array.of_list (List.map unmatchable lst))
-         | XTRA("C",[Coqast.Id((0,0),str)]) ->
-             DOPN(Const(path_of_string str),
-		  Array.of_list (List.map unmatchable lst))
-         | a ->
-             DOPN(a,Array.of_list (List.map unmatchable lst)))
-  | DLAM(ne,t) ->
-      DLAM(ne,unmatchable t)
-  | DLAMV(ne,tab) ->
-      DLAMV(ne,(Array.map unmatchable tab))
-  | a -> a
-
 
 (***************************)
 (* hash-consing functions  *)                         
@@ -1248,10 +1195,10 @@ module Hoper =
   Hashcons.Make(
     struct
       type t = sorts oper
-      type u = (Coqast.t -> Coqast.t) * (sorts -> sorts)
+      type u = (sorts -> sorts)
                * (section_path -> section_path) * (string -> string)
-      let hash_sub (hast,hsort,hsp,hstr) = function
-	| XTRA(s,al) -> XTRA(hstr s, List.map hast al)
+      let hash_sub (hsort,hsp,hstr) = function
+	| XTRA s -> XTRA (hstr s)
         | Sort s -> Sort (hsort s)
         | Const sp -> Const (hsp sp)
         | Abst sp -> Abst (hsp sp)
@@ -1261,9 +1208,7 @@ module Hoper =
         | t -> t 
       let equal o1 o2 =
         match (o1,o2) with
-          | (XTRA(s1,al1), XTRA(s2,al2)) ->
-              (s1==s2 & List.length al1 = List.length al2)
-              & List.for_all2 (==) al1 al2
+          | (XTRA s1, XTRA s2) -> s1==s2
           | (Sort s1, Sort s2) -> s1==s2
           | (Const sp1, Const sp2) -> sp1==sp2
           | (Abst sp1, Abst sp2) -> sp1==sp2
@@ -1287,11 +1232,11 @@ module Hconstr =
       let hash = Hashtbl.hash
     end)
 
-let hcons_oper (hast,hsorts,hsp,hstr) =
-  Hashcons.simple_hcons Hoper.f (hast,hsorts,hsp,hstr)
+let hcons_oper (hsorts,hsp,hstr) =
+  Hashcons.simple_hcons Hoper.f (hsorts,hsp,hstr)
 
-let hcons_term (hast,hsorts,hsp,hname,hident,hstr) =
-  let hoper = hcons_oper (hast,hsorts,hsp,hstr) in
+let hcons_term (hsorts,hsp,hname,hident,hstr) =
+  let hoper = hcons_oper (hsorts,hsp,hstr) in
   Hashcons.recursive_hcons Hconstr.f (hoper,hname,hident)
 
 module Htype =
@@ -1307,9 +1252,8 @@ module Htype =
 let hcons_constr (hspcci,hspfw,hname,hident,hstr) =
   let hsortscci = Hashcons.simple_hcons Hsorts.f hspcci in
   let hsortsfw = Hashcons.simple_hcons Hsorts.f hspfw in
-  let (hast,_) = Coqast.hcons_ast hstr in
-  let hcci = hcons_term (hast,hsortscci,hspcci,hname,hident,hstr) in
-  let hfw = hcons_term (hast,hsortsfw,hspfw,hname,hident,hstr) in
+  let hcci = hcons_term (hsortscci,hspcci,hname,hident,hstr) in
+  let hfw = hcons_term (hsortsfw,hspfw,hname,hident,hstr) in
   let htcci = Hashcons.simple_hcons Htype.f (hcci,hsortscci) in
   (hcci,hfw,htcci)
 
diff --git a/kernel/term.mli b/kernel/term.mli
index ee60fbedd..0af1cf613 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -24,7 +24,7 @@ type 'a oper =
   | Fix of int array * int
   | CoFix of int
 
-  | XTRA of string * Coqast.t list
+  | XTRA of string
       (* an extra slot, for putting in whatever sort of
          operator we need for whatever sort of application *)
 
@@ -73,7 +73,7 @@ type kindOfTerm =
   | IsRel          of int
   | IsMeta         of int
   | IsVar          of identifier
-  | IsXtra         of string * Coqast.t list
+  | IsXtra         of string
   | IsSort         of sorts
   | IsImplicit
   | IsCast         of constr * constr
@@ -112,7 +112,7 @@ val mkMeta : int -> constr
 val mkVar : identifier -> constr
 
 (* Construct an  [XTRA] term. *)
-val mkXtra : string -> Coqast.t list -> constr
+val mkXtra : string -> constr
 
 (* Construct a type *)
 val mkSort : sorts -> constr
@@ -232,7 +232,7 @@ val isMETA : constr -> bool
 val destVar : constr -> identifier
 
 (* Destructs an XTRA *)
-val destXtra : constr -> string * Coqast.t list
+val destXtra : constr -> string
 
 (* Destructs a sort. [is_Prop] recognizes the sort \textsf{Prop}, whether 
    [isprop] recognizes both \textsf{Prop} and \textsf{Set}. *)
@@ -417,8 +417,7 @@ val prod_and_pop :
     -> (name * constr) list * constr * (int * constr) list
 
 (* recusively applies [prod_and_pop] :
-   if [env] = $[na_1:T_1 ; na_2:T_2 ; ... ; na_n:T_n]@tlenv$
-   then
+   if [env] = $[na_1:T_1 ; na_2:T_2 ; ... ; na_n:T_n]@tlenv$ then
    [(prod_and_popl n env T l)] gives $(tlenv,(na_n:T_n)...(na_1:T_1)T,l')$
    where $l'$ is [l] lifted down [n] steps *)
 val prod_and_popl :
@@ -508,10 +507,6 @@ val replace_consts :
 
 val subst_meta : (int * constr) list -> constr -> constr
 
-(* Transforms a constr into a matchable constr *)
-val matchable : constr -> constr
-val unmatchable: constr -> constr
-
 
 (*s Hash-consing functions for constr. *)
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 178963c48..40f41d603 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -204,7 +204,7 @@ let error_elim_expln env kp ki =
 
 exception Arity of (constr * constr * string) option
 
-let is_correct_arity env kd kn (c,p) = 
+let is_correct_arity env kelim (c,p) = 
   let rec srec ind (pt,t) =
     try 
       (match whd_betadeltaiota env pt, whd_betadeltaiota env t with
@@ -218,7 +218,7 @@ let is_correct_arity env kd kn (c,p) =
              let ksort = (match k with DOP0(Sort s) -> s 
 			    | _ -> raise (Arity None)) in
              if is_conv env a1 ind then
-               if List.exists (base_sort_cmp CONV ksort) kd then
+               if List.exists (base_sort_cmp CONV ksort) kelim then
 		 (true,k)
                else 
 		 raise (Arity (Some(k,ki,error_elim_expln env k ki)))
@@ -229,14 +229,14 @@ let is_correct_arity env kd kn (c,p) =
 	 | k, ki -> 
 	     let ksort = (match k with DOP0(Sort s) -> s 
                             | _ ->  raise (Arity None)) in
-             if List.exists (base_sort_cmp CONV ksort) kn then 
+             if List.exists (base_sort_cmp CONV ksort) kelim then 
 	       false,k
              else 
 	       raise (Arity (Some(k,ki,error_elim_expln env k ki))))
     with Arity kinds ->
       let listarity =
-	(List.map (fun s -> make_arity_dep env (DOP0(Sort s)) t ind) kd)
-	@(List.map (fun s -> make_arity_nodep env (DOP0(Sort s)) t) kn)
+	(List.map (fun s -> make_arity_dep env (DOP0(Sort s)) t ind) kelim)
+	@(List.map (fun s -> make_arity_nodep env (DOP0(Sort s)) t) kelim)
       in error_elim_arity CCI env ind listarity c p pt kinds
   in srec 
 
@@ -247,13 +247,12 @@ let cast_instantiate_arity mis =
 let find_case_dep_nparams env (c,p) (mind,largs) typP =    
   let mis = lookup_mind_specif mind env in 
   let nparams = mis_nparams mis
-  and kd = mis_kd mis 
-  and kn = mis_kn mis
+  and kelim = mis_kelim mis 
   and t = cast_instantiate_arity mis in 
   let (globargs,la) = list_chop nparams largs in
   let glob_t = hnf_prod_applist env "find_elim_boolean" t globargs in
   let arity = applist(mind,globargs) in
-  let (dep,_) = is_correct_arity env kd kn (c,p) arity (typP,glob_t) in
+  let (dep,_) = is_correct_arity env kelim (c,p) arity (typP,glob_t) in
   (dep, (nparams, globargs,la))
 
 let type_one_branch_dep (env,nparams,globargs,p) co t = 
diff --git a/kernel/typing.ml b/kernel/typing.ml
index ebae3faf9..0b236ce44 100644
--- a/kernel/typing.ml
+++ b/kernel/typing.ml
@@ -14,6 +14,7 @@ open Inductive
 open Environ
 open Type_errors
 open Typeops
+open Indtypes
 
 (* Fonctions temporaires pour relier la forme castée de la forme jugement *)
 
@@ -58,10 +59,10 @@ let rec execute mf env cstr =
 	in
         (match kind_of_term metaty with
            | IsCast (typ,kind) -> 
-	       ({ uj_val = cstr; uj_type = typ; uj_kind = kind}, u0)
+	       ({ uj_val = cstr; uj_type = typ; uj_kind = kind }, u0)
            | _ ->
 	       let (jty,u1) = execute mf env metaty in
-	       let k = hnf_constr env jty.uj_type in
+	       let k = whd_betadeltaiotaeta env jty.uj_type in
 	       ({ uj_val = cstr; uj_type = metaty; uj_kind = k }, u1))
 	
     | IsRel n -> 
@@ -248,13 +249,11 @@ let lookup_mind = lookup_mind
 let lookup_mind_specif = lookup_mind_specif
 let lookup_meta = lookup_meta
 
-let push_rel_or_var push (id,ty) env =
-  let (j,u) = safe_machine env ty.body in
+let push_rel_or_var push (id,c) env =
+  let (j,u) = safe_machine env c in
   let env' = set_universes u env in
-  let expty = DOP0(Sort ty.typ) in
-  match conv env' j.uj_type expty with
-    | Convertible u' -> push (id,ty) (set_universes u' env')
-    | NotConvertible -> error_actual_type CCI env ty.body j.uj_type expty
+  let var = assumption_of_judgement env' j in
+  push (id,var) env'
 
 let push_var nvar env = push_rel_or_var push_var nvar env
 
@@ -272,8 +271,7 @@ let add_constant sp ce env =
 	  const_body = Some (ref (Cooked ce.const_entry_body));
 	  const_type = typed_type_of_judgment env'' jt;
 	  const_hyps = get_globals (context env);
-	  const_opaque = false;
-	  const_eval = None } 
+	  const_opaque = false } 
 	in
 	add_constant sp cb (set_universes u'' env'')
     | NotConvertible -> 
@@ -292,31 +290,46 @@ let add_parameter sp c env =
     const_body = Some (ref (Cooked c));
     const_type = type_from_judgment env' j;
     const_hyps = get_globals (context env);
-    const_opaque = false;
-    const_eval = None } 
+    const_opaque = false } 
   in
   Environ.add_constant sp cb env'
 
-let add_mind sp me env =
-  let name_params = 
-    List.map (fun (id,c) -> (Name id, c)) me.mind_entry_params in
-  (* just to check the params *)
-  let env_params =
-    List.fold_left 
-      (fun env (id,c) ->
-	 let (j,u) = safe_machine env c in
-	 let env' = set_universes u env in
-	 Environ.push_var (id, assumption_of_judgement env' j) env')
-      env me.mind_entry_params
+let push_vars vars env =
+  List.fold_left (fun env nvar -> push_var nvar env) env vars
+
+let push_rels vars env =
+  List.fold_left (fun env nvar -> push_rel nvar env) env vars
+
+let check_type_constructs env_params univ nparams lc =
+  let check_one env c =
+    let (_,c) = decompose_prod_n nparams c in
+    let (j,u) = safe_machine env c in
+    match whd_betadeltaiota env j.uj_type with
+      | DOP0 (Sort (Type uc)) -> set_universes (enforce_geq univ uc u) env
+      | _ -> error "Type of Constructor not well-formed"
+  in
+  Array.fold_left check_one env_params lc
+
+let check_prop_constructs env_ar lc =
+  let check_one c = 
+    let (j,_) = safe_machine env_ar c in
+    match whd_betadeltaiota env_ar j.uj_type with
+      | DOP0 (Sort _) -> cast_of_judgment j
+      | _ -> error "The type of a constructor must be a type"
   in
-  let env_arities =
-    List.fold_left 
-      (fun env (id,ar,_) -> 
-	 let (j,u) = safe_machine env (prod_it ar name_params) in
-	 let env' = set_universes u env in
-	 Environ.push_var (id, assumption_of_judgement env' j) env')
-      env me.mind_entry_inds
+  Array.map check_one lc
+
+let add_mind sp mie env =
+  mind_check_names mie;
+  mind_check_arities env mie;
+  let params = mind_extract_and_check_params mie in
+  mind_check_lc params mie;
+  let env_arities = 
+    push_rels 
+      (List.map (fun (id,ar,_,_) -> (Name id,ar)) mie.mind_entry_inds) env 
   in
+  let env_params = push_rels params env_arities in
+  (* ICI *)
   env_arities
 
 type judgment = unsafe_judgment
diff --git a/kernel/typing.mli b/kernel/typing.mli
index e67308d26..314554e85 100644
--- a/kernel/typing.mli
+++ b/kernel/typing.mli
@@ -23,8 +23,8 @@ val universes : 'a environment -> universes
 val metamap : 'a environment -> (int * constr) list
 val context : 'a environment -> context
 
-val push_var : identifier * typed_type -> 'a environment -> 'a environment
-val push_rel : name * typed_type -> 'a environment -> 'a environment
+val push_var : identifier * constr -> 'a environment -> 'a environment
+val push_rel : name * constr -> 'a environment -> 'a environment
 val add_constant : 
   section_path -> constant_entry -> 'a environment -> 'a environment
 val add_parameter :