Removed obsolete v7->v8 translation code (function check_same_type is

costly in size but it is still used for checking that the parameters
of mutual inductive types are the same...).

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

3 files changed, 0 insertions, 83 deletions

diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index f52ec8fd8..ac9ed5714 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -21,7 +21,6 @@ open Pattern
 open Topconstr
 open Notation
 
-(** v7->v8 translation *)
 val check_same_type : constr_expr -> constr_expr -> unit
 
 (** Translation of pattern, cases pattern, rawterm and term into syntax
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index cd56bccb7..08ac7fd68 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -307,85 +307,6 @@ let split_product na' = function
       rename na na' t (CProdN(loc,(nal,bk,t)::bl,c))
   | _ -> anomaly "ill-formed fixpoint body"
 
-let merge_binders (na1,bk1,ty1) cofun (na2,bk2,ty2) codom =
-  let na =
-    match snd na1, snd na2 with
-        Anonymous, Name id ->
-          if occur_var_constr_expr id cofun then
-            failwith "avoid capture"
-          else na2
-      | Name id, Anonymous ->
-          if occur_var_constr_expr id codom then
-            failwith "avoid capture"
-          else na1
-      | Anonymous, Anonymous -> na1
-      | Name id1, Name id2 ->
-          if id1 <> id2 then failwith "not same name" else na1 in
-  let ty =
-    match ty1, ty2 with
-        CHole _, _ -> ty2
-      | _, CHole _ -> ty1
-      | _ ->
-          Constrextern.check_same_type ty1 ty2;
-          ty2 in
-  (LocalRawAssum ([na],bk1,ty), codom)
-
-let rec strip_domain bvar cofun c =
-  match c with
-    | CArrow(loc,a,b) ->
-        merge_binders bvar cofun ((dummy_loc,Anonymous),default_binder_kind,a) b
-    | CProdN(loc,[([na],bk,ty)],c') ->
-        merge_binders bvar cofun (na,bk,ty) c'
-    | CProdN(loc,([na],bk,ty)::bl,c') ->
-        merge_binders bvar cofun (na,bk,ty) (CProdN(loc,bl,c'))
-    | CProdN(loc,(na::nal,bk,ty)::bl,c') ->
-        merge_binders bvar cofun (na,bk,ty) (CProdN(loc,(nal,bk,ty)::bl,c'))
-    | _ -> failwith "not a product"
-
-(* Note: binder sharing is lost *)
-let rec strip_domains (nal,bk,ty) cofun c =
-  match nal with
-      [] -> assert false
-    | [na] ->
-        let bnd, c' = strip_domain (na,bk,ty) cofun c in
-        ([bnd],None,c')
-    | na::nal ->
-        let f = CLambdaN(dummy_loc,[(nal,bk,ty)],cofun) in
-        let bnd, c1 = strip_domain (na,bk,ty) f c in
-        (try
-          let bl, rest, c2 = strip_domains (nal,bk,ty) cofun c1 in
-          (bnd::bl, rest, c2)
-        with Failure _ -> ([bnd],Some (nal,bk,ty), c1))
-
-(* Re-share binders *)
-let rec factorize_binders = function
-  | ([] | [_] as l) -> l
-  | LocalRawAssum (nal,k,ty) as d :: (LocalRawAssum (nal',k',ty')::l as l') ->
-      (try
-	let _ = Constrextern.check_same_type ty ty' in
-	factorize_binders (LocalRawAssum (nal@nal',k,ty)::l)
-      with _ ->
-	d :: factorize_binders l')
-  | d :: l -> d :: factorize_binders l
-
-(* Extract lambdas when a type constraint occurs *)
-let rec extract_def_binders c ty =
-  match c with
-    | CLambdaN(loc,bvar::lams,b) ->
-        (try
-          let f = CLambdaN(loc,lams,b) in
-          let bvar', rest, ty' = strip_domains bvar f ty in
-          let c' =
-            match rest, lams with
-                None,[] -> b
-              | None, _ -> f
-              | Some bvar,_ -> CLambdaN(loc,bvar::lams,b) in
-          let (bl,c2,ty2) = extract_def_binders c' ty' in
-          (factorize_binders (bvar'@bl), c2, ty2)
-        with Failure _ ->
-          ([],c,ty))
-    | _ -> ([],c,ty)
-
 let rec split_fix n typ def =
   if n = 0 then ([],typ,def)
   else
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index f1bb49312..d2d44f245 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -24,9 +24,6 @@ val extract_lam_binders :
   constr_expr -> local_binder list * constr_expr
 val extract_prod_binders :
   constr_expr -> local_binder list * constr_expr
-val extract_def_binders :
-  constr_expr -> constr_expr ->
-  local_binder list * constr_expr * constr_expr
 val split_fix :
   int -> constr_expr -> constr_expr ->
   local_binder list *  constr_expr * constr_expr