Suppression des parseurs et printeurs v7; suppression du traducteur (mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.)

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

9 files changed, 45 insertions, 540 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 28e8c41396..d9f7324cf4 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1641,7 +1641,7 @@ let build_initial_predicate isdep allnames pred =
   in buildrec 0 pred allnames
 
 let extract_arity_signature env0 tomatchl tmsign =
-  let get_one_sign n tm {contents = (na,t)} =
+  let get_one_sign n tm (na,t) =
     match tm with
       | NotInd (bo,typ) -> 
 	  (match t with
@@ -1684,34 +1684,23 @@ let extract_arity_signature env0 tomatchl tmsign =
  * type and 1 assumption for each term not _syntactically_ in an
  * inductive type.
 
- * V7 case: determines whether the multiple case is dependent or not
- * - if its arity is made of nrealargs assumptions for each matched
- * term in an inductive type and nothing for terms not _syntactically_
- * in an inductive type, then it is non dependent
- * - if its arity is made of 1+nrealargs assumptions for each matched
- * term in an inductive type and nothing for terms not _syntactically_
- * in an inductive type, then it is dependent and needs an adjustement
- * to fulfill the criterion above that terms not in an inductive type
- * counts for 1 in the dependent case
+ * Each matched terms are independently considered dependent or not.
 
- * V8 case: each matched terms are independently considered dependent
- * or not
-
- * A type constraint but no annotation case: it is assumed non dependent
+ * A type constraint but no annotation case: it is assumed non dependent.
  *)
 
 let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
-  (* No type annotation at all *)
-  | (None,{contents = None}) ->
+  (* No type annotation *)
+  | None ->
       (match tycon with
        | None -> None
        | Some t ->
-	 let names,pred = prepare_predicate_from_tycon loc false env isevars tomatchs t in
+	 let names,pred = 
+	   prepare_predicate_from_tycon loc false env isevars tomatchs t in
 	 Some (build_initial_predicate false names pred))
 
-  (* v8 style type annotation *)
-  | (None,{contents = Some rtntyp}) ->
-
+  (* Some type annotation *)
+  | Some rtntyp ->
       (* We extract the signature of the arity *)
       let arsign = extract_arity_signature env tomatchs sign in
       let env = List.fold_right push_rels arsign env in
@@ -1719,39 +1708,6 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
       let predccl = (typing_fun (mk_tycon (new_Type ())) env rtntyp).uj_val in
       Some (build_initial_predicate true allnames predccl)
 
-  (* 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 = !isevars in
-        (* We first assume the predicate is non dependent *)
-	let ndep_arity = build_expected_arity env isevars false tomatchs in
-        try
-	  false, nb_prod ndep_arity, typing_fun (mk_tycon ndep_arity) env pred
-	with PretypeError _ | TypeError _ |
-	    Stdpp.Exc_located (_,(PretypeError _ | TypeError _)) ->
-        (* Backtrack! *)
-        isevars := isevars_copy;
-        (* We then assume the predicate is dependent *)
-	let dep_arity = build_expected_arity env isevars true tomatchs in
-	try
-	  true, nb_prod dep_arity, typing_fun (mk_tycon dep_arity) env pred
-	with PretypeError _ | TypeError _ |
-	  Stdpp.Exc_located (_,(PretypeError _ | TypeError _)) ->
-        (* Backtrack again! *)
-        isevars := isevars_copy;
-        (* Otherwise we attempt to type it without constraints, possibly *)
-        (* failing with an error message; it may also be well-typed *)
-	(* but fails to satisfy arity constraints in case_dependent *)
-        let predj = typing_fun empty_tycon env pred in
-	error_wrong_predicate_arity_loc
-	  loc env predj.uj_val ndep_arity dep_arity
-      in
-      let ln,predccl= extract_predicate_conclusion dep tomatchs predj.uj_val in
-      set_arity_signature dep n sign tomatchs pred x;
-      Some (build_initial_predicate dep ln predccl)
-
-
 (**************************************************************************)
 (* Main entry of the matching compilation                                 *)
 
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index de63ea5258..7da7abcce6 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -53,7 +53,7 @@ val compile_cases :
   evar_defs ref ->
   type_constraint -> 
   env ->
-  (rawconstr option * rawconstr option ref) *
-  (rawconstr * (name * (loc * inductive * name list) option) ref) list *
+  rawconstr option *
+  (rawconstr * (name * (loc * inductive * name list) option)) list *
   (loc * identifier list * cases_pattern list * rawconstr) list ->
   unsafe_judgment
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 6d49baf52b..62c721b8b8 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -210,8 +210,8 @@ let inductive_class_of ind = fst (class_info (CL_IND ind))
 let class_args_of c = snd (decompose_app c)
 
 let string_of_class = function
-  | CL_FUN -> if !Options.v7 then "FUNCLASS" else "Funclass"
-  | CL_SORT -> if !Options.v7 then "SORTCLASS" else "Sortclass"
+  | CL_FUN -> "Funclass"
+  | CL_SORT -> "Sortclass"
   | CL_CONST sp ->
       string_of_qualid (shortest_qualid_of_global Idset.empty (ConstRef sp))
   | CL_IND sp ->
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 19c5ca54be..b955d62d7d 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -223,14 +223,13 @@ let detype_case computable detype detype_eqn testdep
     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 alias, aliastyp, newpred, pred = 
+  let alias, aliastyp, pred= 
     if (not !Options.raw_print) & synth_type & computable & Array.length bl<>0 
     then 
-      Anonymous, None, None, None
+      Anonymous, None, None
     else
-      let p = option_app detype p in
-      match p with
-        | None -> Anonymous, None, None, None
+      match option_app detype p with
+        | None -> Anonymous, None, None
         | Some p ->
             let decompose_lam k c =
               let rec lamdec_rec l avoid k c =
@@ -255,7 +254,7 @@ let detype_case computable detype detype_eqn testdep
 	      else 
 		let pars = list_tabulate (fun _ -> Anonymous) mib.mind_nparams
 		in Some (dummy_loc,indsp,pars@nl) in
-            n, aliastyp, Some typ, Some p
+            n, aliastyp, Some typ
   in
   let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
   let eqnv = array_map3 detype_eqn constructs consnargsl bl in
@@ -273,10 +272,10 @@ let detype_case computable detype detype_eqn testdep
     with Not_found -> st
   in 
   if tag = RegularStyle then
-    RCases (dummy_loc,(pred,ref newpred),[tomatch,ref (alias,aliastyp)],eqnl)
+    RCases (dummy_loc,pred,[tomatch,(alias,aliastyp)],eqnl)
   else
     let bl' = Array.map detype bl in
-    if not !Options.v7 && tag = LetStyle && aliastyp = None then
+    if 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
@@ -293,37 +292,16 @@ let detype_case computable detype detype_eqn testdep
                     | 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)
+      RLetTuple (dummy_loc,nal,(alias,pred),tomatch,d)
     else
     let nondepbrs =
       array_map3 (extract_nondep_branches testdep) bl bl' consnargsl in
-    if not !Options.v7 && tag = IfStyle && aliastyp = None
+    if tag = IfStyle && aliastyp = None
       && array_for_all ((<>) None) nondepbrs then
-      RIf (dummy_loc,tomatch,(alias,newpred),
+      RIf (dummy_loc,tomatch,(alias,pred),
            out_some nondepbrs.(0),out_some nondepbrs.(1))
-    else if !Options.v7 then
-      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)
-    else
-      RCases(dummy_loc,(pred,ref newpred),[tomatch,ref (alias,aliastyp)],eqnl)
+    else 
+      RCases(dummy_loc,pred,[tomatch,(alias,aliastyp)],eqnl)
 
 
 let rec detype tenv avoid env t =
@@ -405,11 +383,6 @@ and detype_cofix tenv avoid env n (names,tys,bodies) =
        Array.map (fun (_,bd,_) -> bd) v)
 
 and share_names tenv n l avoid env c t =
-  if !Options.v7 && n=0 then
-    let c = detype tenv avoid env c in
-    let t = detype tenv avoid env t in
-    (List.rev l,c,t)
-  else
   match kind_of_term c, kind_of_term t with
     (* factorize even when not necessary to have better presentation *)
     | Lambda (na,t,c), Prod (na',t',c') ->
@@ -535,17 +508,16 @@ let rec subst_raw subst raw =
 	if r1' == r1 && r2' == r2 then raw else
 	  RLetIn (loc,n,r1',r2')
 
-  | RCases (loc,(ro,rtno),rl,branches) -> 
-      let ro' = option_smartmap (subst_raw subst) ro 
-      and rtno' = ref (option_smartmap (subst_raw subst) !rtno)
+  | RCases (loc,rtno,rl,branches) -> 
+      let rtno' = 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 (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
+        if a == a' && topt == topt' then y else (a',(n,topt'))) rl
       and branches' = list_smartmap 
 			(fun (loc,idl,cpl,r as branch) ->
 			   let cpl' = list_smartmap (subst_pat subst) cpl
@@ -554,15 +526,8 @@ let rec subst_raw subst raw =
 			       (loc,idl,cpl',r'))
 			branches
       in
-	if ro' == ro && rl' == rl && branches' == branches then raw else
-	  RCases (loc,(ro',rtno'),rl',branches')
-
-  | 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',x)
+	if rtno' == rtno && rl' == rl && branches' == branches then raw else
+	  RCases (loc,rtno',rl',branches')
 
   | RLetTuple (loc,nal,(na,po),b,c) ->
       let po' = option_smartmap (subst_raw subst) po
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index df9139db1f..634f0b5915 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -22,14 +22,8 @@ open Mod_subst
 (* Metavariables *)
 
 type patvar_map = (patvar * constr) list
-let patvar_of_int n =
-  let p = if !Options.v7 & not (Options.do_translate ()) then "?" else "X"
-  in
-  Names.id_of_string (p ^ string_of_int n)
 let pr_patvar = pr_id
 
-let patvar_of_int_v7 n = Names.id_of_string ("?" ^ string_of_int n)
-
 (* Patterns *)
 
 type constr_pattern =
@@ -217,26 +211,21 @@ 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,_) ->
-      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)
   | RIf (_,c,(_,None),b1,b2) ->
       PCase ((None,IfStyle),None, pat_of_raw metas vars c,
              [|pat_of_raw metas vars b1; pat_of_raw metas vars b2|])
-  | RCases (loc,(po,_),[c,_],brs) ->
+  | RCases (loc,None,[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,
+      PCase ((sp,Term.RegularStyle),None,
              pat_of_raw metas vars c,
              Array.init (List.length brs)
 	       (pat_of_raw_branch loc metas vars sp brs))
   | r ->
       let loc = loc_of_rawconstr r in
-      user_err_loc (loc,"pattern_of_rawconstr", Pp.str "Not supported pattern")
+      user_err_loc (loc,"pattern_of_rawconstr", Pp.str "Pattern not supported")
 
 and pat_of_raw_branch loc metas vars ind brs i =
   let bri = List.filter
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 7ce0c4124e..0815f87211 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -25,10 +25,6 @@ open Mod_subst
 type patvar_map = (patvar * constr) list
 val pr_patvar : patvar -> std_ppcmds
 
-(* Only for v7 parsing/printing *)
-val patvar_of_int : int -> patvar
-val patvar_of_int_v7 : int -> patvar
-
 (* Patterns *)
 
 type constr_pattern =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0baaa98198..193d0a1616 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -462,201 +462,6 @@ let rec pretype tycon env isevars lvar = function
 	     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 =
-               arity_of_case_predicate env indf dep (Type (new_univ())) in
-             let _ = e_cumul env isevars pj.uj_type ar in
-	     let pj = j_nf_evar (evars_of !isevars) pj in
-	     let pj = if dep then pj else make_dep_of_undep env indt pj in
-	     let (bty,rsty) = 
-	       Indrec.type_rec_branches 
-		 false env (evars_of !isevars) indt pj.uj_val cj.uj_val 
-	     in
-	     if Array.length bty <> 1 then
-	       error_number_branches_loc 
-		 loc env (evars_of !isevars) cj (Array.length bty);
-	     let fj = 
-	       let tyc = bty.(0) in 
-	       pretype (mk_tycon tyc) env isevars lvar f 
-	     in
-	     let fv = j_val fj in
-	     let ft = fj.uj_type in
-	     check_branches_message loc env isevars cj.uj_val (bty,[|ft|]);
-	     let v =
-	       let mis,_ = dest_ind_family indf in
-	       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 }
-
-	 | None -> 
-             (* get type information from type of branches *)
-	     let expbr = Cases.branch_scheme env isevars false indf in
-	     if Array.length expbr <> 1 then
-	       error_number_branches_loc loc env (evars_of !isevars) 
-		 cj (Array.length expbr);
-             let expti = expbr.(0) in
-	     let fj = pretype (mk_tycon expti) env isevars lvar f in
-	     let use_constraint () =
-               (* get type information from constraint *)
-               (* warning: if the constraint comes from an evar type, it *)
-               (* may be Type while Prop or Set would be expected *)
-	       match tycon with
-		 | Some pred ->
-		     let arsgn = make_arity_signature env true indf in
-                     let pred = lift (List.length arsgn) pred in
-  		     let pred = 
-                       it_mkLambda_or_LetIn (nf_evar (evars_of !isevars) pred)
-			 arsgn in
-                     false, pred
-	         | None ->
-                     let sigma = evars_of !isevars in
-                     error_cant_find_case_type_loc loc env sigma cj.uj_val
-	     in
-             let ok, p =
-	       try
-		 let pred = 
-		   Cases.pred_case_ml 
-		     env (evars_of !isevars) false indt (0,fj.uj_type) 
-		 in 
-		 if is_ground_term !isevars pred then
-		   true, pred
-		 else
-		   use_constraint ()
-	       with Cases.NotInferable _ ->
-		 use_constraint ()
-	     in 
-	     let p = nf_evar (evars_of !isevars) p in
-	     let (bty,rsty) =
-	       Indrec.type_rec_branches
-		 false env (evars_of !isevars) indt p cj.uj_val 
-	     in
-	     let _ = option_app (e_cumul env isevars rsty) tycon in
-	     let fj = 
-	       if ok then fj 
-	       else pretype (mk_tycon bty.(0)) env isevars lvar f 
-	     in
-	     let fv = fj.uj_val in
-	     let v =
-	       let mis,_ = dest_ind_family indf in
-	       let ci = make_default_case_info env st mis in
-	       mkCase (ci, (nf_betaiota p), cj.uj_val,[|fv|] ) 
-	     in
-	     { 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 (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
-
   | RIf (loc,c,(na,po),b1,b2) ->
       let cj = pretype empty_tycon env isevars lvar c in
       let (IndType (indf,realargs)) = 
@@ -707,200 +512,6 @@ let rec pretype tycon env isevars lvar = function
       in
       { uj_val = v; uj_type = p }
 
-  | 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) = 
-	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 (dep,pj) = 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 =
-              arity_of_case_predicate env indf dep (Type (new_univ())) in
-            let _ = e_cumul env isevars pj.uj_type ar in
-            (dep, pj)
-	| None -> 
-            (* get type information from type of branches *)
-	    let expbr = Cases.branch_scheme env isevars isrec indf in
-	    let rec findtype i =
-	      if i >= Array.length lf
-	      then
-                (* get type information from constraint *)
-                (* warning: if the constraint comes from an evar type, it *)
-                (* may be Type while Prop or Set would be expected *)
-	        match tycon with
-		  | Some pred ->
-		      let arsgn = make_arity_signature env true indf in
-                      let pred = lift (List.length arsgn) pred in
-  		      let pred = 
-			it_mkLambda_or_LetIn (nf_evar (evars_of !isevars) pred)
-			  arsgn in
-                      (true, 
-                       Retyping.get_judgment_of env (evars_of !isevars) pred)
-	          | None ->
-                      let sigma = evars_of !isevars in
-                      error_cant_find_case_type_loc loc env sigma cj.uj_val
-	      else
-		try
-		  let expti = expbr.(i) in
-		  let fj =
-		    pretype (mk_tycon expti) env isevars lvar lf.(i) in
-		  let pred = 
-		    Cases.pred_case_ml (* eta-expanse *)
-                      env (evars_of !isevars) isrec indt (i,fj.uj_type) in
-		  if not (is_ground_term !isevars pred) then findtype (i+1)
-		  else 
-		    let pty =
-                      Retyping.get_type_of env (evars_of !isevars) pred in
-		    let pj = { uj_val = pred; uj_type = pty } in
-(*
-                    let _ = option_app (the_conv_x_leq env isevars pred) tycon
-                    in
-*)
-                    (true,pj)
-		with Cases.NotInferable _ -> findtype (i+1) in
-	    findtype 0 
-      in
-      let pj = j_nf_evar (evars_of !isevars) pj in
-      let pj = if dep then pj else make_dep_of_undep env indt pj in
-      let (bty,rsty) =
-	Indrec.type_rec_branches
-          isrec env (evars_of !isevars) indt pj.uj_val cj.uj_val in
-      let _ = option_app (e_cumul env isevars rsty) tycon in
-      if Array.length bty <> Array.length lf then
-	error_number_branches_loc loc env (evars_of !isevars) 
-	  cj (Array.length bty)
-      else
-	let lfj =
-	  array_map2
-            (fun tyc f -> pretype (mk_tycon tyc) env isevars lvar f) bty
-            lf in
-	let lfv = Array.map j_val lfj in
-	let lft = Array.map (fun j -> j.uj_type) lfj in
-	check_branches_message loc env isevars cj.uj_val (bty,lft);
-	let v =
-	  if isrec
-	  then 
-	    transform_rec loc env (evars_of !isevars)(pj,cj.uj_val,lfv) indt
-	  else
-	    let mis,_ = dest_ind_family indf in
-	    let ci = make_default_case_info env st mis in
-	    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 tyi = snd ind in
-          if isrec && mis_is_recursive_subset [tyi] recargs then
-            Some (Detyping.detype (false,env)
-	      (ids_of_context env) (names_of_rel_context env)
-              (nf_evar (evars_of !isevars) v))
-	  else
-	    (* Translate into a "match ... with" *)
-            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 intyp =
-		    if nal=[] then None else
-                      let args = List.map (fun _ -> Anonymous) params @ nal in
-		      Some (dummy_loc,ind,args) in
-                  (Some rtntyopt,(List.hd na,intyp)) in
-	    let rawbranches =
-	      array_map3 (fun bj b cstr ->
-		let rec strip n r = if n=0 then r else
-		  match r with
-		    | RLambda (_,_,_,t) -> strip (n-1) t
-		    | RLetIn (_,_,_,t) -> strip (n-1) t
-		    | _ -> assert false in
-		let n = rel_context_length cstr.cs_args in
-		try
-		  let _,ccl = decompose_lam_n_assum n bj.uj_val in
-		  if noccur_between 1 n ccl then Some (strip n b) else None
-		with _ -> (* Not eta-expanded or not reduced *) None)
-		lfj lf (get_constructors env indf) in
-	    if st = IfStyle & snd indnalopt = None 
-	       & rawbranches.(0) <> None && rawbranches.(1) <> None then
-	      (* Translate into a "if ... then ... else" *)
-	      (* TODO: translate into a "if" even if po is dependent *)
-	      Some (RIf (loc,c,(fst indnalopt,rtntypopt),
-	          out_some rawbranches.(0),out_some rawbranches.(1)))
-	    else
-            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 mib.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 }
-
   | RCases (loc,po,tml,eqns) ->
       Cases.compile_cases loc
 	((fun vtyc env -> pretype vtyc env isevars lvar),isevars)
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index dde8490d05..a75f6165f6 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -58,11 +58,9 @@ 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 option ref) *
-      (rawconstr * (name * (loc * inductive * name list) option) ref) list * 
+  | RCases of loc * rawconstr option *
+      (rawconstr * (name * (loc * inductive * name list) option)) list * 
       (loc * identifier list * cases_pattern list * rawconstr) list
-  | ROrderedCase of loc * case_style * rawconstr option * rawconstr * 
-      rawconstr array * rawconstr option ref
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
   | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
@@ -77,8 +75,8 @@ and rawdecl = name * rawconstr option * rawconstr
 
 let cases_predicate_names tml =
   List.flatten (List.map (function
-    | (tm,{contents=(na,None)}) -> [na]
-    | (tm,{contents=(na,Some (_,_,nal))}) -> na::nal) tml)
+    | (tm,(na,None)) -> [na]
+    | (tm,(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
@@ -97,12 +95,10 @@ 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,rtntypopt),tml,pl) ->
-      RCases (loc,(option_app f tyopt,ref (option_app f !rtntypopt)),
+  | RCases (loc,rtntypopt,tml,pl) ->
+      RCases (loc,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,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)
   | RIf (loc,c,(na,po),b1,b2) ->
@@ -140,8 +136,6 @@ let map_rawconstr_with_binders_loc loc g f e = function
       let h (_,idl,p,c) = (loc,idl,p,f (List.fold_right g' idl e) c) in
       RCases
 	(loc,option_app (f e) tyopt,List.map (f e) tml, List.map h pl)
-  | ROrderedCase (_,b,tyopt,tm,bv) ->
-      ROrderedCase (loc,b,option_app (f e) tyopt,f e tm,Array.map (f e) bv)
   | RRec (_,fk,idl,tyl,bv) ->
       let idl',e' = fold_ident g idl e in
       RRec (loc,fk,idl',Array.map (f e) tyl,Array.map (f e') bv)
@@ -161,12 +155,10 @@ 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,rtntypopt),tml,pl) ->
-	(occur_option tyopt) or (occur_option !rtntypopt)
+    | RCases (loc,rtntypopt,tml,pl) ->
+	(occur_option rtntypopt)
         or (List.exists (fun (tm,_) -> occur tm) tml)
 	or (List.exists occur_pattern pl)
-    | ROrderedCase (loc,b,tyopt,tm,bv,_) -> 
-	(occur_option tyopt) or (occur tm) or (array_exists occur bv)
     | RLetTuple (loc,nal,rtntyp,b,c) -> 
 	occur_return_type rtntyp id
         or (occur b) or (not (List.mem (Name id) nal) & (occur c))
@@ -205,7 +197,6 @@ let loc_of_rawconstr = function
   | RProd (loc,_,_,_) -> loc
   | RLetIn (loc,_,_,_) -> loc
   | RCases (loc,_,_,_) -> loc
-  | ROrderedCase (loc,_,_,_,_,_) -> loc
   | RLetTuple (loc,_,_,_,_) -> loc
   | RIf (loc,_,_,_,_) -> loc
   | RRec (loc,_,_,_,_,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 4e4df6b39c..014739fcb7 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -55,11 +55,9 @@ 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 option ref) *
-      (rawconstr * (name * (loc * inductive * name list) option) ref) list * 
+  | RCases of loc * rawconstr option *
+      (rawconstr * (name * (loc * inductive * name list) option)) list * 
       (loc * identifier list * cases_pattern list * rawconstr) list
-  | ROrderedCase of loc * case_style * rawconstr option * rawconstr * 
-      rawconstr array * rawconstr option ref
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
   | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
@@ -73,8 +71,7 @@ type rawconstr =
 and rawdecl = name * rawconstr option * rawconstr
 
 val cases_predicate_names : 
-  (rawconstr * (name * (loc * inductive * name list) option) ref) list ->
-      name list
+  (rawconstr * (name * (loc * inductive * name list) option)) 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