Nouveaux types 'constructor' et 'inductive' dans Term;

les fonctions sur les inductifs prennent maintenant des 'inductive' en
paramètres; elle n'ont plus besoin de faire des appels dangereux
aux find_m*type qui centralisent la levée de raise Induc.


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

15 files changed, 173 insertions, 142 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index eaa87b5be..c8c85c76e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -127,13 +127,10 @@ let lookup_constant sp env =
 let lookup_mind sp env =
   Spmap.find sp env.env_globals.env_inductives
 
-let lookup_mind_specif i env =
-  match i with
-    | DOPN (MutInd (sp,tyi), args) ->
-	let mib = lookup_mind sp env in
-	{ mis_sp = sp; mis_mib = mib; mis_tyi = tyi; mis_args = args;
-	  mis_mip = mind_nth_type_packet mib tyi }
-    | _ -> invalid_arg "lookup_mind_specif"
+let lookup_mind_specif ((sp,tyi),args) env =
+  let mib = lookup_mind sp env in
+  { mis_sp = sp; mis_mib = mib; mis_tyi = tyi; mis_args = args;
+    mis_mip = mind_nth_type_packet mib tyi }
 
 let lookup_abst sp env =
   Spmap.find sp env.env_globals.env_abstractions
diff --git a/kernel/environ.mli b/kernel/environ.mli
index ffb5861e1..6d38ad819 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -46,7 +46,7 @@ val lookup_var : identifier -> env -> name * typed_type
 val lookup_rel : int -> env -> name * typed_type
 val lookup_constant : section_path -> env -> constant_body
 val lookup_mind : section_path -> env -> mutual_inductive_body
-val lookup_mind_specif : constr -> env -> mind_specif
+val lookup_mind_specif : inductive -> env -> mind_specif
 
 val id_of_global : env -> sorts oper -> identifier
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index da9604699..cdb45e9d4 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -111,7 +111,7 @@ let listrec_mconstr env ntypes nparams i indlc =
                  let hd = array_hd cl 
 		 and largs = array_tl cl in
                  (match hd with 
-                    | Rel k -> 
+                    | Rel k ->
                         if k >= n && k<n+ntypes then begin
 			  check_correct_par env nparams ntypes n (k-n+1) largs;
 			  Mrec(n+ntypes-k-1) 
@@ -121,17 +121,17 @@ let listrec_mconstr env ntypes nparams i indlc =
                           else Norec
 			else 
 			  raise (IllFormedInd (NonPos n))
-                    | (DOPN(MutInd(sp,i),_) as mi) -> 
+                    | DOPN(MutInd ind_sp,a) -> 
                         if (noccur_bet n ntypes x) then
                           Norec
                         else 
-			  Imbr(sp,i,imbr_positive n mi largs)
+			  Imbr(ind_sp,imbr_positive n (ind_sp,a) largs)
                     | err -> 
 			if noccur_bet n ntypes x then Norec
 			else raise (IllFormedInd (NonPos n)))
              | _ -> anomaly "check_pos")
 	  
-  and imbr_positive n mi largs = 
+  and imbr_positive n mi largs =
     let mispeci = lookup_mind_specif mi env in
     let auxnpar = mis_nparams mispeci in
     let (lpar,auxlargs) = array_chop auxnpar largs in 
@@ -197,10 +197,10 @@ let listrec_mconstr env ntypes nparams i indlc =
                           then Param(n-1-k)
                           else Norec
 			else raise (IllFormedInd (NonPos n))
-                    | (DOPN(MutInd(sp,i),_) as mi) -> 
+                    | DOPN(MutInd ind_sp,a) -> 
                         if (noccur_bet n ntypes x) 
                         then Norec
-                        else Imbr(sp,i,imbr_positive n mi largs)
+                        else Imbr(ind_sp,imbr_positive n (ind_sp,a) largs)
                     | err -> if noccur_bet n ntypes x then Norec
 		      else raise (IllFormedInd (NonPos n)))
              | _ -> anomaly "check_param_pos")
@@ -249,7 +249,7 @@ let listrec_mconstr env ntypes nparams i indlc =
 let is_recursive listind =
   let rec one_is_rec rvec = 
     List.exists (function Mrec(i) -> List.mem i listind 
-                   | Imbr(_,_,lvec) -> one_is_rec lvec
+                   | Imbr(_,lvec) -> one_is_rec lvec
                    | Norec -> false
                    | Param _ -> false) rvec
   in 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index e46be516a..41342e6d4 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -12,7 +12,7 @@ type recarg =
   | Param of int 
   | Norec 
   | Mrec of int 
-  | Imbr of section_path * int * (recarg list)
+  | Imbr of inductive_path * recarg list
 
 type mutual_inductive_packet = {
   mind_consnames : identifier array;
@@ -51,11 +51,22 @@ let mis_recarg mis = mis.mis_mip.mind_listrec
 let mis_typename mis = mis.mis_mip.mind_typename
 let mis_consnames mis = mis.mis_mip.mind_consnames
 
+(* A light version of mind_specif_of_mind with pre-splitted args *)
+type inductive_summary =
+    {fullmind : constr;
+     mind : inductive;
+     nparams : int;
+     nrealargs : int;
+     nconstr : int;
+     params : constr list;
+     realargs : constr list;
+     arity : constr}
+
 let is_recursive listind = 
   let rec one_is_rec rvec = 
     List.exists (function
 		   | Mrec(i)        -> List.mem i listind 
-                   | Imbr(_,_,lvec) -> one_is_rec lvec
+                   | Imbr(_,lvec) -> one_is_rec lvec
                    | Norec          -> false
                    | Param(_)       -> false) rvec
   in 
@@ -158,4 +169,8 @@ let mind_check_lc params mie =
   in
   List.iter check_lc mie.mind_entry_inds
 
-let inductive_of_constructor (ind_sp,i) = ind_sp
+let inductive_path_of_constructor_path (ind_sp,i) = ind_sp
+let ith_constructor_path_of_inductive_path ind_sp i = (ind_sp,i)
+
+let inductive_of_constructor ((ind_sp,i),args) = (ind_sp,args)
+let ith_constructor_of_inductive (ind_sp,args) i = ((ind_sp,i),args)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 63e85a539..c28d35c8d 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -14,7 +14,7 @@ type recarg =
   | Param of int 
   | Norec 
   | Mrec of int 
-  | Imbr of section_path * int * (recarg list)
+  | Imbr of inductive_path * (recarg list)
 
 type mutual_inductive_packet = {
   mind_consnames : identifier array;
@@ -63,6 +63,20 @@ val mis_consnames : mind_specif -> identifier array
 val mind_nth_type_packet : 
   mutual_inductive_body -> int -> mutual_inductive_packet
 
+(* A light version of mind_specif_of_mind with pre-splitted args
+   Invariant: We have
+   -- Hnf (fullmind) = DOPN(AppL,[|MutInd mind;..params..;..realargs..|])
+   -- with mind  = ((sp,i),localvars) for some sp, i, localvars
+ *)
+type inductive_summary =
+    {fullmind : constr;
+     mind : inductive;
+     nparams : int;
+     nrealargs : int;
+     nconstr : int;
+     params : constr list;
+     realargs : constr list;
+     arity : constr}
 
 (*s Declaration of inductive types. *)
 
@@ -107,4 +121,11 @@ val mind_extract_params : int -> constr -> (name * constr) list * constr
 
 val mind_check_lc : (name * constr) list -> mutual_inductive_entry -> unit
 
-val inductive_of_constructor : constructor_path -> inductive_path
+val inductive_of_constructor : constructor -> inductive
+
+val ith_constructor_of_inductive : inductive -> int -> constructor
+
+val inductive_path_of_constructor_path : constructor_path -> inductive_path
+
+val ith_constructor_path_of_inductive_path :
+  inductive_path -> int -> constructor_path
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5b0fbe61c..84277eb22 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -15,7 +15,6 @@ open Instantiate
 open Closure
 
 exception Redelimination
-exception Induc
 exception Elimconst
 
 type 'a reduction_function = env -> 'a evar_map -> constr -> constr
@@ -480,9 +479,9 @@ let mind_nparams env i =
   let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams
 
 let reduce_mind_case env mia =
-  match mia.mconstr with 
-    | DOPN(MutConstruct((indsp,tyindx),i),_) ->
-	let ind = DOPN(MutInd(indsp,tyindx),args_of_mconstr mia.mconstr) in
+  match mia.mconstr with
+    | DOPN(MutConstruct (ind_sp,i as cstr_sp),args) ->
+	let ind = inductive_of_constructor (cstr_sp,args) in
 	let nparams = mind_nparams env ind in
 	let real_cargs = snd (list_chop nparams mia.mcargs) in
         applist (mia.mlf.(i-1),real_cargs)
@@ -1125,47 +1124,42 @@ let whd_programs_stack env sigma =
 
 let whd_programs env sigma x = applist (whd_programs_stack env sigma x [])
 
+exception Induc
+
 let find_mrectype env sigma c =
   let (t,l) = whd_betadeltaiota_stack env sigma c [] in
   match t with
-    | DOPN(MutInd (sp,i),_) ->  (t,l)
+    | DOPN(MutInd ind_sp,args) ->  ((ind_sp,args),l)
     | _ -> raise Induc
 
 let find_minductype env sigma c =
   let (t,l) = whd_betadeltaiota_stack env sigma c [] in
   match t with
     | DOPN(MutInd (sp,i),_)
-        when mind_type_finite (lookup_mind sp env) i -> (t,l)
+        when mind_type_finite (lookup_mind sp env) i -> (destMutInd t,l)
     | _ -> raise Induc
 
 let find_mcoinductype env sigma c =
   let (t,l) = whd_betadeltaiota_stack env sigma c [] in
   match t with
     | DOPN(MutInd (sp,i),_)
-        when not (mind_type_finite (lookup_mind sp env) i) -> (t,l)
+        when not (mind_type_finite (lookup_mind sp env) i) -> (destMutInd t,l)
     | _ -> raise Induc
 
-let minductype_spec env sigma c = 
-  try 
-    let (x,l) = find_minductype env sigma c in
-    if l<>[] then anomaly "minductype_spec: Not a recursive type 1" else x
-  with Induc -> 
-    anomaly "minductype_spec: Not a recursive type 2"
-      
-let mrectype_spec env sigma c = 
-  try 
-    let (x,l) = find_mrectype env sigma c in
-    if l<>[] then anomaly "mrectype_spec: Not a recursive type 1" else x
-  with Induc -> 
-    anomaly "mrectype_spec: Not a recursive type 2"
-
-let check_mrectype_spec env sigma c =
-  try 
-    let (x,l) = find_mrectype env sigma c in
-    if l<>[] then error "check_mrectype: Not a recursive type 1" else x
-  with Induc -> 
-    error "check_mrectype: Not a recursive type 2"
-
+(* raise Induc if not an inductive type *)
+let try_mutind_of env sigma ty =
+  let (mind,largs) = find_mrectype env sigma ty in
+  let mispec = lookup_mind_specif mind env in 
+  let nparams = mis_nparams mispec in
+  let (params,realargs) = list_chop nparams largs in 
+  {fullmind = ty;
+   mind     = mind;
+   nparams  = nparams;
+   nrealargs = List.length realargs;
+   nconstr  = mis_nconstr mispec;
+   params   = params;
+   realargs = realargs;
+   arity    = Instantiate.mis_arity mispec}
 
 exception IsType
 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index dd06af8ad..6638f30ee 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -14,7 +14,6 @@ open Closure
 (* Reduction Functions. *)
 
 exception Redelimination
-exception Induc
 exception Elimconst
 
 type 'a reduction_function = env -> 'a evar_map -> constr -> constr
@@ -191,18 +190,25 @@ val whd_ise1 : 'a evar_map -> constr -> constr
 val nf_ise1 : 'a evar_map -> constr -> constr
 val whd_ise1_metas : 'a evar_map -> constr -> constr
 
-
 (*s Obsolete Reduction Functions *)
 
 val hnf : env -> 'a evar_map -> constr -> constr * constr list
 val apprec : 'a stack_reduction_function
 val red_product : 'a reduction_function
-val find_mrectype : 
-  env -> 'a evar_map -> constr -> constr * constr list
-val find_minductype : 
-  env -> 'a evar_map -> constr -> constr * constr list
-val find_mcoinductype : 
-  env -> 'a evar_map -> constr -> constr * constr list
-val check_mrectype_spec : env -> 'a evar_map -> constr -> constr
-val minductype_spec : env -> 'a evar_map -> constr -> constr
-val mrectype_spec : env -> 'a evar_map -> constr -> constr
+
+(* [find_m*type env sigma c] coerce [c] to an recursive type (I args).
+   [find_mrectype], [find_minductype] and [find_mcoinductype]
+   respectively accepts any recursive type, only an inductive type and
+   only a coinductive type.
+   They raise [Induc] if not convertible to a recursive type. *)
+
+exception Induc
+val find_mrectype     : env -> 'a evar_map -> constr -> inductive * constr list
+val find_minductype   : env -> 'a evar_map -> constr -> inductive * constr list
+val find_mcoinductype : env -> 'a evar_map -> constr -> inductive * constr list
+
+(* [try_mutind_of env sigma t] raises [Induc] if [t] is not an inductive type*)
+(* The resulting summary is relative to the current env *)
+val try_mutind_of : env -> 'a evar_map -> constr -> Inductive.inductive_summary
+
+
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 2c7829ef9..d7f8b8386 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -57,15 +57,14 @@ let rec execute mf env cstr =
         else 
 	  error "Cannot typecheck an unevaluable abstraction"
 	      
-    | IsConst _ ->
-        (make_judge cstr (type_of_constant env Evd.empty cstr), cst0)
+    | IsConst c ->
+        (make_judge cstr (type_of_constant env Evd.empty c), cst0)
 	  
-    | IsMutInd _ ->
-	(make_judge cstr (type_of_inductive env Evd.empty cstr), cst0)
+    | IsMutInd ind ->
+	(make_judge cstr (type_of_inductive env Evd.empty ind), cst0)
 	  
-    | IsMutConstruct (sp,i,j,args) -> 
-	let (typ,kind) =
-	  destCast (type_of_constructor env Evd.empty (((sp,i),j),args)) in
+    | IsMutConstruct c -> 
+	let (typ,kind) =destCast (type_of_constructor env Evd.empty c) in
         ({ uj_val = cstr; uj_type = typ; uj_kind = kind } , cst0)
 	  
     | IsMutCase (_,p,c,lf) ->
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 314796ee6..afa8d3ef9 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -44,7 +44,7 @@ val lookup_var : identifier -> safe_environment -> name * typed_type
 val lookup_rel : int -> safe_environment -> name * typed_type
 val lookup_constant : section_path -> safe_environment -> constant_body
 val lookup_mind : section_path -> safe_environment -> mutual_inductive_body
-val lookup_mind_specif : constr -> safe_environment -> mind_specif
+val lookup_mind_specif : inductive -> safe_environment -> mind_specif
 
 val export : safe_environment -> string -> compiled_env
 val import : compiled_env -> safe_environment -> safe_environment
diff --git a/kernel/term.ml b/kernel/term.ml
index f2e8d3422..56dd87f8f 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -32,7 +32,7 @@ type 'a oper =
       (* an extra slot, for putting in whatever sort of
          operator we need for whatever sort of application *)
 
-and case_info = inductive_path option
+and case_info = inductive_path
 
 (* Sorts. *)
 
@@ -148,7 +148,7 @@ let mkAppList a l = DOPN (AppL, Array.of_list (a::l))
 
 (* Constructs a constant *) 
 (* The array of terms correspond to the variables introduced in the section *)
-let mkConst sp a = DOPN (Const  sp, a)
+let mkConst (sp,a) = DOPN (Const  sp, a)
 
 (* Constructs an existential variable *)
 let mkEvar n a = DOPN (Evar n, a)
@@ -158,12 +158,12 @@ let mkAbst sp a = DOPN (Abst sp, a)
 
 (* Constructs the ith (co)inductive type of the block named sp *)
 (* The array of terms correspond to the variables introduced in the section *)
-let mkMutInd sp i l = (DOPN (MutInd (sp,i), l))
+let mkMutInd (ind_sp,l) = DOPN (MutInd ind_sp, l)
 
 (* Constructs the jth constructor of the ith (co)inductive type of the 
    block named sp. The array of terms correspond to the variables
    introduced in the section *)
-let mkMutConstruct sp i j l =  (DOPN ((MutConstruct ((sp,i),j),l))) 
+let mkMutConstruct (cstr_sp,l) =  DOPN (MutConstruct cstr_sp,l)
 
 (* Constructs the term <p>Case c of c1 | c2 .. | cn end *)
 let mkMutCase ci p c ac = 
@@ -439,24 +439,22 @@ let args_of_abst = function
 
 (* Destructs a (co)inductive type named sp *)
 let destMutInd = function
-  | DOPN (MutInd (sp,i), l) -> (sp,i,l)
+  | DOPN (MutInd ind_sp, l) -> (ind_sp,l)
   | _ -> invalid_arg "destMutInd"
 	
 let op_of_mind = function
-  | DOPN(MutInd (sp,i),_) -> (sp,i)
+  | DOPN(MutInd ind_sp,_) -> ind_sp
   | _ -> anomaly "op_of_mind called with bad args"
 
 let args_of_mind = function
   | DOPN(MutInd _,args) -> args
   | _ -> anomaly "args_of_mind called with bad args"
 
-let ci_of_mind = function
-  | DOPN(MutInd(sp,tyi),_) -> Some (sp,tyi)
-  | _ -> invalid_arg "ci_of_mind"
+let ci_of_mind = op_of_mind
 
 (* Destructs a constructor *)
 let destMutConstruct = function
-  | DOPN (MutConstruct ((sp,i),j),l) -> (sp,i,j,l)
+  | DOPN (MutConstruct cstr_sp,l) -> (cstr_sp,l)
   | _ -> invalid_arg "dest"
 
 let op_of_mconstr = function
@@ -528,6 +526,11 @@ let destUntypedCoFix = function
 (* Term analysis  *)
 (******************)
 
+type existential = int * constr array
+type constant = section_path * constr array
+type constructor = constructor_path * constr array
+type inductive = inductive_path * constr array
+
 type kindOfTerm = 
   | IsRel          of int
   | IsMeta         of int
@@ -538,11 +541,11 @@ type kindOfTerm =
   | IsProd         of name * constr * constr
   | IsLambda       of name * constr * constr
   | IsAppL         of constr * constr list
-  | IsConst        of section_path * constr array 
   | IsAbst         of section_path * constr array
-  | IsEvar         of int * constr array
-  | IsMutInd       of section_path * int * constr array 
-  | IsMutConstruct of section_path * int * int * constr array 
+  | IsEvar         of existential
+  | IsConst        of constant
+  | IsMutInd       of inductive
+  | IsMutConstruct of constructor
   | IsMutCase      of case_info * constr * constr * constr array
   | IsFix          of int array * int * constr array * name list * constr array
   | IsCoFix        of int * constr array * name list * constr array
@@ -569,8 +572,8 @@ let kind_of_term c =
     | DOPN (Const sp, a)                   -> IsConst (sp,a)
     | DOPN (Evar sp, a)                    -> IsEvar (sp,a)
     | DOPN (Abst sp, a)                    -> IsAbst (sp, a)
-    | DOPN (MutInd (sp,i), l)              -> IsMutInd (sp,i,l)
-    | DOPN (MutConstruct ((sp,i), j),l)    -> IsMutConstruct (sp,i,j,l)
+    | DOPN (MutInd ind_sp, l)              -> IsMutInd (ind_sp,l)
+    | DOPN (MutConstruct cstr_sp,l)        -> IsMutConstruct (cstr_sp,l)
     | DOPN (MutCase ci,v)                  -> 
 	IsMutCase (ci,v.(0),v.(1),Array.sub v 2 (Array.length v - 2))
     | DOPN ((Fix (recindxs,i),a))           ->  
@@ -1316,7 +1319,7 @@ module Hoper =
         | Abst sp -> Abst (hsp sp)
         | MutInd (sp,i) -> MutInd (hsp sp, i)
         | MutConstruct ((sp,i),j) -> MutConstruct ((hsp sp,i),j)
-        | MutCase(Some (sp,i)) -> MutCase(Some (hsp sp, i))
+        | MutCase(sp,i) -> MutCase(hsp sp, i)
         | t -> t 
       let equal o1 o2 =
         match (o1,o2) with
@@ -1327,7 +1330,7 @@ module Hoper =
           | (MutInd (sp1,i1), MutInd (sp2,i2)) -> sp1==sp2 & i1=i2
           | (MutConstruct((sp1,i1),j1), MutConstruct((sp2,i2),j2)) ->
               sp1==sp2 & i1=i2 & j1=j2
-          | (MutCase(Some (sp1,i1)),MutCase(Some (sp2,i2))) -> sp1==sp2 & i1=i2
+          | (MutCase(sp1,i1),MutCase(sp2,i2)) -> sp1==sp2 & i1=i2
           | _ -> o1=o2
       let hash = Hashtbl.hash
     end)
diff --git a/kernel/term.mli b/kernel/term.mli
index 2530c18e1..a7f2e6180 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -26,7 +26,7 @@ type 'a oper =
   | CoFix of int
   | XTRA of string
 
-and case_info = inductive_path option
+and case_info = inductive_path
 
 (*s The sorts of CCI. *)
 
@@ -73,6 +73,10 @@ val outcast_type : constr -> typed_type
   previous ones. *)
 
 (*  Concrete type for making pattern-matching. *)
+type existential = int * constr array
+type constant = section_path * constr array
+type constructor = constructor_path * constr array
+type inductive = inductive_path * constr array
 
 type kindOfTerm =
   | IsRel          of int
@@ -84,11 +88,11 @@ type kindOfTerm =
   | IsProd         of name * constr * constr
   | IsLambda       of name * constr * constr
   | IsAppL         of constr * constr list
-  | IsConst        of section_path * constr array
   | IsAbst         of section_path * constr array
-  | IsEvar         of int * constr array
-  | IsMutInd       of section_path * int * constr array
-  | IsMutConstruct of section_path * int * int * constr array
+  | IsEvar         of existential
+  | IsConst        of constant
+  | IsMutInd       of inductive
+  | IsMutConstruct of constructor
   | IsMutCase      of case_info * constr * constr * constr array
   | IsFix          of int array * int * constr array * name list * constr array
   | IsCoFix        of int * constr array * name list * constr array
@@ -158,7 +162,7 @@ val mkAppList : constr -> constr list  -> constr
 
 (* Constructs a constant *) 
 (* The array of terms correspond to the variables introduced in the section *)
-val mkConst : section_path -> constr array -> constr
+val mkConst : constant -> constr
 
 (* Constructs an existential variable *)
 val mkEvar : int -> constr array -> constr
@@ -168,12 +172,12 @@ val mkAbst : section_path -> constr array -> constr
 
 (* Constructs the ith (co)inductive type of the block named sp *)
 (* The array of terms correspond to the variables introduced in the section *)
-val mkMutInd : section_path -> int -> constr array -> constr
+val mkMutInd : inductive -> constr
 
 (* Constructs the jth constructor of the ith (co)inductive type of the 
    block named sp. The array of terms correspond to the variables
    introduced in the section *)
-val mkMutConstruct : section_path -> int -> int -> constr array -> constr
+val mkMutConstruct : constructor -> constr
 
 (* Constructs the term <p>Case c of c1 | c2 .. | cn end *)
 val mkMutCase : case_info -> constr -> constr -> constr list -> constr
@@ -291,13 +295,13 @@ val path_of_abst : constr -> section_path
 val args_of_abst : constr -> constr array
 
 (* Destructs a (co)inductive type *)
-val destMutInd : constr -> section_path * int * constr array
+val destMutInd : constr -> inductive
 val op_of_mind : constr -> inductive_path
 val args_of_mind : constr -> constr array
 val ci_of_mind : constr -> case_info
 
 (* Destructs a constructor *)
-val destMutConstruct : constr -> section_path * int * int * constr array
+val destMutConstruct : constr -> constructor
 val op_of_mconstr : constr -> constructor_path
 val args_of_mconstr : constr -> constr array
 
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 02db98b98..3cca1c694 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -33,7 +33,7 @@ type type_error =
   | NotClean of int * constr
   | VarNotFound of identifier
   (* Pattern-matching errors *)
-  | BadConstructor of constructor_path * inductive_path
+  | BadConstructor of constructor * inductive
   | WrongNumargConstructor of constructor_path * int
   | WrongPredicateArity of constr * int * int
   | NeedsInversion of constr * constr
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 1c0df5a31..66242b7cf 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -35,7 +35,7 @@ type type_error =
   | NotClean of int * constr
   | VarNotFound of identifier
   (* Pattern-matching errors *)
-  | BadConstructor of constructor_path * inductive_path
+  | BadConstructor of constructor * inductive
   | WrongNumargConstructor of constructor_path * int
   | WrongPredicateArity of constr * int * int
   | NeedsInversion of constr * constr
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 9fb263c59..1254d5ef9 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -81,8 +81,7 @@ let check_hyps id env sigma hyps =
 
 (* Instantiation of terms on real arguments. *)
 
-let type_of_constant env sigma c =
-  let (sp,args) = destConst c in
+let type_of_constant env sigma (sp,args) =
   let cb = lookup_constant sp env in
   let hyps = cb.const_hyps in
   check_hyps (basename sp) env sigma hyps;
@@ -110,8 +109,8 @@ let instantiate_lc mis =
   let lc = mis.mis_mip.mind_lc in
   instantiate_constr (ids_of_sign hyps) lc (Array.to_list mis.mis_args)
 
-let type_of_constructor env sigma ((ind_sp,j),args) =
-  let mind = DOPN (MutInd ind_sp, args) in
+let type_of_constructor env sigma ((ind_sp,j),args as cstr) =
+  let mind = inductive_of_constructor cstr in
   let mis = lookup_mind_specif mind env in
   check_hyps (basename mis.mis_sp) env sigma (mis.mis_mib.mind_hyps);
   let specif = instantiate_lc mis in
@@ -137,8 +136,7 @@ let mis_type_mconstructs mis =
    sAPPVList specif (list_tabulate make_ik ntypes))
 
 let type_mconstructs env sigma mind =
-  let redmind = check_mrectype_spec env sigma mind in
-  let mis = lookup_mind_specif redmind env in 
+  let mis = lookup_mind_specif mind env in 
   mis_type_mconstructs mis
 
 let mis_type_mconstruct i mispec =
@@ -150,21 +148,13 @@ let mis_type_mconstruct i mispec =
   sAPPViList (i-1) specif (list_tabulate make_Ik ntypes)
 
 let type_mconstruct env sigma i mind =
-  let redmind = check_mrectype_spec env sigma mind in
-  let (sp,tyi,args) = destMutInd redmind in
-  let mispec = lookup_mind_specif redmind env in 
-  mis_type_mconstruct i mispec
+  let mis = lookup_mind_specif mind env in
+  mis_type_mconstruct i mis
 
-let type_inst_construct env sigma i mind = 
-  try 
-    let (mI,largs) = find_mrectype env sigma mind in 
-    let mispec = lookup_mind_specif mI env in 
-    let nparams = mis_nparams mispec in 
-    let tc = mis_type_mconstruct i mispec in
-    let (globargs,_) = list_chop nparams largs in
+let type_inst_construct env sigma i (mind,globargs) =
+  let mis = lookup_mind_specif mind env in
+  let tc = mis_type_mconstruct i mis in
     hnf_prod_applist env sigma "Typing.type_construct" tc globargs
-  with Induc -> 
-    error_not_inductive CCI env mind
 
 let type_of_existential env sigma c =
   let (ev,args) = destEvar c in
@@ -262,7 +252,7 @@ let find_case_dep_nparams env sigma (c,p) (mind,largs) typP =
   and t = cast_instantiate_arity mis in 
   let (globargs,la) = list_chop nparams largs in
   let glob_t = hnf_prod_applist env sigma "find_elim_boolean" t globargs in
-  let arity = applist(mind,globargs) in
+  let arity = applist(mkMutInd mind,globargs) in
   let (dep,_) = is_correct_arity env sigma kelim (c,p) arity (typP,glob_t) in
   (dep, (nparams, globargs,la))
 
@@ -297,11 +287,12 @@ let type_one_branch_nodep env sigma (nparams,globargs,p) t =
 
 let type_case_branches env sigma ct pt p c =
   try
-    let ((mI,largs) as indt) = find_mrectype env sigma ct in
+    let (mind,largs) = find_mrectype env sigma ct in
     let (dep,(nparams,globargs,la)) =
-      find_case_dep_nparams env sigma (c,p) indt pt
+      find_case_dep_nparams env sigma (c,p) (mind,largs) pt
     in
-    let (lconstruct,ltypconstr) = type_mconstructs env sigma mI in
+    let (lconstruct,ltypconstr) = type_mconstructs env sigma mind in
+    let mI = mkMutInd mind in
     if dep then 
       (mI, 
        array_map2 (type_one_branch_dep env sigma (nparams,globargs,p))
@@ -502,8 +493,8 @@ let map_lift_fst = map_lift_fst_n 1
 
 let rec instantiate_recarg sp lrc ra = 
   match ra with 
-    | Mrec(j)        -> Imbr(sp,j,lrc)
-    | Imbr(sp1,k,l)  -> Imbr(sp1,k, List.map (instantiate_recarg sp lrc) l)
+    | Mrec(j)        -> Imbr((sp,j),lrc)
+    | Imbr(ind_sp,l) -> Imbr(ind_sp, List.map (instantiate_recarg sp lrc) l)
     | Norec          -> Norec
     | Param(k)       -> List.nth lrc k
 
@@ -520,10 +511,10 @@ let check_term env mind_recvec f =
       | (Mrec(i)::lr,DOP2(Lambda,_,DLAM(_,b)))  -> 
           let l' = map_lift_fst l in
           crec (n+1) ((1,mind_recvec.(i))::l') (lr,b)
-      | (Imbr(sp,i,lrc)::lr,DOP2(Lambda,_,DLAM(_,b))) -> 
+      | (Imbr((sp,i) as ind_sp,lrc)::lr,DOP2(Lambda,_,DLAM(_,b))) -> 
           let l' = map_lift_fst l in
           let sprecargs = 
-	    mis_recargs (lookup_mind_specif (mkMutInd sp i [||]) env) in
+	    mis_recargs (lookup_mind_specif (ind_sp,[||]) env) in
           let lc = 
 	    Array.map (List.map (instantiate_recarg sp lrc)) sprecargs.(i)
 	  in
@@ -618,11 +609,10 @@ let rec check_subterm_rec_meta env sigma vectn k def =
 	      error "Bad occurrence of recursive call"
         | _ -> error "Not enough abstractions in the definition") in
    let (c,d) = check_occur 1 def in 
-   let (mI, largs) = 
+   let ((sp,tyi),_ as mind, largs) = 
      (try find_minductype env sigma c 
       with Induc -> error "Recursive definition on a non inductive type") in
-   let (sp,tyi,_) = destMutInd mI in
-   let mind_recvec = mis_recargs (lookup_mind_specif mI env) in 
+   let mind_recvec = mis_recargs (lookup_mind_specif mind env) in 
    let lcx = mind_recvec.(tyi)  in
    (* n   = decreasing argument in the definition;
       lst = a mapping var |-> recargs
@@ -771,7 +761,8 @@ let check_fix env sigma = function
 (* Co-fixpoints. *)
 
 let mind_nparams env i =
-  let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams
+  let mis = lookup_mind_specif i env in
+  mis.mis_mib.mind_nparams
 
 let check_guard_rec_meta env sigma nbfix def deftype = 
   let rec codomain_is_coind c  =
@@ -781,11 +772,11 @@ let check_guard_rec_meta env sigma nbfix def deftype =
 	  (try find_mcoinductype env sigma b
            with 
 	     | Induc -> error "The codomain is not a coinductive type"
-	     | _ -> error "Type of Cofix function not as expected")
+(*	     | _ -> error "Type of Cofix function not as expected") ??? *) )
   in
-  let (mI, _) = codomain_is_coind deftype in
-  let (sp,tyi,_) = destMutInd mI in
-  let lvlra = (mis_recargs (lookup_mind_specif mI env)) in
+  let (mind, _) = codomain_is_coind deftype in
+  let ((sp,tyi),_) = mind in
+  let lvlra = (mis_recargs (lookup_mind_specif mind env)) in
   let vlra = lvlra.(tyi) in  
   let rec check_rec_call alreadygrd n vlra  t = 
     if noccur_with_meta n nbfix t then
@@ -807,9 +798,9 @@ let check_guard_rec_meta env sigma nbfix def deftype =
              else  
 	       error "check_guard_rec_meta: ???"
 		 
-	| (DOPN ((MutConstruct((x,y),i)),l), args)  ->
+	| (DOPN (MutConstruct(_,i as cstr_sp),l), args)  ->
             let lra =vlra.(i-1) in 
-            let mI = DOPN(MutInd(x,y),l) in
+            let mI = inductive_of_constructor (cstr_sp,l) in
             let _,realargs = list_chop (mind_nparams env mI) args in
             let rec process_args_of_constr l lra =
               match l with
@@ -825,9 +816,9 @@ let check_guard_rec_meta env sigma nbfix def deftype =
                             (check_rec_call true n newvlra t) &&
                             (process_args_of_constr lr lrar)
 			    
-                       |  (Imbr(sp,i,lrc)::lrar)  ->
+                       |  (Imbr((sp,i) as ind_sp,lrc)::lrar)  ->
 			    let mis =
-			      lookup_mind_specif (mkMutInd sp i [||]) env in
+			      lookup_mind_specif (ind_sp,[||]) env in
                             let sprecargs = mis_recargs mis in
                             let lc = (Array.map 
                                         (List.map 
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 55191e284..a7aec8cde 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -27,12 +27,11 @@ val assumption_of_judgment :
 
 val relative : env -> int -> unsafe_judgment
 
-val type_of_constant : env -> 'a evar_map -> constr -> typed_type
+val type_of_constant : env -> 'a evar_map -> constant -> typed_type
 
-val type_of_inductive : env -> 'a evar_map -> constr -> typed_type
+val type_of_inductive : env -> 'a evar_map -> inductive -> typed_type
 
-val type_of_constructor :
-  env -> 'a evar_map -> (constructor_path * constr array) -> constr
+val type_of_constructor : env -> 'a evar_map -> constructor -> constr
 
 val type_of_existential : env -> 'a evar_map -> constr -> constr
 
@@ -89,10 +88,12 @@ val make_arity_nodep :
 
 val find_case_dep_nparams :
   env -> 'a evar_map -> constr * constr ->
-    constr * constr list ->
+    inductive * constr list ->
       constr -> bool * (int * constr list * constr list) 
 
-val type_inst_construct : env -> 'a evar_map -> int -> constr -> constr 
+(* The constr list is the global args list *)
+val type_inst_construct :
+  env -> 'a evar_map -> int -> inductive * constr list -> constr 
 
 val hyps_inclusion : env -> 'a evar_map -> var_context -> var_context -> bool