Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 161 insertions, 204 deletions

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 88a0c2a6..1352b383 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -6,7 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indrec.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id$ *)
+
+(* File initially created by Christine Paulin, 1996 *)
+
+(* This file builds various inductive schemes *)
 
 open Pp
 open Util
@@ -15,6 +19,7 @@ open Libnames
 open Nameops
 open Term
 open Termops
+open Namegen
 open Declarations
 open Entries
 open Inductive
@@ -27,6 +32,8 @@ open Safe_typing
 open Nametab
 open Sign
 
+type dep_flag = bool
+
 (* Errors related to recursors building *)
 type recursion_scheme_error =
   | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * inductive
@@ -34,7 +41,7 @@ type recursion_scheme_error =
 
 exception RecursionSchemeError of recursion_scheme_error
 
-let make_prod_dep dep env = if dep then prod_name env else mkProd
+let make_prod_dep dep env = if dep then mkProd_name env else mkProd
 let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
 
 (*******************************************)
@@ -43,22 +50,16 @@ let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
 
 (**********************************************************************)
 (* Building case analysis schemes *)
-(* Nouvelle version, plus concise mais plus coûteuse à cause de
-   lift_constructor et lift_inductive_family qui ne se contentent pas de 
-   lifter les paramètres globaux *)
+(* Christine Paulin, 1996 *)
 
-let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind =
+let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
   let lnamespar = mib.mind_params_ctxt in
-  let dep = match depopt with 
-    | None -> inductive_sort_family mip <> InProp
-    | Some d -> d
-  in
   if not (List.mem kind (elim_sorts specif)) then
     raise
       (RecursionSchemeError
 	 (NotAllowedCaseAnalysis (false,new_sort_in_family kind,ind)));
 
-  let ndepar = mip.mind_nrealargs + 1 in
+  let ndepar = mip.mind_nrealargs_ctxt + 1 in
 
   (* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *)
   (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *)
@@ -67,7 +68,7 @@ let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind =
   let indf = make_ind_family(ind, extended_rel_list 0 lnamespar) in
   let constrs = get_constructors env indf in
 
-  let rec add_branch env k = 
+  let rec add_branch env k =
     if k = Array.length mip.mind_consnames then
       let nbprod = k+1 in
 
@@ -82,7 +83,7 @@ let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind =
           (mkRel (ndepar + nbprod),
            if dep then extended_rel_vect 0 deparsign
            else extended_rel_vect 1 arsign) in
-      let p = 
+      let p =
 	it_mkLambda_or_LetIn_name env'
 	  ((if dep then mkLambda_name env' else mkLambda)
 	   (Anonymous,depind,pbody))
@@ -100,27 +101,28 @@ let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind =
 	(add_branch (push_rel (Anonymous, None, t) env) (k+1))
   in
   let typP = make_arity env' dep indf (new_sort_in_family kind) in
-  it_mkLambda_or_LetIn_name env 
+  it_mkLambda_or_LetIn_name env
     (mkLambda_string "P" typP
        (add_branch (push_rel (Anonymous,None,typP) env') 0)) lnamespar
-    
+
 (* check if the type depends recursively on one of the inductive scheme *)
 
 (**********************************************************************)
 (* Building the recursive elimination *)
+(* Christine Paulin, 1996 *)
 
 (*
- * t is the type of the constructor co and recargs is the information on 
+ * t is the type of the constructor co and recargs is the information on
  * the recursive calls. (It is assumed to be in form given by the user).
  * build the type of the corresponding branch of the recurrence principle
- * assuming f has this type, branch_rec gives also the term 
- *   [x1]..[xk](f xi (F xi) ...) to be put in the corresponding branch of 
+ * assuming f has this type, branch_rec gives also the term
+ *   [x1]..[xk](f xi (F xi) ...) to be put in the corresponding branch of
  * the case operation
- * FPvect gives for each inductive definition if we want an elimination 
- * on it with which predicate and which recursive function. 
+ * FPvect gives for each inductive definition if we want an elimination
+ * on it with which predicate and which recursive function.
  *)
 
-let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = 
+let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
   let make_prod = make_prod_dep dep in
   let nparams = List.length vargs in
   let process_pos env depK pk =
@@ -136,39 +138,39 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
      	| Ind (_,_) ->
 	    let realargs = list_skipn nparams largs in
 	    let base = applist (lift i pk,realargs) in
-            if depK then 
+            if depK then
 	      Reduction.beta_appvect
                 base [|applist (mkRel (i+1),extended_rel_list 0 sign)|]
-            else 
+            else
 	      base
-      	| _ -> assert false 
+      	| _ -> assert false
     in
     prec env 0 []
   in
   let rec process_constr env i c recargs nhyps li =
-    if nhyps > 0 then match kind_of_term c with 
+    if nhyps > 0 then match kind_of_term c with
       | Prod (n,t,c_0) ->
-          let (optionpos,rest) = 
-	    match recargs with 
+          let (optionpos,rest) =
+	    match recargs with
 	      | [] -> None,[]
               | ra::rest ->
-                  (match dest_recarg ra with 
+                  (match dest_recarg ra with
 	            | Mrec j when is_rec -> (depPvect.(j),rest)
-	            | Imbr _  -> 
-		        Flags.if_verbose warning "Ignoring recursive call"; 
-		        (None,rest) 
+	            | Imbr _  ->
+		        Flags.if_verbose warning "Ignoring recursive call";
+		        (None,rest)
                     | _ -> (None, rest))
-	  in 
-          (match optionpos with 
-	     | None -> 
+	  in
+          (match optionpos with
+	     | None ->
 		 make_prod env
 		   (n,t,
 		    process_constr (push_rel (n,None,t) env) (i+1) c_0 rest
 		      (nhyps-1) (i::li))
-             | Some(dep',p) -> 
+             | Some(dep',p) ->
 		 let nP = lift (i+1+decP) p in
                  let env' = push_rel (n,None,t) env in
-		 let t_0 = process_pos env' dep' nP (lift 1 t) in 
+		 let t_0 = process_pos env' dep' nP (lift 1 t) in
 		 make_prod_dep (dep or dep') env
                    (n,t,
 		    mkArrow t_0
@@ -190,27 +192,27 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
       else c
   in
   let nhyps = List.length cs.cs_args in
-  let nP = match depPvect.(tyi) with 
+  let nP = match depPvect.(tyi) with
     | Some(_,p) -> lift (nhyps+decP) p
     | _ -> assert false in
   let base = appvect (nP,cs.cs_concl_realargs) in
   let c = it_mkProd_or_LetIn base cs.cs_args in
   process_constr env 0 c recargs nhyps []
 
-let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = 
+let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
   let process_pos env fk  =
     let rec prec env i hyps p =
       let p',largs = whd_betadeltaiota_nolet_stack env sigma p in
       match kind_of_term p' with
 	| Prod (n,t,c) ->
 	    let d = (n,None,t) in
-	    lambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c)
+	    mkLambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c)
 	| LetIn (n,b,t,c) ->
 	    let d = (n,Some b,t) in
 	    mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
-     	| Ind _ -> 
+     	| Ind _ ->
             let realargs = list_skipn nparrec largs
-            and arg = appvect (mkRel (i+1),extended_rel_vect 0 hyps) in 
+            and arg = appvect (mkRel (i+1),extended_rel_vect 0 hyps) in
             applist(lift i fk,realargs@[arg])
      	| _ -> assert false
     in
@@ -218,24 +220,24 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
   in
   (* ici, cstrprods est la liste des produits du constructeur instantié *)
   let rec process_constr env i f = function
-    | (n,None,t as d)::cprest, recarg::rest -> 
-        let optionpos = 
-	  match dest_recarg recarg with 
+    | (n,None,t as d)::cprest, recarg::rest ->
+        let optionpos =
+	  match dest_recarg recarg with
             | Norec   -> None
             | Imbr _  -> None
             | Mrec i  -> fvect.(i)
-	in 
-        (match optionpos with 
+	in
+        (match optionpos with
            | None ->
-	       lambda_name env
+	       mkLambda_name env
 		 (n,t,process_constr (push_rel d env) (i+1)
 		    (whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1)])))
 		    (cprest,rest))
-           | Some(_,f_0) -> 
+           | Some(_,f_0) ->
 	       let nF = lift (i+1+decF) f_0 in
                let env' = push_rel d env in
-	       let arg = process_pos env' nF (lift 1 t) in 
-               lambda_name env
+	       let arg = process_pos env' nF (lift 1 t) in
+               mkLambda_name env
 		 (n,t,process_constr env' (i+1)
 		    (whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1); arg])))
 		    (cprest,rest)))
@@ -251,9 +253,9 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
   process_constr env 0 f (List.rev cstr.cs_args, recargs)
 
 
-(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k 
+(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k
    variables *)
-let context_chop k ctx = 
+let context_chop k ctx =
   let rec chop_aux acc = function
     | (0, l2) -> (List.rev acc, l2)
     | (n, ((_,Some _,_ as h)::t)) -> chop_aux (h::acc) (n, t)
@@ -266,24 +268,24 @@ let context_chop k ctx =
 let mis_make_indrec env sigma listdepkind mib =
   let nparams = mib.mind_nparams in
   let nparrec = mib. mind_nparams_rec in
-  let lnonparrec,lnamesparrec = 
+  let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let nrec = List.length listdepkind in
   let depPvec =
-    Array.create mib.mind_ntypes (None : (bool * constr) option) in 
-  let _ = 
-    let rec 
-	assign k = function 
+    Array.create mib.mind_ntypes (None : (bool * constr) option) in
+  let _ =
+    let rec
+	assign k = function
 	  | [] -> ()
-          | (indi,mibi,mipi,dep,_)::rest -> 
+          | (indi,mibi,mipi,dep,_)::rest ->
               (Array.set depPvec (snd indi) (Some(dep,mkRel k));
                assign (k-1) rest)
-    in 
-      assign nrec listdepkind in 
+    in
+      assign nrec listdepkind in
   let recargsvec =
     Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in
   (* recarg information for non recursive parameters *)
-  let rec recargparn l n = 
+  let rec recargparn l n =
     if n = 0 then l else recargparn (mk_norec::l) (n-1) in
   let recargpar = recargparn [] (nparams-nparrec) in
   let make_one_rec p =
@@ -293,80 +295,80 @@ let mis_make_indrec env sigma listdepkind mib =
 	    let tyi = snd indi in
 	    let nctyi =
               Array.length mipi.mind_consnames in (* nb constructeurs du type*)
-	      
+
             (* arity in the context of the fixpoint, i.e.
                P1..P_nrec f1..f_nbconstruct *)
 	    let args = extended_rel_list (nrec+nbconstruct) lnamesparrec in
 	    let indf = make_ind_family(indi,args) in
-	      
+
 	    let arsign,_ = get_arity env indf in
 	    let depind = build_dependent_inductive env indf in
 	    let deparsign = (Anonymous,None,depind)::arsign in
-	      
+
 	    let nonrecpar = rel_context_length lnonparrec in
 	    let larsign = rel_context_length deparsign in
 	    let ndepar = larsign - nonrecpar in
 	    let dect = larsign+nrec+nbconstruct in
-	      
+
             (* constructors in context of the Cases expr, i.e.
                P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *)
 	    let args' = extended_rel_list (dect+nrec) lnamesparrec in
 	    let args'' = extended_rel_list ndepar lnonparrec in
             let indf' = make_ind_family(indi,args'@args'') in
-	      
-	    let branches = 
+
+	    let branches =
 	      let constrs = get_constructors env indf' in
 	      let fi = rel_vect (dect-i-nctyi) nctyi in
-	      let vecfi = Array.map 
+	      let vecfi = Array.map
 		(fun f -> appvect (f,extended_rel_vect ndepar lnonparrec))
-		fi 
+		fi
 	      in
 		array_map3
-		  (make_rec_branch_arg env sigma 
+		  (make_rec_branch_arg env sigma
 		      (nparrec,depPvec,larsign))
-                  vecfi constrs (dest_subterms recargsvec.(tyi)) 
+                  vecfi constrs (dest_subterms recargsvec.(tyi))
 	    in
-	      
-	    let j = (match depPvec.(tyi) with 
-	      | Some (_,c) when isRel c -> destRel c 
-	      | _ -> assert false) 
+
+	    let j = (match depPvec.(tyi) with
+	      | Some (_,c) when isRel c -> destRel c
+	      | _ -> assert false)
 	    in
-	      
+
 	    (* Predicate in the context of the case *)
-	      
+
 	    let depind' = build_dependent_inductive env indf' in
 	    let arsign',_ = get_arity env indf' in
 	    let deparsign' = (Anonymous,None,depind')::arsign' in
-	      
+
 	    let pargs =
-	      let nrpar = extended_rel_list (2*ndepar) lnonparrec 
+	      let nrpar = extended_rel_list (2*ndepar) lnonparrec
 	      and nrar = if dep then extended_rel_list 0 deparsign'
 		else extended_rel_list 1 arsign'
 	      in nrpar@nrar
-		
+
 	    in
 
 	    (* body of i-th component of the mutual fixpoint *)
-	    let deftyi = 
+	    let deftyi =
 	      let ci = make_case_info env indi RegularStyle in
-	      let concl = applist (mkRel (dect+j+ndepar),pargs) in 
+	      let concl = applist (mkRel (dect+j+ndepar),pargs) in
 	      let pred =
-		it_mkLambda_or_LetIn_name env 
+		it_mkLambda_or_LetIn_name env
 		  ((if dep then mkLambda_name env else mkLambda)
 		      (Anonymous,depind',concl))
 		  arsign'
 	      in
 		it_mkLambda_or_LetIn_name env
-		  (mkCase (ci, pred, 
+		  (mkCase (ci, pred,
 		          mkRel 1,
 			  branches))
 		  (lift_rel_context nrec deparsign)
 	    in
-	      
+
 	    (* type of i-th component of the mutual fixpoint *)
-	      
+
 	    let typtyi =
-	      let concl = 
+	      let concl =
 		let pargs = if dep then extended_rel_vect 0 deparsign
 		  else extended_rel_vect 1 arsign
 		in appvect (mkRel (nbconstruct+ndepar+nonrecpar+j),pargs)
@@ -374,25 +376,25 @@ let mis_make_indrec env sigma listdepkind mib =
 		concl
 		deparsign
 	    in
-	      mrec (i+nctyi) (rel_context_nhyps arsign ::ln) (typtyi::ltyp) 
+	      mrec (i+nctyi) (rel_context_nhyps arsign ::ln) (typtyi::ltyp)
                 (deftyi::ldef) rest
-        | [] -> 
+        | [] ->
 	    let fixn = Array.of_list (List.rev ln) in
             let fixtyi = Array.of_list (List.rev ltyp) in
-            let fixdef = Array.of_list (List.rev ldef) in 
+            let fixdef = Array.of_list (List.rev ldef) in
             let names = Array.create nrec (Name(id_of_string "F")) in
 	      mkFix ((fixn,p),(names,fixtyi,fixdef))
-      in 
-	mrec 0 [] [] [] 
-    in 
-    let rec make_branch env i = function 
+      in
+	mrec 0 [] [] []
+    in
+    let rec make_branch env i = function
       | (indi,mibi,mipi,dep,_)::rest ->
           let tyi = snd indi in
 	  let nconstr = Array.length mipi.mind_consnames in
-	  let rec onerec env j = 
-	    if j = nconstr then 
-	      make_branch env (i+j) rest 
-	    else 
+	  let rec onerec env j =
+	    if j = nconstr then
+	      make_branch env (i+j) rest
+	    else
 	      let recarg = (dest_subterms recargsvec.(tyi)).(j) in
 	      let recarg = recargpar@recarg in
 	      let vargs = extended_rel_list (nrec+i+j) lnamesparrec in
@@ -400,106 +402,107 @@ let mis_make_indrec env sigma listdepkind mib =
 	      let p_0 =
 		type_rec_branch
                   true dep env sigma (vargs,depPvec,i+j) tyi cs recarg
-	      in 
+	      in
 		mkLambda_string "f" p_0
 		  (onerec (push_rel (Anonymous,None,p_0) env) (j+1))
 	  in onerec env 0
-      | [] -> 
+      | [] ->
 	  makefix i listdepkind
     in
-    let rec put_arity env i = function 
-      | (indi,_,_,dep,kinds)::rest -> 
+    let rec put_arity env i = function
+      | (indi,_,_,dep,kinds)::rest ->
 	  let indf = make_ind_family (indi,extended_rel_list i lnamesparrec) in
 	  let typP = make_arity env dep indf (new_sort_in_family kinds) in
 	    mkLambda_string "P" typP
 	      (put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest)
-      | [] -> 
-	  make_branch env 0 listdepkind 
+      | [] ->
+	  make_branch env 0 listdepkind
     in
-      
+
     (* Body on make_one_rec *)
     let (indi,mibi,mipi,dep,kind) = List.nth listdepkind p in
-      
+
       if (mis_is_recursive_subset
 	(List.map (fun (indi,_,_,_,_) -> snd indi) listdepkind)
-	mipi.mind_recargs) 
-      then 
+	mipi.mind_recargs)
+      then
 	let env' = push_rel_context lnamesparrec env in
-	  it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) 
+	  it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind)
 	    lnamesparrec
-      else 
-	mis_make_case_com (Some dep) env sigma indi (mibi,mipi) kind 
-  in 
+      else
+	mis_make_case_com dep env sigma indi (mibi,mipi) kind
+  in
     (* Body of mis_make_indrec *)
     list_tabulate make_one_rec nrec
 
 (**********************************************************************)
 (* This builds elimination predicate for Case tactic *)
 
-let make_case_com depopt env sigma ity kind =
-  let (mib,mip) = lookup_mind_specif env ity in 
-    mis_make_case_com depopt env sigma ity (mib,mip) kind
+let build_case_analysis_scheme env sigma ity dep kind =
+  let (mib,mip) = lookup_mind_specif env ity in
+  mis_make_case_com dep env sigma ity (mib,mip) kind
 
-let make_case_dep env   = make_case_com (Some true) env
-let make_case_nodep env = make_case_com (Some false) env 
-let make_case_gen env   = make_case_com None env
+let build_case_analysis_scheme_default env sigma ity kind =
+  let (mib,mip) = lookup_mind_specif env ity in
+  let dep = inductive_sort_family mip <> InProp in
+  mis_make_case_com dep env sigma ity (mib,mip) kind
 
 
 (**********************************************************************)
-(* [instantiate_indrec_scheme s rec] replace the sort of the scheme
+(* [modify_sort_scheme s rec] replaces the sort of the scheme
    [rec] by [s] *)
 
-let change_sort_arity sort = 
+let change_sort_arity sort =
   let rec drec a = match kind_of_term a with
-    | Cast (c,_,_) -> drec c 
+    | Cast (c,_,_) -> drec c
     | Prod (n,t,c) -> mkProd (n, t, drec c)
     | LetIn (n,b,t,c) -> mkLetIn (n,b, t, drec c)
     | Sort _ -> mkSort sort
     | _ -> assert false
-  in 
-    drec 
+  in
+    drec
 
 (* [npar] is the number of expected arguments (then excluding letin's) *)
-let instantiate_indrec_scheme sort =
+let modify_sort_scheme sort =
   let rec drec npar elim =
     match kind_of_term elim with
-      | Lambda (n,t,c) -> 
-	  if npar = 0 then 
+      | Lambda (n,t,c) ->
+	  if npar = 0 then
 	    mkLambda (n, change_sort_arity sort t, c)
-	  else 
+	  else
 	    mkLambda (n, t, drec (npar-1) c)
       | LetIn (n,b,t,c) -> mkLetIn (n,b,t,drec npar c)
-      | _ -> anomaly "instantiate_indrec_scheme: wrong elimination type"
+      | _ -> anomaly "modify_sort_scheme: wrong elimination type"
   in
   drec
 
 (* Change the sort in the type of an inductive definition, builds the
    corresponding eta-expanded term *)
-let instantiate_type_indrec_scheme sort npars term =
+let weaken_sort_scheme sort npars term =
   let rec drec np elim =
     match kind_of_term elim with
-      | Prod (n,t,c) -> 
-	  if np = 0 then 
+      | Prod (n,t,c) ->
+	  if np = 0 then
             let t' = change_sort_arity sort t in
             mkProd (n, t', c),
             mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1)))
-	  else 
+	  else
             let c',term' = drec (np-1) c in
 	    mkProd (n, t, c'), mkLambda (n, t, term')
       | LetIn (n,b,t,c) -> let c',term' = drec np c in
-           mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term') 
-      | _ -> anomaly "instantiate_type_indrec_scheme: wrong elimination type"
+           mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term')
+      | _ -> anomaly "weaken_sort_scheme: wrong elimination type"
   in
   drec npars
 
 (**********************************************************************)
 (* Interface to build complex Scheme *)
-(* Check inductive types only occurs once 
+(* Check inductive types only occurs once
 (otherwise we obtain a meaning less scheme) *)
 
-let check_arities listdepkind = 
+let check_arities listdepkind =
   let _ = List.fold_left
-    (fun ln ((_,ni as mind),mibi,mipi,dep,kind) -> 
+    (fun ln ((_,ni as mind),mibi,mipi,dep,kind) ->
        let kelim = elim_sorts (mibi,mipi) in
        if not (List.exists ((=) kind) kelim) then raise
 	 (RecursionSchemeError
@@ -510,56 +513,29 @@ let check_arities listdepkind =
 	    [] listdepkind
   in true
 
-let build_mutual_indrec env sigma = function 
-  | (mind,mib,mip,dep,s)::lrecspec ->
+let build_mutual_induction_scheme env sigma = function
+  | (mind,dep,s)::lrecspec ->
+      let (mib,mip) = Global.lookup_inductive mind in
       let (sp,tyi) = mind in
-      let listdepkind = 
-    	(mind,mib,mip, dep,s)::
+      let listdepkind =
+	(mind,mib,mip,dep,s)::
     	(List.map
-	   (function (mind',mibi',mipi',dep',s') ->
+	   (function (mind',dep',s') ->
 	      let (sp',_) = mind' in
 	      if sp=sp' then
                 let (mibi',mipi') = lookup_mind_specif env mind' in
 		(mind',mibi',mipi',dep',s')
 	      else
-		  raise (RecursionSchemeError (NotMutualInScheme (mind,mind'))))
+		raise (RecursionSchemeError (NotMutualInScheme (mind,mind'))))
 	   lrecspec)
       in
-      let _ = check_arities listdepkind in 
+      let _ = check_arities listdepkind in
       mis_make_indrec env sigma listdepkind mib
-  | _ -> anomaly "build_indrec expects a non empty list of inductive types"
+  | _ -> anomaly "build_induction_scheme expects a non empty list of inductive types"
 
-let build_indrec env sigma ind =
+let build_induction_scheme env sigma ind dep kind =
   let (mib,mip) = lookup_mind_specif env ind in
-  let kind = inductive_sort_family mip in
-  let dep = kind <> InProp in
-    List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] mib)
-
-(**********************************************************************)
-(* To handle old Case/Match syntax in Pretyping                       *)
-
-(*****************************************)
-(* To interpret Case and Match operators *)
-(* Expects a dependent predicate *)
-
-let type_rec_branches recursive env sigma indt p c = 
-  let IndType (indf,realargs) = indt in
-  let (ind,params) = dest_ind_family indf in
-  let (mib,mip) = lookup_mind_specif env ind in
-  let recargs = mip.mind_recargs in
-  let tyi = snd ind in
-  let init_depPvec i = if i = tyi then Some(true,p) else None in
-  let depPvec = Array.init mib.mind_ntypes init_depPvec in
-  let constructors = get_constructors env indf in
-  let lft =
-    array_map2
-      (type_rec_branch recursive true env sigma (params,depPvec,0) tyi)
-      constructors (dest_subterms recargs) in
-  (lft,Reduction.beta_appvect p (Array.of_list (realargs@[c])))
-(* Non recursive case. Pb: does not deal with unification
-    let (p,ra,_) = type_case_branches env (ind,params@realargs) pj c in
-    (p,ra)
-*)
+  List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] mib)
 
 (*s Eliminations. *)
 
@@ -568,51 +544,32 @@ let elimination_suffix = function
   | InSet  -> "_rec"
   | InType -> "_rect"
 
+let case_suffix = "_case"
+
 let make_elimination_ident id s = add_suffix id (elimination_suffix s)
 
 (* Look up function for the default elimination constant *)
 
 let lookup_eliminator ind_sp s =
   let kn,i = ind_sp in
-  let mp,dp,l = repr_kn kn in
+  let mp,dp,l = repr_mind kn in
   let ind_id = (Global.lookup_mind kn).mind_packets.(i).mind_typename in
   let id = add_suffix ind_id (elimination_suffix s) in
   (* Try first to get an eliminator defined in the same section as the *)
   (* inductive type *)
-  let ref = ConstRef (make_con mp dp (label_of_id id)) in
-  try 
-    let _ = sp_of_global ref in
-    constr_of_global ref
+  try
+    let cst =Global.constant_of_delta
+      (make_con mp dp (label_of_id id)) in
+    let _ = Global.lookup_constant cst in
+      mkConst cst
   with Not_found ->
   (* Then try to get a user-defined eliminator in some other places *)
   (* using short name (e.g. for "eq_rec") *)
-  try constr_of_global (Nametab.locate (make_short_qualid id))
+  try constr_of_global (Nametab.locate (qualid_of_ident id))
   with Not_found ->
     errorlabstrm "default_elim"
       (strbrk "Cannot find the elimination combinator " ++
        pr_id id ++ strbrk ", the elimination of the inductive definition " ++
-       pr_global_env Idset.empty (IndRef ind_sp) ++ 
+       pr_global_env Idset.empty (IndRef ind_sp) ++
        strbrk " on sort " ++ pr_sort_family s ++
        strbrk " is probably not allowed.")
-
-
-(*  let env = Global.env() in
-  let path = sp_of_global None (IndRef ind_sp) in
-  let dir, base = repr_path path in
-  let id = add_suffix base (elimination_suffix s) in
-  (* Try first to get an eliminator defined in the same section as the *)
-  (* inductive type *)
-  try construct_absolute_reference (Names.make_path dir id)
-  with Not_found ->
-  (* Then try to get a user-defined eliminator in some other places *)
-  (* using short name (e.g. for "eq_rec") *)
-    try constr_of_global (Nametab.locate (make_short_qualid id))
-    with Not_found ->
-      errorlabstrm "default_elim"
-	(str "Cannot find the elimination combinator " ++
-           pr_id id ++ spc () ++
-	   str "The elimination of the inductive definition " ++
-           pr_id base ++ spc () ++ str "on sort " ++ 
-           spc () ++ pr_sort_family s ++
-	   str " is probably not allowed")
-*)