Nouvelle mouture du traducteur v7->v8

Option -v8 à coqtop lance coqtopnew
Le terminateur reste "." en v8
Ajout construction primitive CLetTuple/RLetTuple
Introduction typage dans le traducteur pour traduire les Case/Cases/Match
Ajout mutables dans RCases or ROrderedCase pour permettre la traduction
Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts
+ Bugs ou améliorations diverses
Raffinement affichage projections de Record/Structure.


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

10 files changed, 584 insertions, 72 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c24748970d..e2aa74cba5 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -591,11 +591,15 @@ let occur_rawconstr id =
     | RLambda (loc,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
     | RProd (loc,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
     | RLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c))
-    | RCases (loc,tyopt,tml,pl) ->
-	(occur_option tyopt) or (List.exists occur tml)
+    | RCases (loc,(tyopt,rtntypopt),tml,pl) ->
+	(occur_option tyopt) or (occur_option !rtntypopt)
+        or (List.exists (fun (tm,_) -> occur tm) tml)
 	or (List.exists occur_pattern pl)
-    | ROrderedCase (loc,b,tyopt,tm,bv) -> 
+    | ROrderedCase (loc,b,tyopt,tm,bv,_) -> 
 	(occur_option tyopt) or (occur tm) or (array_exists occur bv)
+    | RLetTuple (loc,nal,(na,tyopt),b,c) -> 
+	(na <> Name id & occur_option tyopt)
+        or (occur b) or (not (List.mem (Name id) nal) & (occur c))
     | RRec (loc,fk,idl,tyl,bv) ->
 	(array_exists occur tyl) or
 	(not (array_exists (fun id2 -> id=id2) idl) & array_exists occur bv)
@@ -1546,6 +1550,45 @@ let extract_predicate_conclusion nargs pred =
       | _ -> (* eta-expansion *) applist (lift 1 p, [mkRel 1]) in
   iterate decomp_lam_force nargs pred
 
+let set_arity_signature dep n arsign tomatchl pred x =
+  (* avoid is not exhaustive ! *)
+  let rec decomp_lam_force n avoid l p =
+    if n = 0 then (List.rev l,p,avoid) else
+    match p with
+      | RLambda (_,(Name id as na),_,c) -> 
+          decomp_lam_force (n-1) (id::avoid) (na::l) c
+      | RLambda (_,(Anonymous as na),_,c) -> decomp_lam_force (n-1) avoid (na::l) c
+      | _ ->
+          let x = next_ident_away (id_of_string "x") avoid in
+          decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
+          (* eta-expansion *)
+            (let a = RVar (dummy_loc,x) in
+             match p with
+               | RApp (loc,p,l) -> RApp (loc,p,l@[a])
+               | _ -> (RApp (dummy_loc,p,[a]))) in
+  let rec decomp_block avoid p = function
+    | ([], _) -> x := Some p
+    | ((_,IsInd (_,IndType(indf,realargs)))::l),(y::l')  ->
+	let (ind,params) = dest_ind_family indf in
+        let (nal,p,avoid') = decomp_lam_force (List.length realargs) avoid [] p 
+        in
+        let na,p,avoid' = 
+          if dep then decomp_lam_force 1 avoid' [] p else [Anonymous],p,avoid'
+        in 
+        y :=
+        (List.hd na,
+         if List.for_all ((=) Anonymous) nal then
+           None
+         else
+           Some (dummy_loc, ind, (List.map (fun _ -> Anonymous) params)@nal));
+        decomp_block avoid' p (l,l')
+    | (_::l),(y::l') ->
+        y := (Anonymous,None);
+        decomp_block avoid p (l,l')
+    | _ -> anomaly "set_arity_signature"
+  in
+  decomp_block [] pred (tomatchl,arsign)
+
 let prepare_predicate_from_tycon loc dep env isevars tomatchs c =
   let cook (n, l, env) = function
     | c,IsInd (_,IndType(indf,realargs)) ->
@@ -1571,7 +1614,7 @@ let prepare_predicate_from_tycon loc dep env isevars tomatchs c =
       map_constr_with_full_binders push_rel build_skeleton env c in
   build_skeleton env (lift n c)
   
-(* Here, [pred] is assumed to be in the context build from all *)
+(* Here, [pred] is assumed to be in the context built from all *)
 (* realargs and terms to match *)
 let build_initial_predicate env sigma isdep pred tomatchl =
   let cook n = function
@@ -1595,6 +1638,45 @@ let build_initial_predicate env sigma isdep pred tomatchl =
 		PrLetIn ((realargs,None), buildrec (n+nrealargs) q ltm)
   in buildrec 0 0 tomatchl
 
+let extract_arity_signature env0 tomatchl tmsign =
+  let get_one_sign n tm {contents = (na,t)} =
+    match tm with
+      | NotInd _ -> 
+	  (match t with
+	    | None -> []
+	    | Some (loc,_,_) -> 
+ 	    user_err_loc (loc,"",
+	    str "Unexpected type annotation for a term of non inductive type"))
+      | IsInd (_,IndType(indf,realargs)) ->
+          let indf' = lift_inductive_family n indf in
+	  let (ind,params) = dest_ind_family indf' in
+	  let nrealargs = List.length realargs in
+	  let realnal =
+	    match t with
+	      | Some (loc,ind',nal) ->
+		  let nparams = List.length params in
+		  if ind <> ind' then
+		    user_err_loc (loc,"",str "Wrong inductive type");
+		  if List.length nal <> nparams + nrealargs then
+		    user_err_loc (loc,"",
+		    str "Wrong number of arguments for inductive type");
+		  let parnal,realnal = list_chop nparams nal in
+		  if List.exists ((<>) Anonymous) parnal then
+		    user_err_loc (loc,"",
+		    str "The parameters of inductive type must be implicit");
+		  List.rev realnal
+	      | None -> list_tabulate (fun _ -> Anonymous) nrealargs in
+	  let arsign = fst (get_arity env0 indf') in
+	  (na,None,build_dependent_inductive env0 indf')
+	  ::(List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign) in
+  let rec buildrec n = function
+    | [],[] -> []
+    | (_,tm)::ltm, x::tmsign ->
+	let l = get_one_sign n tm x in
+	(buildrec (n + List.length l) (ltm,tmsign)) @ l
+    | _ -> assert false
+  in buildrec 0 (tomatchl,tmsign)
+
 (* determines wether the multiple case is dependent or not. For that
  * the predicate given by the user is eta-expanded. If the result
  * of expansion is pred, then :
@@ -1606,15 +1688,28 @@ let build_initial_predicate env sigma isdep pred tomatchl =
  *        else error! (can not treat mixed dependent and non dependent case
  *)
 
-let prepare_predicate loc typing_fun isevars env tomatchs tycon = function
-  | None ->
+let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
+  (* No type annotation at all *)
+  | (None,{contents = None}) ->
       (match tycon with
        | None -> None
        | Some t ->
 	 let pred = prepare_predicate_from_tycon loc false env isevars tomatchs t in
 	 Some
 	  (build_initial_predicate env (evars_of isevars) false pred tomatchs))
-  | Some pred ->
+
+  (* v8 style type annotation *)
+  | (None,{contents = Some rtntyp}) ->
+
+      (* We extract the signature of the arity *)
+      let arsign = extract_arity_signature env tomatchs sign in
+      let env = push_rels arsign env in
+      let predccl = (typing_fun empty_tycon env rtntyp).uj_val in
+      Some
+        (build_initial_predicate env (evars_of isevars) true predccl tomatchs)
+
+  (* v7 style type annotation; set the v8 annotation by side effect *)
+  | (Some pred,x) ->
       let loc = loc_of_rawconstr pred in
       let dep, n, predj =
 	let isevars_copy = evars_of isevars in
@@ -1643,6 +1738,7 @@ let prepare_predicate loc typing_fun isevars env tomatchs tycon = function
 (*
       let etapred,cdep = case_dependent env (evars_of isevars) loc predj tomatchs in
 *)
+      set_arity_signature dep n sign tomatchs pred x;
       Some(build_initial_predicate env (evars_of isevars) dep predccl tomatchs)
 
 
@@ -1656,11 +1752,12 @@ let compile_cases loc (typing_fun,isevars) tycon env (predopt, tomatchl, eqns)=
 
   (* We build the vector of terms to match consistently with the *)
   (* constructors found in patterns *)
-  let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in
+  let rawtms, tmsign = List.split tomatchl in
+  let tomatchs = coerce_to_indtype typing_fun isevars env matx rawtms in
 
   (* We build the elimination predicate if any and check its consistency *)
   (* with the type of arguments to match *)
-  let pred = prepare_predicate loc typing_fun isevars env tomatchs tycon predopt in
+  let pred = prepare_predicate loc typing_fun isevars env tomatchs tmsign tycon predopt in
 
   (* We deal with initial aliases *)
   let matx = prepare_initial_aliases (known_dependent pred) tomatchs matx in 
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 287e78f76a..1c4e6b92cd 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -41,6 +41,8 @@ type ml_case_error =
 
 exception NotInferable of ml_case_error
 
+val occur_rawconstr : identifier -> rawconstr -> bool
+
 val pred_case_ml : (* raises [NotInferable] if not inferable *)
   env -> evar_map -> bool -> inductive_type -> int * types -> constr 
 
@@ -49,6 +51,7 @@ val pred_case_ml : (* raises [NotInferable] if not inferable *)
 val compile_cases :
   loc -> (type_constraint -> env -> rawconstr -> unsafe_judgment)
   * evar_defs -> type_constraint -> env ->
-    rawconstr option * rawconstr list *
+      (rawconstr option * rawconstr option ref) *
+      (rawconstr * (name * (loc * inductive * name list) option) ref) list *
     (loc * identifier list * cases_pattern list * rawconstr) list ->
     unsafe_judgment
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 9e4eaf8a1c..a82b2b90ae 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -162,7 +162,6 @@ let computable p k =
   noccur_between 1 (k+1) ccl
 
 
-
 let lookup_name_as_renamed env t s =
   let rec lookup avoid env_names n c = match kind_of_term c with
     | Prod (name,_,c') ->
@@ -195,7 +194,7 @@ let lookup_index_as_renamed env t n =
     | _ -> None
   in lookup n 1 t
 
-let detype_case computable detype detype_eqn tenv avoid env indsp st p c bl =
+let detype_case computable detype detype_eqn tenv avoid env indsp st p k c bl =
   let synth_type = synthetize_type () in
   let tomatch = detype tenv avoid env c in
 
@@ -207,11 +206,41 @@ let detype_case computable detype detype_eqn tenv avoid env indsp st p c bl =
     List.rev (fst (decompose_prod_assum t)) in
   let consnargs = Array.init (Array.length mip.mind_consnames) get_consnarg in
   let consnargsl = Array.map List.length consnargs in
-  let pred = 
+  let alias, aliastyp, newpred, pred = 
     if synth_type & computable & bl <> [||] then
-      None
-    else 
-      option_app (detype tenv avoid env) p in
+      Anonymous, None, None, None
+    else
+      let p = option_app (detype tenv avoid env) p in
+      match p with
+        | None -> Anonymous, None, None, None
+        | Some p ->
+            let decompose_lam k c =
+              let name_cons = function
+                  Anonymous -> fun l -> l | Name id -> fun l -> id::l in
+              let rec lamdec_rec l avoid k c =
+                if k = 0 then l,c else match c with
+                  | RLambda (_,x,t,c) -> 
+                      lamdec_rec (x::l) (name_cons x avoid) (k-1) c
+                  | c -> 
+                      let x = next_ident_away (id_of_string "xx") avoid in
+                      lamdec_rec ((Name x)::l) (x::avoid) (k-1)
+                        (let a = RVar (dummy_loc,x) in
+                          match c with
+                          | RApp (loc,p,l) -> RApp (loc,p,l@[a])
+                          | _ -> (RApp (dummy_loc,c,[a])))
+              in 
+              lamdec_rec [] [] k c in
+            let nl,typ = decompose_lam k p in
+	    let n,typ = match typ with 
+              | RLambda (_,x,t,c) -> x, c
+	      | _ -> Anonymous, typ in
+	    let aliastyp =
+	      if List.for_all ((=) Anonymous) nl then None
+	      else 
+		let pars = list_tabulate (fun _ -> Anonymous) mip.mind_nparams
+		in Some (dummy_loc,indsp,pars@nl) in
+            n, aliastyp, Some typ, Some p
+  in
   let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
   let eqnv = array_map3 (detype_eqn tenv avoid env) constructs consnargsl bl in
   let eqnl = Array.to_list eqnv in
@@ -226,29 +255,48 @@ let detype_case computable detype detype_eqn tenv avoid env indsp st p c bl =
     with Not_found -> st
   in 
   if tag = RegularStyle then
-    RCases (dummy_loc,pred,[tomatch],eqnl)
+    RCases (dummy_loc,(pred,ref newpred),[tomatch,ref (alias,aliastyp)],eqnl)
   else
-    let rec remove_type avoid args c =
-      match c,args with
-        | RLambda (loc,na,t,c), _::args ->
-            let h = RHole (loc,BinderType na) in
-            RLambda (loc,na,h,remove_type avoid args c)
-        | RLetIn (loc,na,b,c), _::args ->
-            RLetIn (loc,na,b,remove_type avoid args c)
-        | c, (na,None,t)::args ->
-            let id = next_name_away_with_default "x" na avoid in
-            let h = RHole (dummy_loc,BinderType na) in
-            let c = remove_type (id::avoid) args
-              (RApp (dummy_loc,c,[RVar (dummy_loc,id)])) in
-            RLambda (dummy_loc,Name id,h,c)
-        | c, (na,Some b,t)::args ->
-            let h = RHole (dummy_loc,BinderType na) in
-            let avoid = name_fold (fun x l -> x::l) na avoid in
-            RLetIn (dummy_loc,na,h,remove_type avoid args c)
-        | c, [] -> c in
     let bl = Array.map (detype tenv avoid env) bl in
-    let bl = array_map2 (remove_type avoid) consnargs bl in
-    ROrderedCase (dummy_loc,tag,pred,tomatch,bl)
+    if not !Options.v7 && tag = LetStyle && aliastyp = None then
+      let rec decomp_lam_force n avoid l p =
+	if n = 0 then (List.rev l,p) else
+          match p with
+            | RLambda (_,(Name id as na),_,c) -> 
+		decomp_lam_force (n-1) (id::avoid) (na::l) c
+            | RLambda (_,(Anonymous as na),_,c) -> 
+		decomp_lam_force (n-1) avoid (na::l) c
+            | _ ->
+		let x = Nameops.next_ident_away (id_of_string "x") avoid in
+		decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
+                  (* eta-expansion *)
+                  (let a = RVar (dummy_loc,x) in
+                  match p with
+                    | RApp (loc,p,l) -> RApp (loc,p,l@[a])
+                    | _ -> (RApp (dummy_loc,p,[a]))) in
+      let (nal,d) = decomp_lam_force consnargsl.(0) avoid [] bl.(0) in
+      RLetTuple (dummy_loc,nal,(alias,newpred),tomatch,d)
+    else
+      let rec remove_type avoid args c =
+	match c,args with
+          | RLambda (loc,na,t,c), _::args ->
+              let h = RHole (dummy_loc,BinderType na) in
+              RLambda (loc,na,h,remove_type avoid args c)
+          | RLetIn (loc,na,b,c), _::args ->
+              RLetIn (loc,na,b,remove_type avoid args c)
+          | c, (na,None,t)::args ->
+              let id = next_name_away_with_default "x" na avoid in
+              let h = RHole (dummy_loc,BinderType na) in
+              let c = remove_type (id::avoid) args
+		(RApp (dummy_loc,c,[RVar (dummy_loc,id)])) in
+              RLambda (dummy_loc,Name id,h,c)
+          | c, (na,Some b,t)::args ->
+              let h = RHole (dummy_loc,BinderType na) in
+              let avoid = name_fold (fun x l -> x::l) na avoid in
+              RLetIn (dummy_loc,na,h,remove_type avoid args c)
+          | c, [] -> c in
+      let bl = array_map2 (remove_type avoid) consnargs bl in
+      ROrderedCase (dummy_loc,tag,pred,tomatch,bl,ref None)
 
 let rec detype tenv avoid env t =
   match kind_of_term (collapse_appl t) with
@@ -291,8 +339,8 @@ let rec detype tenv avoid env t =
 	let comp = computable p (annot.ci_pp_info.ind_nargs) in
 	let ind = annot.ci_ind in
 	let st = annot.ci_pp_info.style in
-	detype_case comp detype detype_eqn tenv avoid env ind st (Some p) c bl
-	
+	detype_case comp detype detype_eqn tenv avoid env ind st (Some p)
+          annot.ci_pp_info.ind_nargs c bl
     | Fix (nvn,recdef) -> detype_fix tenv avoid env nvn recdef
     | CoFix (n,recdef) -> detype_cofix tenv avoid env n recdef
 
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 13d37c8436..5cf174875a 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -29,7 +29,7 @@ val detype_case :
     'a -> Rawterm.loc * Names.identifier list * Rawterm.cases_pattern list *
     Rawterm.rawconstr) ->
     env -> identifier list -> names_context -> inductive -> case_style ->
-      'a option -> 'a -> 'a array -> rawconstr
+      'a option -> int -> 'a -> 'a array -> rawconstr
 
 (* look for the index of a named var or a nondep var as it is renamed *)
 val lookup_name_as_renamed  : env -> constr -> identifier -> int option
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 161c37ae80..ca25938b6c 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -69,14 +69,20 @@ let mis_make_case_com depopt env sigma (ind,mib,mip) kind =
       let indf = make_ind_family(ind,extended_rel_list nbprod lnamespar) in
       let lnamesar,_ = get_arity env indf in
       let ci = make_default_case_info env RegularStyle ind in
+      let depind = build_dependent_inductive env indf in
+      let deparsign = (Anonymous,None,depind)::lnamesar in
+      let p = (* mkRel nbprod *)
       it_mkLambda_or_LetIn_name env'
-       	(lambda_create env'
-           (build_dependent_inductive env indf,
-            mkCase (ci,
-		       mkRel (nbprod+nbargsprod),
-		       mkRel 1,
-		       rel_vect nbargsprod k)))
-       	lnamesar
+          (appvect
+            (mkRel ((if dep then nbargsprod else mip.mind_nrealargs) + nbprod),
+            if dep then extended_rel_vect 0 deparsign
+            else extended_rel_vect 0 lnamesar))
+          (if dep then deparsign else lnamesar) in
+      it_mkLambda_or_LetIn_name env'
+       	(mkCase (ci, lift nbargsprod p,
+		     mkRel 1,
+		     rel_vect nbargsprod k))
+       	deparsign
     else
       let cs = lift_constructor (k+1) constrs.(k) in
       let t = build_branch_type env dep (mkRel (k+1)) cs in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index a64c553899..adc5932f18 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -239,6 +239,28 @@ let find_coinductive env sigma c =
 (* find appropriate names for pattern variables. Useful in the
    Case tactic. *)
 
+let is_dep_predicate env kelim pred nodep_ar = 
+  let rec srec env pval pt nodep_ar =
+    let pt' = whd_betadeltaiota env Evd.empty pt in
+    let pv' = whd_betadeltaiota env Evd.empty pval in
+    match kind_of_term pv', kind_of_term pt', kind_of_term nodep_ar with
+      | Lambda (na,t,b), Prod (_,_,a), Prod (_,_,a') ->
+	  srec (push_rel_assum (na,t) env) b a a'
+      | _,              Prod (na,t,a), Prod (_,_,a') ->
+	  srec (push_rel_assum (na,t) env) (lift 1 pv') a a'
+      | Lambda (_,_,b), Prod (_,_,_), _ -> (*dependent (mkRel 1) b*) true
+      | _, Prod (_,_,_), _ -> true
+      | _ -> false in 
+  srec env pred.uj_val pred.uj_type nodep_ar
+
+let is_dependent_elimination_predicate env pred indf =
+  let (ind,params) = indf in
+  let (_,mip) = Inductive.lookup_mind_specif env ind in
+  let kelim = mip.mind_kelim in
+  let arsign,s = get_arity env indf in
+  let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in
+  is_dep_predicate env kelim pred glob_t
+
 let is_dep_arity env kelim predty nodep_ar = 
   let rec srec pt nodep_ar =
     let pt' = whd_betadeltaiota env Evd.empty pt in
@@ -256,7 +278,6 @@ let is_dependent_elimination env predty indf =
   let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in
   is_dep_arity env kelim predty glob_t
 
-
 let set_names env n brty =
   let (ctxt,cl) = decompose_prod_n_assum n brty in
   it_mkProd_or_LetIn_name env cl ctxt
@@ -277,7 +298,7 @@ let type_case_branches_with_names env indspec pj c =
   let (lbrty,conclty,_) = Inductive.type_case_branches env indspec pj c in
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let params = list_firstn mip.mind_nparams args in
-  if is_dependent_elimination env pj.uj_type (ind,params) then
+  if is_dependent_elimination_predicate env pj (ind,params) then
     (set_pattern_names env ind lbrty, conclty)
   else (lbrty, conclty)
 
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 92c581c719..d3479a8466 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -237,15 +237,16 @@ let rec pat_of_raw metas vars = function
       Options.if_verbose
         Pp.warning "Cast not taken into account in constr pattern";
       pat_of_raw metas vars c
-  | ROrderedCase (_,st,po,c,br) ->
+  | ROrderedCase (_,st,po,c,br,_) ->
       PCase ((None,st),option_app (pat_of_raw metas vars) po,
              pat_of_raw metas vars c,
              Array.map (pat_of_raw metas vars) br)
-  | RCases (loc,po,[c],brs) ->
+  | RCases (loc,(po,_),[c,_],brs) ->
       let sp =
 	match brs with
 	  | (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind
 	  | _ -> None in
+      (* When po disappears: switch to rtn type *)
       PCase ((sp,Term.RegularStyle),option_app (pat_of_raw metas vars) po,
              pat_of_raw metas vars c,
              Array.init (List.length brs)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0b665d4b29..e86d60c77a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -50,7 +50,7 @@ let transform_rec loc env sigma (pj,c,lf) indt =
   let (mib,mip) = lookup_mind_specif env ind in
   let recargs = mip.mind_recargs in
   let mI = mkInd ind in
-  let ci = make_default_case_info env MatchStyle ind in
+  let ci = make_default_case_info env (if Options.do_translate() then RegularStyle else MatchStyle) ind in
   let nconstr = Array.length mip.mind_consnames in
   if Array.length lf <> nconstr then 
     (let cj = {uj_val=c; uj_type=mkAppliedInd indt} in
@@ -146,6 +146,8 @@ let inh_conv_coerce_to_tycon loc env isevars j = function
    | None -> j
    | Some typ -> inh_conv_coerce_to loc env isevars j typ
 
+let push_rels vars env = List.fold_right push_rel vars env
+
 (*
 let evar_type_case isevars env ct pt lft p c =
   let (mind,bty,rslty) = type_case_branches env (evars_of isevars) ct pt p c
@@ -330,8 +332,7 @@ let rec pretype tycon env isevars lvar = function
       { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
 	uj_type = type_app (subst1 j.uj_val) j'.uj_type }
 
-  (* Special Case for let constructions to avoid exponential behavior *)      
-  | ROrderedCase (loc,st,po,c,[|f|]) when st <> MatchStyle ->
+  | RLetTuple (loc,nal,(na,po),c,d) ->
       let cj = pretype empty_tycon env isevars lvar c in
       let (IndType (indf,realargs) as indt) = 
 	try find_rectype env (evars_of isevars) cj.uj_type
@@ -339,8 +340,67 @@ let rec pretype tycon env isevars lvar = function
 	  let cloc = loc_of_rawconstr c in
 	  error_case_not_inductive_loc cloc env (evars_of isevars) cj 
       in
+      let cstrs = get_constructors env indf in
+      if Array.length cstrs <> 1 then
+        user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor");
+      let cs = cstrs.(0) in
+      if List.length nal <> cs.cs_nargs then
+        user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables");
+      let fsign = List.map2 (fun na (_,c,t) -> (na,c,t))
+        (List.rev nal) cs.cs_args in
+      let env_f = push_rels fsign env in
+      let arsgn,_ = get_arity env indf in
+      let psign = (na,None,build_dependent_inductive env indf)::arsgn in
+      let nar = List.length arsgn in
       (match po with
 	 | Some p ->
+             let env_p = push_rels psign env in
+             let pj = pretype_type empty_valcon env_p isevars lvar p in
+             let ccl = nf_evar (evars_of isevars) pj.utj_val in
+             let fty =
+               let inst = (Array.to_list cs.cs_concl_realargs)
+                 @[build_dependent_constructor cs]
+               in substl inst (liftn cs.cs_nargs nar ccl) in
+	     let fj = pretype (mk_tycon fty) env_f isevars lvar d in
+	     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
+	     let p = it_mkLambda_or_LetIn ccl psign in
+	     let v =
+	       let mis,_ = dest_ind_family indf in
+	       let ci = make_default_case_info env LetStyle mis in
+	       mkCase (ci, p, cj.uj_val,[|f|]) in 
+             let cs = build_dependent_constructor cs in
+	     { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
+
+	 | None -> 
+             let tycon = option_app (lift cs.cs_nargs) tycon in
+	     let fj = pretype tycon env_f isevars lvar d in
+	     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
+	     let ccl = nf_evar (evars_of isevars) fj.uj_type in
+             let ccl =
+               if noccur_between 1 cs.cs_nargs ccl then
+                 lift (- cs.cs_nargs) ccl 
+               else
+                 error_cant_find_case_type_loc loc env (evars_of isevars) 
+                   cj.uj_val in
+             let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
+	     let v =
+	       let mis,_ = dest_ind_family indf in
+	       let ci = make_default_case_info env LetStyle mis in
+	       mkCase (ci, p, cj.uj_val,[|f|] ) 
+	     in
+	     { uj_val = v; uj_type = ccl })
+
+  (* Special Case for let constructions to avoid exponential behavior *)      
+  | ROrderedCase (loc,st,po,c,[|f|],xx) when st <> MatchStyle ->
+      let cj = pretype empty_tycon env isevars lvar c in
+      let (IndType (indf,realargs) as indt) = 
+	try find_rectype env (evars_of isevars) cj.uj_type
+	with Not_found ->
+	  let cloc = loc_of_rawconstr c in
+	  error_case_not_inductive_loc cloc env (evars_of isevars) cj 
+      in
+      let j = match po with
+	 | Some p ->
              let pj = pretype empty_tycon env isevars lvar p in
              let dep = is_dependent_elimination env pj.uj_type indf in
              let ar =
@@ -425,9 +485,110 @@ let rec pretype tycon env isevars lvar = function
 	       let ci = make_default_case_info env st mis in
 	       mkCase (ci, (nf_betaiota pj.uj_val), cj.uj_val,[|fv|] ) 
 	     in
-	     { uj_val = v; uj_type = rsty })
+	     { uj_val = v; uj_type = rsty } in
+
+      (* Build the LetTuple form for v8 *)
+      let c =
+        let (ind,params) = dest_ind_family indf in
+        let rtntypopt, indnalopt = match po with
+          | None -> None, (Anonymous,None)
+          | Some p ->
+              let pj = pretype empty_tycon env isevars lvar p in
+              let dep = is_dependent_elimination env pj.uj_type indf in
+              let rec decomp_lam_force n avoid l p =
+                (* avoid is not exhaustive ! *)
+                if n = 0 then (List.rev l,p,avoid) else
+                  match p with
+                    | RLambda (_,(Name id as na),_,c) -> 
+                        decomp_lam_force (n-1) (id::avoid) (na::l) c
+                    | RLambda (_,(Anonymous as na),_,c) ->
+                        decomp_lam_force (n-1) avoid (na::l) c
+                    | _ ->
+                        let x = Nameops.next_ident_away (id_of_string "x") avoid in
+                        decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
+                          (* eta-expansion *)
+                          (RApp (dummy_loc,p, [RVar (dummy_loc,x)])) in
+              let (nal,p,avoid) = 
+                decomp_lam_force (List.length realargs) [] [] p in
+              let na,rtntyp,_ = 
+                if dep then decomp_lam_force 1 avoid [] p
+                else [Anonymous],p,[] in
+              let intyp =
+                if List.for_all
+                  (function
+                    | Anonymous -> true
+                    | Name id -> not (Cases.occur_rawconstr id rtntyp)) nal
+                then (* No dependency in realargs *)
+                  None
+                else
+                  let args = List.map (fun _ -> Anonymous) params @ nal in
+                  Some (dummy_loc,ind,args) in
+              (Some rtntyp,(List.hd na,intyp)) in
+        let cs = (get_constructors env indf).(0) in
+        match indnalopt with
+          | (na,None) -> (* Represented as a let *)
+              let rec decomp_lam_force n avoid l p =
+                if n = 0 then (List.rev l,p) else
+                  match p with
+                    | RLambda (_,(Name id as na),_,c) -> 
+                        decomp_lam_force (n-1) (id::avoid) (na::l) c
+                    | RLambda (_,(Anonymous as na),_,c) -> 
+                        decomp_lam_force (n-1) avoid (na::l) c
+                    | _ ->
+                        let x = Nameops.next_ident_away (id_of_string "x") avoid in
+                        decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
+                          (* eta-expansion *)
+                          (let a = RVar (dummy_loc,x) in
+                          match p with
+                            | RApp (loc,p,l) -> RApp (loc,p,l@[a])
+                            | _ -> (RApp (dummy_loc,p,[a]))) in
+              let (nal,d) = decomp_lam_force cs.cs_nargs [] [] f in
+              RLetTuple (loc,nal,(na,rtntypopt),c,d)
+          | _ -> (* Represented as a match *)
+            let detype_eqn constr construct_nargs branch =
+              let name_cons = function 
+                | Anonymous -> fun l -> l
+                | Name id -> fun l -> id::l in
+              let make_pat na avoid b ids =
+                PatVar (dummy_loc,na),
+                name_cons na avoid,name_cons na ids
+              in
+              let rec buildrec ids patlist avoid n b =
+                if n=0 then
+                  (dummy_loc, ids, 
+                  [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)],
+                  b)
+                else
+                  match b with
+	            | RLambda (_,x,_,b) -> 
+	                let pat,new_avoid,new_ids = make_pat x avoid b ids in
+                        buildrec new_ids (pat::patlist) new_avoid (n-1) b
+                          
+	            | RLetIn (_,x,_,b) -> 
+	                let pat,new_avoid,new_ids = make_pat x avoid b ids in
+                        buildrec new_ids (pat::patlist) new_avoid (n-1) b
+                          
+	            | RCast (_,c,_) ->    (* Oui, il y a parfois des cast *)
+	                buildrec ids patlist avoid n c
+                        
+	            | _ -> (* eta-expansion *)
+                        (* nommage de la nouvelle variable *)
+                        let id = Nameops.next_ident_away (id_of_string "x") avoid in
+	                let new_b = RApp (dummy_loc, b, [RVar(dummy_loc,id)])in
+                        let pat,new_avoid,new_ids =
+	                  make_pat (Name id) avoid new_b ids in
+	                buildrec new_ids (pat::patlist) new_avoid (n-1) new_b
+	                  
+              in 
+              buildrec [] [] [] construct_nargs branch in
+            let eqn = detype_eqn (ind,1) cs.cs_nargs f in
+            RCases (loc,(po,ref rtntypopt),[c,ref indnalopt],[eqn])
+      in
+      xx := Some c;
+      (* End building the v8 syntax *)
+      j
 
-  | ROrderedCase (loc,st,po,c,lf) ->
+  | ROrderedCase (loc,st,po,c,lf,x) ->
       let isrec = (st = MatchStyle) in
       let cj = pretype empty_tycon env isevars lvar c in
       let (IndType (indf,realargs) as indt) = 
@@ -503,6 +664,147 @@ let rec pretype tycon env isevars lvar = function
 	    mkCase (ci, (nf_betaiota pj.uj_val), cj.uj_val,
                        Array.map (fun j-> j.uj_val) lfj)
 	in
+        (* Build the Cases form for v8 *)
+        let c =
+          let (ind,params) = dest_ind_family indf in
+          let (mib,mip) = lookup_mind_specif env ind in
+          let recargs = mip.mind_recargs in
+          let mI = mkInd ind in
+          let nconstr = Array.length mip.mind_consnames in
+          let tyi = snd ind in
+          if isrec && mis_is_recursive_subset [tyi] recargs then
+            Some (Detyping.detype env [] (names_of_rel_context env)
+              (nf_evar (evars_of isevars) v))
+  (*
+            let sigma = evars_of isevars in
+            let init_depFvec i = if i = tyi then Some(dep,mkRel 1) else None in
+            let depFvec = Array.init mib.mind_ntypes init_depFvec in
+            (* build now the fixpoint *)
+            let lnames,_ = get_arity env indf in
+            let nar = List.length lnames in
+            let nparams = mip.mind_nparams in
+            let constrs = get_constructors env (lift_inductive_family (nar+2) indf) in
+            let branches = 
+              array_map3
+	        (fun f t reca -> 
+	          whd_beta
+                  (Indrec.make_rec_branch_arg env sigma
+                    (nparams,depFvec,nar+1)
+                    f t reca))
+                (Array.map (lift (nar+2)) lfv) constrs (dest_subterms recargs) 
+            in 
+            let ci = make_default_case_info env RegularStyle ind in
+            let deffix = 
+              it_mkLambda_or_LetIn_name env
+	        (lambda_create env
+	          (applist (mI,List.append (List.map (lift (nar+1)) params)
+                    (extended_rel_list 0 lnames)),
+                  mkCase (ci, lift (nar+2) pj.uj_val, mkRel 1, branches)))
+                (lift_rel_context 1 lnames) 
+            in
+            if noccurn 1 deffix then 
+              Some
+                (Detyping.detype env [] (names_of_rel_context env)
+                  (whd_beta (applist (pop deffix,realargs@[cj.uj_val]))))
+            else
+              let ind = applist (mI,(List.append 
+		(List.map (lift nar) params)
+		(extended_rel_list 0 lnames))) in
+              let typPfix =
+                let rec aux = function
+                  | (na,Some b,t)::l -> 
+                  | (na,None,t)::l -> RProd (dummy_loc,na,
+                  | [] -> 
+	        it_mkProd_or_LetIn_name env
+	          (prod_create env 
+	            (ind,
+	            (if dep then
+		      let ext_lnames = (Anonymous,None,ind)::lnames in
+		      let args = extended_rel_list 0 ext_lnames in
+		      whd_beta (applist (lift (nar+1) p, args))
+	            else
+		      let args = extended_rel_list 1 lnames in
+		      whd_beta (applist (lift (nar+1) p, args)))))
+                  lnames in
+              let fix =
+                RRec (dummy_loc,RFix ([|nar|],0),
+	        ([|(id_of_string "F")|],[|typPfix|],[|deffix|])) in
+              RApp (dummy_loc,fix,realargs@[c])
+              (msgerrnl (str "Warning: could't translate Match"); None)
+*)
+          else
+            let rtntypopt, indnalopt = match po with
+              | None -> None, (Anonymous,None)
+              | Some p ->
+                  let rec decomp_lam_force n avoid l p =
+                    (* avoid is not exhaustive ! *)
+                    if n = 0 then (List.rev l,p,avoid) else
+                      match p with
+                        | RLambda (_,(Name id as na),_,c) -> 
+                            decomp_lam_force (n-1) (id::avoid) (na::l) c
+                        | RLambda (_,(Anonymous as na),_,c) ->
+                            decomp_lam_force (n-1) avoid (na::l) c
+                        | _ ->
+                            let x = Nameops.next_ident_away (id_of_string "x") avoid in
+                            decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
+                              (* eta-expansion *)
+                              (RApp (dummy_loc,p, [RVar (dummy_loc,x)])) in
+                  let (nal,p,avoid) = 
+                    decomp_lam_force (List.length realargs) [] [] p in
+                  let na,rtntyopt,_ = 
+                    if dep then decomp_lam_force 1 avoid [] p
+                    else [Anonymous],p,[] in
+                  let args = List.map (fun _ -> Anonymous) params @ nal in
+                  (Some rtntyopt,(List.hd na,Some (dummy_loc,ind,args))) in
+
+            let detype_eqn constr construct_nargs branch =
+              let name_cons = function 
+                | Anonymous -> fun l -> l
+                | Name id -> fun l -> id::l in
+              let make_pat na avoid b ids =
+                PatVar (dummy_loc,na),
+                name_cons na avoid,name_cons na ids
+              in
+              let rec buildrec ids patlist avoid n b =
+                if n=0 then
+                  (dummy_loc, ids, 
+                  [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)],
+                  b)
+                else
+                  match b with
+	            | RLambda (_,x,_,b) -> 
+	                let pat,new_avoid,new_ids = make_pat x avoid b ids in
+                        buildrec new_ids (pat::patlist) new_avoid (n-1) b
+                          
+	            | RLetIn (_,x,_,b) -> 
+	                let pat,new_avoid,new_ids = make_pat x avoid b ids in
+                        buildrec new_ids (pat::patlist) new_avoid (n-1) b
+                          
+	            | RCast (_,c,_) ->    (* Oui, il y a parfois des cast *)
+	                buildrec ids patlist avoid n c
+                        
+	            | _ -> (* eta-expansion *)
+                        (* nommage de la nouvelle variable *)
+                        let id = Nameops.next_ident_away (id_of_string "x") avoid in
+	                let new_b = RApp (dummy_loc, b, [RVar(dummy_loc,id)])in
+                        let pat,new_avoid,new_ids =
+	                  make_pat (Name id) avoid new_b ids in
+	                buildrec new_ids (pat::patlist) new_avoid (n-1) new_b
+	                  
+              in 
+              buildrec [] [] [] construct_nargs branch in
+            let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
+            let get_consnarg j = 
+              let typi = mis_nf_constructor_type (ind,mib,mip) (j+1) in
+              let _,t = decompose_prod_n_assum mip.mind_nparams typi in
+              List.rev (fst (decompose_prod_assum t)) in
+            let consnargs = Array.init (Array.length mip.mind_consnames) get_consnarg in
+            let consnargsl = Array.map List.length consnargs in
+            let constructs = Array.init (Array.length lf) (fun i -> (ind,i+1)) in
+            let eqns = array_map3 detype_eqn constructs consnargsl lf in
+            Some (RCases (loc,(po,ref rtntypopt),[c,ref indnalopt],Array.to_list eqns)) in
+        x := c;
+        (* End build the Cases form for v8 *)
 	{ uj_val = v;
 	  uj_type = rsty }
 
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 3e13cd8610..bdb6914c24 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -67,10 +67,14 @@ type rawconstr =
   | RLambda of loc * name * rawconstr * rawconstr
   | RProd of loc * name * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
-  | RCases of loc * rawconstr option * rawconstr list * 
+  | RCases of loc * (rawconstr option * rawconstr option ref) *
+      (rawconstr * (name * (loc * inductive * name list) option) ref) list * 
       (loc * identifier list * cases_pattern list * rawconstr) list
+      (* Rem: "ref" used for the v7->v8 translation only *)
   | ROrderedCase of loc * case_style * rawconstr option * rawconstr * 
-      rawconstr array
+      rawconstr array * rawconstr option ref
+  | RLetTuple of loc * name list * (name * rawconstr option) * 
+      rawconstr * rawconstr
   | RRec of loc * fix_kind * identifier array * 
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
@@ -78,6 +82,10 @@ type rawconstr =
   | RCast of loc * rawconstr * rawconstr
   | RDynamic of loc * Dyn.t
 
+let cases_predicate_names tml =
+  List.flatten (List.map (function
+    | (tm,{contents=(na,None)}) -> [na]
+    | (tm,{contents=(na,Some (_,_,nal))}) -> na::nal) tml)
 
 (*i - if PRec (_, names, arities, bodies) is in env then arities are
    typed in env too and bodies are typed in env enriched by the
@@ -96,7 +104,8 @@ let loc = function
   | RProd (loc,_,_,_) -> loc
   | RLetIn (loc,_,_,_) -> loc
   | RCases (loc,_,_,_) -> loc
-  | ROrderedCase (loc,_,_,_,_) -> loc
+  | ROrderedCase (loc,_,_,_,_,_) -> loc
+  | RLetTuple (loc,_,_,_,_) -> loc
   | RRec (loc,_,_,_,_) -> loc
   | RCast (loc,_,_) -> loc
   | RSort (loc,_) -> loc
@@ -112,11 +121,14 @@ let map_rawconstr f = function
   | RLambda (loc,na,ty,c) -> RLambda (loc,na,f ty,f c)
   | RProd (loc,na,ty,c) -> RProd (loc,na,f ty,f c)
   | RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c)
-  | RCases (loc,tyopt,tml,pl) ->
-      RCases (loc,option_app f tyopt,List.map f tml,
+  | RCases (loc,(tyopt,rtntypopt),tml,pl) ->
+      RCases (loc,(option_app f tyopt,ref (option_app f !rtntypopt)),
+        List.map (fun (tm,x) -> (f tm,x)) tml,
         List.map (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl)
-  | ROrderedCase (loc,b,tyopt,tm,bv) ->
-      ROrderedCase (loc,b,option_app f tyopt,f tm, Array.map f bv)
+  | ROrderedCase (loc,b,tyopt,tm,bv,x) ->
+      ROrderedCase (loc,b,option_app f tyopt,f tm, Array.map f bv,ref (option_app f !x))
+  | RLetTuple (loc,nal,(na,po),b,c) ->
+      RLetTuple (loc,nal,(na,option_app f po),f b,f c)
   | RRec (loc,fk,idl,tyl,bv) -> RRec (loc,fk,idl,Array.map f tyl,Array.map f bv)
   | RCast (loc,c,t) -> RCast (loc,f c,f t)
   | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x
@@ -202,9 +214,17 @@ let rec subst_raw subst raw =
 	if r1' == r1 && r2' == r2 then raw else
 	  RLetIn (loc,n,r1',r2')
 
-  | RCases (loc,ro,rl,branches) -> 
+  | RCases (loc,(ro,rtno),rl,branches) -> 
       let ro' = option_smartmap (subst_raw subst) ro 
-      and rl' = list_smartmap (subst_raw subst) rl
+      and rtno' = ref (option_smartmap (subst_raw subst) !rtno)
+      and rl' = list_smartmap (fun (a,x as y) ->
+        let a' = subst_raw subst a in
+        let (n,topt) = !x in 
+        let topt' = option_smartmap
+          (fun (loc,(sp,i),x as t) ->
+            let sp' = subst_kn subst sp in
+            if sp == sp' then t else (loc,(sp',i),x)) topt in
+        if a == a' && topt == topt' then y else (a',ref (n,topt'))) rl
       and branches' = list_smartmap 
 			(fun (loc,idl,cpl,r as branch) ->
 			   let cpl' = list_smartmap (subst_pat subst) cpl
@@ -214,15 +234,22 @@ let rec subst_raw subst raw =
 			branches
       in
 	if ro' == ro && rl' == rl && branches' == branches then raw else
-	  RCases (loc,ro',rl',branches')
+	  RCases (loc,(ro',rtno'),rl',branches')
 
-  | ROrderedCase (loc,b,ro,r,ra) -> 
+  | ROrderedCase (loc,b,ro,r,ra,x) -> 
       let ro' = option_smartmap (subst_raw subst) ro
       and r' = subst_raw subst r 
       and ra' = array_smartmap (subst_raw subst) ra in
 	if ro' == ro && r' == r && ra' == ra then raw else
-	  ROrderedCase (loc,b,ro',r',ra')
-
+	  ROrderedCase (loc,b,ro',r',ra',x)
+
+  | RLetTuple (loc,nal,(na,po),b,c) ->
+      let po' = option_smartmap (subst_raw subst) po
+      and b' = subst_raw subst b 
+      and c' = subst_raw subst c in
+	if po' == po && b' == b && c' == c then raw else
+          RLetTuple (loc,nal,(na,po),b,c)
+      
   | RRec (loc,fix,ida,ra1,ra2) -> 
       let ra1' = array_smartmap (subst_raw subst) ra1
       and ra2' = array_smartmap (subst_raw subst) ra2 in
@@ -255,7 +282,8 @@ let loc_of_rawconstr = function
   | RProd (loc,_,_,_) -> loc
   | RLetIn (loc,_,_,_) -> loc
   | RCases (loc,_,_,_) -> loc
-  | ROrderedCase (loc,_,_,_,_) -> loc
+  | ROrderedCase (loc,_,_,_,_,_) -> loc
+  | RLetTuple (loc,_,_,_,_) -> loc
   | RRec (loc,_,_,_,_) -> loc
   | RSort (loc,_) -> loc
   | RHole (loc,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index fbd01db9ac..27bb76b69a 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -65,10 +65,13 @@ type rawconstr =
   | RLambda of loc * name * rawconstr * rawconstr
   | RProd of loc * name * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
-  | RCases of loc * rawconstr option * rawconstr list * 
+  | RCases of loc * (rawconstr option * rawconstr option ref) *
+      (rawconstr * (name * (loc * inductive * name list) option) ref) list * 
       (loc * identifier list * cases_pattern list * rawconstr) list
   | ROrderedCase of loc * case_style * rawconstr option * rawconstr * 
-      rawconstr array
+      rawconstr array * rawconstr option ref
+  | RLetTuple of loc * name list * (name * rawconstr option) * 
+      rawconstr * rawconstr
   | RRec of loc * fix_kind * identifier array * 
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
@@ -76,6 +79,9 @@ type rawconstr =
   | RCast of loc * rawconstr * rawconstr
   | RDynamic of loc * Dyn.t
 
+val cases_predicate_names : 
+  (rawconstr * (name * (loc * inductive * name list) option) ref) list ->
+      name list
 
 (*i - if PRec (_, names, arities, bodies) is in env then arities are
    typed in env too and bodies are typed in env enriched by the