From 94b27cf1c88ba0473b4b59a81be93b1d7d1f9316 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 2 Jun 2000 14:18:01 +0000
Subject: Retrait de decomp_prod non conforme à sa spec

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@496 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/reduction.ml  | 9 ---------
 kernel/reduction.mli | 1 -
 2 files changed, 10 deletions(-)

(limited to 'kernel')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 2d699b7855..c7acd792af 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1032,15 +1032,6 @@ let splay_arity env sigma c =
 
 let sort_of_arity env c = snd (splay_arity env Evd.empty c)
   
-let decomp_prod env sigma = 
-  let rec decrec m c =
-    match whd_betadeltaiota env sigma c with
-      | DOP0(Sort _) as x -> m,x
-      | DOP2(Prod,a,DLAM(n,c_0)) -> decrec (m+1) c_0
-      | _ -> error "decomp_prod: Not a product"
-  in 
-  decrec 0
-    
 let decomp_n_prod env sigma n = 
   let rec decrec m ln c = if m = 0 then (ln,c) else 
     match whd_betadeltaiota env sigma c with
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 0d2c39c5f5..fb623595a1 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -96,7 +96,6 @@ val hnf_lam_applist  : env -> 'a evar_map -> constr -> constr list -> constr
 val splay_prod : env -> 'a evar_map -> constr -> (name * constr) list * constr
 val splay_arity : env -> 'a evar_map -> constr -> (name * constr) list * sorts
 val sort_of_arity : env -> constr -> sorts
-val decomp_prod : env -> 'a evar_map -> constr -> int * constr
 val decomp_n_prod : 
   env -> 'a evar_map -> int -> constr -> ((name * constr) list) * constr
 
-- 
cgit v1.2.3