Suppression résidus code v7 et traducteur

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

1 files changed, 0 insertions, 90 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 193d0a1616..3e0ac74714 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -55,96 +55,6 @@ open Declarations
 open Inductive
 open Inductiveops
 
-let lift_context n l = 
-  let k = List.length l in 
-  list_map_i (fun i (name,c) -> (name,liftn n (k-i) c)) 0 l
-
-(* Tells if a given predicate in v7 syntax is dependent or not *)
-
-let is_dep_arity env kelim predty nodep_ar = 
-  let rec srec pt nodep_ar =
-    let pt' = whd_betadeltaiota env Evd.empty pt in
-    match kind_of_term pt', kind_of_term nodep_ar with
-      | Prod (_,a1,a2), Prod (_,a1',a2') -> srec a2 a2'
-      | Prod (_,a1,a2), _ -> true
-      | _ -> false in 
-  srec predty nodep_ar
-
-let is_dependent_elimination env predty indf =
-  let (ind,params) = dest_ind_family 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_arity env kelim predty glob_t
-
-(* Interpret v7 Match construct *)
-
-let transform_rec loc env sigma (pj,c,lf) indt = 
-  let p = pj.uj_val in
-  let (indf,realargs) = dest_ind_type 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 mI = mkInd 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
-     error_number_branches_loc loc env sigma cj nconstr);
-  let tyi = snd ind in
-  if mis_is_recursive_subset [tyi] recargs then
-    let dep =
-      is_dependent_elimination env (nf_evar sigma pj.uj_type) indf 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 = mib.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)) lf) constrs (dest_subterms recargs) 
-    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) p, mkRel 1, branches)))
-        (lift_rel_context 1 lnames) 
-    in
-    if noccurn 1 deffix then 
-      whd_beta (applist (pop deffix,realargs@[c]))
-    else
-      let ind = applist (mI,(List.append 
-			     (List.map (lift nar) params)
-			     (extended_rel_list 0 lnames))) in
-      let typPfix = 
-	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 =
-        mkFix (([|nar|],0),
-	       ([|Name(id_of_string "F")|],[|typPfix|],[|deffix|])) in
-      applist (fix,realargs@[c])
-  else
-    mkCase (ci, p, c, lf)
-
 (************************************************************************)
 
 (* To embed constr in rawconstr *)