From 0d03f17a33b43aa87bb201953e4e1a567aac6355 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 31 Dec 2008 10:57:09 +0000
Subject: Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod
 -> splay_prod_n, lam_it -> it_mkLambda, splay_lambda -> splay_lam). Added
 shortcuts for "fst (decompose_prod t)" and co.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11727 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/reductionops.ml | 26 ++++++++++++++++++--------
 1 file changed, 18 insertions(+), 8 deletions(-)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 4bb9a9a5dc..f51820bf62 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -750,7 +750,7 @@ let splay_prod env sigma =
   in 
   decrec env []
 
-let splay_lambda env sigma = 
+let splay_lam env sigma = 
   let rec decrec env m c =
     let t = whd_betadeltaiota env sigma c in
     match kind_of_term t with
@@ -767,14 +767,14 @@ let splay_prod_assum env sigma =
     match kind_of_term t with
     | Prod (x,t,c)  ->
 	prodec_rec (push_rel (x,None,t) env)
-	  (Sign.add_rel_decl (x, None, t) l) c
+	  (add_rel_decl (x, None, t) l) c
     | LetIn (x,b,t,c) ->
 	prodec_rec (push_rel (x, Some b, t) env)
-	  (Sign.add_rel_decl (x, Some b, t) l) c
+	  (add_rel_decl (x, Some b, t) l) c
     | Cast (c,_,_)    -> prodec_rec env l c
     | _               -> l,t
   in
-  prodec_rec env Sign.empty_rel_context
+  prodec_rec env empty_rel_context
 
 let splay_arity env sigma c =
   let l, c = splay_prod env sigma c in
@@ -784,15 +784,25 @@ let splay_arity env sigma c =
 
 let sort_of_arity env c = snd (splay_arity env Evd.empty c)
 
-let decomp_n_prod env sigma n = 
+let splay_prod_n env sigma n = 
   let rec decrec env m ln c = if m = 0 then (ln,c) else 
     match kind_of_term (whd_betadeltaiota env sigma c) with
       | Prod (n,a,c0) ->
 	  decrec (push_rel (n,None,a) env)
-	    (m-1) (Sign.add_rel_decl (n,None,a) ln) c0
-      | _                      -> invalid_arg "decomp_n_prod"
+	    (m-1) (add_rel_decl (n,None,a) ln) c0
+      | _                      -> invalid_arg "splay_prod_n"
   in 
-  decrec env n Sign.empty_rel_context
+  decrec env n empty_rel_context
+
+let splay_lam_n env sigma n = 
+  let rec decrec env m ln c = if m = 0 then (ln,c) else 
+    match kind_of_term (whd_betadeltaiota env sigma c) with
+      | Lambda (n,a,c0) ->
+	  decrec (push_rel (n,None,a) env)
+	    (m-1) (add_rel_decl (n,None,a) ln) c0
+      | _                      -> invalid_arg "splay_lam_n"
+  in 
+  decrec env n empty_rel_context
 
 exception NotASort
 
-- 
cgit v1.2.3