deplacement poly_args; iterateurs sur les segments

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

2 files changed, 0 insertions, 36 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index dd2adf2f5f..d496a9e49a 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1104,40 +1104,6 @@ let is_info_type env sigma t =
   (s <> Prop Null && 
    try info_arity env sigma t.utj_val with IsType -> true)
 
-(* calcul des arguments implicites *)
-
-(* la seconde liste est ordonne'e *)
-
-let ord_add x l =
-  let rec aux l = match l with 
-    | []    -> [x]
-    | y::l' -> if y > x then x::l else if x = y then l else y::(aux l')
-  in 
-  aux l
-    
-let add_free_rels_until bound m acc =
-  let rec frec depth acc c = match kind_of_term c with
-    | IsRel n when (n < bound+depth) & (n >= depth) ->
-	Intset.add (bound+depth-n) acc
-    | _ -> fold_constr_with_binders succ frec depth acc c
-  in 
-  frec 1 acc m 
-
-(* calcule la liste des arguments implicites *)
-
-let poly_args env sigma t =
-  let rec aux env n t =
-    match kind_of_term (whd_betadeltaiota env sigma t) with
-      | IsProd (x,a,b) ->
-	  add_free_rels_until n a
-	    (aux (push_rel_assum (x,a) env) (n+1) b)
-      | _ -> Intset.empty
-  in 
-  match kind_of_term (whd_betadeltaiota env sigma t) with 
-    | IsProd (x,a,b) ->
-	Intset.elements (aux (push_rel_assum (x,a) env) 1 b)
-    | _ -> []
-
 (* Expanding existential variables (pretyping.ml) *)
 (* 1- whd_ise fails if an existential is undefined *)
 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 7908c26f26..10b4edc43c 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -142,8 +142,6 @@ val is_info_cast_type : env -> 'a evar_map -> constr -> bool
 val contents_of_cast_type : env -> 'a evar_map -> constr -> contents
 i*)
 
-val poly_args : env -> 'a evar_map -> constr -> int list
-
 val whd_programs : 'a reduction_function
 
 (* [reduce_fix] contracts a fix redex if it is actually reducible *)