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

13 files changed, 212 insertions, 187 deletions

diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index d81b98ac4..26b997f0f 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -143,7 +143,7 @@ and slot_for_fv env fv =
 	match !rv with
 	| VKvalue (v, _) -> v
 	| VKnone -> 
-	    let (_, b, _) = Sign.lookup_rel i env.env_rel_context in
+	    let (_, b, _) = lookup_rel i env.env_rel_context in
 	    let (v, d) =
 	      match b with 
 		| None -> (val_of_rel i, Idset.empty)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 80c24058e..c43b63370 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -41,7 +41,7 @@ let empty_context env =
 
 (* Rel context *)
 let lookup_rel n env =
-  Sign.lookup_rel n env.env_rel_context
+  lookup_rel n env.env_rel_context
 
 let evaluable_rel n env =
   try
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index f09ba50ec..3452be55c 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -215,7 +215,7 @@ let typecheck_inductive env mie =
 	 let lev =
 	   (* Decide that if the conclusion is not explicitly Type *)
 	   (* then the inductive type is not polymorphic *)
-	   match kind_of_term (snd (decompose_prod_assum arity.utj_val)) with
+	   match kind_of_term ((strip_prod_assum arity.utj_val)) with
 	   | Sort (Type u) -> Some u
 	   | _ -> None in
          (cst,env_ar',(id,full_arity,lev)::l))
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 118d19830..d09cdbdb7 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -66,7 +66,7 @@ val type_case_branches :
     -> types array * types * constraints
 
 (* Return the arity of an inductive type *)
-val mind_arity : one_inductive_body -> Sign.rel_context * sorts_family
+val mind_arity : one_inductive_body -> rel_context * sorts_family
 
 val inductive_sort_family : one_inductive_body -> sorts_family
 
@@ -85,8 +85,8 @@ val type_of_inductive_knowing_parameters :
 
 val max_inductive_sort : sorts array -> universe
 
-val instantiate_universes : env -> Sign.rel_context ->
-    polymorphic_arity -> types array -> Sign.rel_context * sorts
+val instantiate_universes : env -> rel_context ->
+    polymorphic_arity -> types array -> rel_context * sorts
 
 (***************************************************************)
 (* Debug *)
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 8d45bb9e3..0c0126762 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -103,7 +103,7 @@ let push_named_context_val d (ctxt,vals) =
   let rval = ref VKnone in
     Sign.add_named_decl d ctxt, (id,rval)::vals
 
-exception ASSERT of Sign.rel_context
+exception ASSERT of rel_context
 
 let push_named d env = 
 (*  if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index e2e1e57d9..3d2f3e9b9 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -471,10 +471,10 @@ let dest_prod env =
     match kind_of_term t with
       | Prod (n,a,c0) ->
           let d = (n,None,a) in
-	  decrec (push_rel d env) (Sign.add_rel_decl d m) c0
+	  decrec (push_rel d env) (add_rel_decl d m) c0
       | _ -> m,t
   in 
-  decrec env Sign.empty_rel_context
+  decrec env empty_rel_context
 
 (* The same but preserving lets *)
 let dest_prod_assum env = 
@@ -483,14 +483,14 @@ let dest_prod_assum env =
     match kind_of_term rty with
     | Prod (x,t,c)  ->
         let d = (x,None,t) in
-	prodec_rec (push_rel d env) (Sign.add_rel_decl d l) c
+	prodec_rec (push_rel d env) (add_rel_decl d l) c
     | LetIn (x,b,t,c) ->
         let d = (x,Some b,t) in
-	prodec_rec (push_rel d env) (Sign.add_rel_decl d l) c
+	prodec_rec (push_rel d env) (add_rel_decl d l) c
     | Cast (c,_,_)    -> prodec_rec env l c
     | _               -> l,rty
   in
-  prodec_rec env Sign.empty_rel_context
+  prodec_rec env empty_rel_context
 
 let dest_arity env c =
   let l, c = dest_prod_assum env c in
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 2e344b217..6ac1591bb 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -70,8 +70,8 @@ val hnf_prod_applist : env -> types -> constr list -> types
 (************************************************************************)
 (*s Recognizing products and arities modulo reduction *)
 
-val dest_prod       : env -> types -> Sign.rel_context * types
-val dest_prod_assum : env -> types -> Sign.rel_context * types
+val dest_prod       : env -> types -> rel_context * types
+val dest_prod_assum : env -> types -> rel_context * types
 
-val dest_arity : env -> types -> Sign.arity
+val dest_arity : env -> types -> arity
 val is_arity   : env -> types -> bool
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 218ac6c48..d30d70860 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -43,31 +43,6 @@ let fold_named_context_reverse f ~init l = List.fold_left f init l
 (*s Signatures of ordered section variables *)
 type section_context = named_context
 
-(*s Signatures of ordered optionally named variables, intended to be
-   accessed by de Bruijn indices (to represent bound variables) *)
-
-type rel_declaration = name * constr option * types
-type rel_context = rel_declaration list
-
-let empty_rel_context = []
-
-let add_rel_decl d ctxt = d::ctxt
-
-let rec lookup_rel n sign =
-  match n, sign with
-  | 1, decl :: _ -> decl
-  | n, _ :: sign -> lookup_rel (n-1) sign
-  | _, []        -> raise Not_found
-
-let rel_context_length = List.length
-
-let rel_context_nhyps hyps =
-  let rec nhyps acc = function
-    | [] -> acc
-    | (_,None,_)::hyps -> nhyps (1+acc) hyps
-    | (_,Some _,_)::hyps -> nhyps acc hyps in
-  nhyps 0 hyps
-
 let fold_rel_context f l ~init:x = List.fold_right f l x
 let fold_rel_context_reverse f ~init:x l = List.fold_left f x l
 
@@ -102,98 +77,3 @@ let push_named_to_rel_context hyps ctxt =
 	(n+1), (map_rel_declaration (substn_vars n s) d)::ctxt
     | [] -> 1, hyps in
   snd (subst ctxt)
-
-
-(*********************************)
-(*       Term constructors       *)
-(*********************************)
-
-let it_mkProd_or_LetIn   = List.fold_left (fun c d -> mkProd_or_LetIn d c)
-let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c)
-
-(*********************************)
-(*       Term destructors        *)
-(*********************************)
-
-type arity = rel_context * sorts
-
-(* Decompose an arity (i.e. a product of the form (x1:T1)..(xn:Tn)s
-   with s a sort) into the pair ([(xn,Tn);...;(x1,T1)],s) *)
-
-let destArity = 
-  let rec prodec_rec l c =
-    match kind_of_term c with
-    | Prod (x,t,c)    -> prodec_rec ((x,None,t)::l) c
-    | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c
-    | Cast (c,_,_)      -> prodec_rec l c
-    | Sort s          -> l,s
-    | _               -> anomaly "destArity: not an arity"
-  in 
-  prodec_rec []
-
-let mkArity (sign,s) = it_mkProd_or_LetIn (mkSort s) sign
-
-let rec isArity c =
-  match kind_of_term c with
-  | Prod (_,_,c)    -> isArity c
-  | LetIn (_,b,_,c) -> isArity (subst1 b c)
-  | Cast (c,_,_)      -> isArity c
-  | Sort _          -> true
-  | _               -> false
-
-(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
-   ([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
-let decompose_prod_assum = 
-  let rec prodec_rec l c =
-    match kind_of_term c with
-    | Prod (x,t,c)    -> prodec_rec (add_rel_decl (x,None,t) l) c
-    | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) c
-    | Cast (c,_,_)      -> prodec_rec l c
-    | _               -> l,c
-  in 
-  prodec_rec empty_rel_context
-
-(* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair
-   ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)
-let decompose_lam_assum = 
-  let rec lamdec_rec l c =
-    match kind_of_term c with
-    | Lambda (x,t,c)  -> lamdec_rec (add_rel_decl (x,None,t) l) c
-    | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) c
-    | Cast (c,_,_)      -> lamdec_rec l c
-    | _               -> l,c
-  in 
-  lamdec_rec empty_rel_context
-
-(* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T 
-   into the pair ([(xn,Tn);...;(x1,T1)],T) *)
-let decompose_prod_n_assum n =
-  if n < 0 then
-    error "decompose_prod_n_assum: integer parameter must be positive";
-  let rec prodec_rec l n c = 
-    if n=0 then l,c
-    else match kind_of_term c with 
-    | Prod (x,t,c)    -> prodec_rec (add_rel_decl (x,None,t) l) (n-1) c
-    | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) (n-1) c
-    | Cast (c,_,_)      -> prodec_rec l n c
-    | c -> error "decompose_prod_n_assum: not enough assumptions"
-  in 
-  prodec_rec empty_rel_context n
-
-(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T 
-   into the pair ([(xn,Tn);...;(x1,T1)],T)
-   Lets in between are not expanded but turn into local definitions,
-   but n is the actual number of destructurated lambdas.  *)
-let decompose_lam_n_assum n =
-  if n < 0 then
-    error "decompose_lam_n_assum: integer parameter must be positive";
-  let rec lamdec_rec l n c = 
-    if n=0 then l,c 
-    else match kind_of_term c with 
-    | Lambda (x,t,c)  -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c
-    | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) n c
-    | Cast (c,_,_)      -> lamdec_rec l n c
-    | c -> error "decompose_lam_n_assum: not enough abstractions"
-  in 
-  lamdec_rec empty_rel_context n 
-
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 5d34c5ab4..b3e7ace55 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -40,16 +40,6 @@ val instance_from_named_context : named_context -> constr array
 (*s Signatures of ordered optionally named variables, intended to be
    accessed by de Bruijn indices *)
 
-(* In [rel_context], more recent declaration is on top *)
-type rel_context = rel_declaration list
-
-val empty_rel_context : rel_context
-val add_rel_decl : rel_declaration -> rel_context -> rel_context
-
-val lookup_rel : int -> rel_context -> rel_declaration
-val rel_context_length : rel_context -> int
-val rel_context_nhyps : rel_context -> int
-
 val push_named_to_rel_context : named_context -> rel_context -> rel_context
 
 (*s Recurrence on [rel_context]: older declarations processed first *)
@@ -70,35 +60,3 @@ val iter_rel_context : (constr -> unit) -> rel_context -> unit
 
 (*s Map function of [named_context] *)
 val iter_named_context : (constr -> unit) -> named_context -> unit
-
-(*s Term constructors *)
-
-val it_mkLambda_or_LetIn : constr -> rel_context -> constr
-val it_mkProd_or_LetIn : types -> rel_context -> types
-
-(*s Term destructors *)
-
-(* Destructs a term of the form $(x_1:T_1)..(x_n:T_n)s$ into the pair *)
-type arity = rel_context * sorts
-val destArity : types -> arity
-val mkArity : arity -> types
-val isArity : types -> bool
-
-(* Transforms a product term $(x_1:T_1)..(x_n:T_n)T$ including letins
-   into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a
-   product nor a let. *)
-val decompose_prod_assum : types -> rel_context * types
-
-(* Transforms a lambda term $[x_1:T_1]..[x_n:T_n]T$ including letins
-   into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a
-   lambda nor a let. *)
-val decompose_lam_assum : constr -> rel_context * constr
-
-(* Given a positive integer n, transforms a product term 
-   $(x_1:T_1)..(x_n:T_n)T$
-   into the pair $([(xn,Tn);...;(x1,T1)],T)$. *)
-val decompose_prod_n_assum : int -> types -> rel_context * types
-
-(* Given a positive integer $n$, transforms a lambda term 
-   $[x_1:T_1]..[x_n:T_n]T$ into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$ *)
-val decompose_lam_n_assum : int -> constr -> rel_context * constr
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 387d97de9..1f77c3e43 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -115,8 +115,7 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
       | Type _, Type _ -> (* shortcut here *) prop_sort, prop_sort
       | (Prop _, Type _) | (Type _,Prop _) -> error ()
       | _ -> (s1, s2) in
-    check_conv cst conv_leq env 
-      (Sign.mkArity (ctx1,s1)) (Sign.mkArity (ctx2,s2))
+    check_conv cst conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
   in
 
   let check_packet cst p1 p2 =
@@ -210,8 +209,8 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
        Hence they don't have to be checked again *)
 
     let t1,t2 = 
-      if Sign.isArity t2 then
-        let (ctx2,s2) = Sign.destArity t2 in
+      if isArity t2 then
+        let (ctx2,s2) = destArity t2 in
         match s2 with
         | Type v when not (is_univ_variable v) ->
           (* The type in the interface is inferred and is made of algebraic
@@ -222,13 +221,13 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
             | Type u when not (is_univ_variable u) ->
               (* Both types are inferred, no need to recheck them. We
                  cheat and collapse the types to Prop *)
-                Sign.mkArity (ctx1,prop_sort), Sign.mkArity (ctx2,prop_sort)
+                mkArity (ctx1,prop_sort), mkArity (ctx2,prop_sort)
             | Prop _ ->
               (* The type in the interface is inferred, it may be the case
                  that the type in the implementation is smaller because
                  the body is more reduced. We safely collapse the upper
                  type to Prop *)
-                Sign.mkArity (ctx1,prop_sort), Sign.mkArity (ctx2,prop_sort)
+                mkArity (ctx1,prop_sort), mkArity (ctx2,prop_sort)
             | Type _ ->
               (* The type in the interface is inferred and the type in the
                  implementation is not inferred or is inferred but from a
diff --git a/kernel/term.ml b/kernel/term.ml
index 49d7afa22..24879f41d 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -654,6 +654,34 @@ let map_rel_declaration = map_named_declaration
 let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a)
 let fold_rel_declaration = fold_named_declaration
 
+(***************************************************************************)
+(*     Type of local contexts (telescopes)                                 *)
+(***************************************************************************)
+
+(*s Signatures of ordered optionally named variables, intended to be
+   accessed by de Bruijn indices (to represent bound variables) *)
+
+type rel_context = rel_declaration list
+
+let empty_rel_context = []
+
+let add_rel_decl d ctxt = d::ctxt
+
+let rec lookup_rel n sign =
+  match n, sign with
+  | 1, decl :: _ -> decl
+  | n, _ :: sign -> lookup_rel (n-1) sign
+  | _, []        -> raise Not_found
+
+let rel_context_length = List.length
+
+let rel_context_nhyps hyps =
+  let rec nhyps acc = function
+    | [] -> acc
+    | (_,None,_)::hyps -> nhyps (1+acc) hyps
+    | (_,Some _,_)::hyps -> nhyps acc hyps in
+  nhyps 0 hyps
+
 (****************************************************************************)
 (*              Functions for dealing with constr terms                     *)
 (****************************************************************************)
@@ -1049,6 +1077,9 @@ let prod_appvect t nL = Array.fold_left prod_app t nL
 (* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *)
 let prod_applist t nL = List.fold_left prod_app t nL
 
+let it_mkProd_or_LetIn   = List.fold_left (fun c d -> mkProd_or_LetIn d c)
+let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c)
+
 (*********************************)
 (* Other term destructors        *)
 (*********************************)
@@ -1099,6 +1130,62 @@ let decompose_lam_n n =
   in 
   lamdec_rec [] n 
 
+(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
+   ([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
+let decompose_prod_assum = 
+  let rec prodec_rec l c =
+    match kind_of_term c with
+    | Prod (x,t,c)    -> prodec_rec (add_rel_decl (x,None,t) l) c
+    | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) c
+    | Cast (c,_,_)      -> prodec_rec l c
+    | _               -> l,c
+  in 
+  prodec_rec empty_rel_context
+
+(* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair
+   ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *)
+let decompose_lam_assum = 
+  let rec lamdec_rec l c =
+    match kind_of_term c with
+    | Lambda (x,t,c)  -> lamdec_rec (add_rel_decl (x,None,t) l) c
+    | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) c
+    | Cast (c,_,_)      -> lamdec_rec l c
+    | _               -> l,c
+  in 
+  lamdec_rec empty_rel_context
+
+(* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T 
+   into the pair ([(xn,Tn);...;(x1,T1)],T) *)
+let decompose_prod_n_assum n =
+  if n < 0 then
+    error "decompose_prod_n_assum: integer parameter must be positive";
+  let rec prodec_rec l n c = 
+    if n=0 then l,c
+    else match kind_of_term c with 
+    | Prod (x,t,c)    -> prodec_rec (add_rel_decl (x,None,t) l) (n-1) c
+    | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) (n-1) c
+    | Cast (c,_,_)      -> prodec_rec l n c
+    | c -> error "decompose_prod_n_assum: not enough assumptions"
+  in 
+  prodec_rec empty_rel_context n
+
+(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T 
+   into the pair ([(xn,Tn);...;(x1,T1)],T)
+   Lets in between are not expanded but turn into local definitions,
+   but n is the actual number of destructurated lambdas.  *)
+let decompose_lam_n_assum n =
+  if n < 0 then
+    error "decompose_lam_n_assum: integer parameter must be positive";
+  let rec lamdec_rec l n c = 
+    if n=0 then l,c 
+    else match kind_of_term c with 
+    | Lambda (x,t,c)  -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c
+    | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) n c
+    | Cast (c,_,_)      -> lamdec_rec l n c
+    | c -> error "decompose_lam_n_assum: not enough abstractions"
+  in 
+  lamdec_rec empty_rel_context n 
+
 (* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction
  * gives n (casts are ignored) *)
 let nb_lam = 
@@ -1118,7 +1205,47 @@ let nb_prod =
   in 
   nbrec 0
 
-(* Rem: end of import from old module Generic *)
+let prod_assum t = fst (decompose_prod_assum t)
+let prod_n_assum n t = fst (decompose_prod_n_assum n t)
+let strip_prod_assum t = snd (decompose_prod_assum t)
+let strip_prod t = snd (decompose_prod t)
+let strip_prod_n n t = snd (decompose_prod_n n t)
+let lam_assum t = fst (decompose_lam_assum t)
+let lam_n_assum n t = fst (decompose_lam_n_assum n t)
+let strip_lam_assum t = snd (decompose_lam_assum t)
+let strip_lam t = snd (decompose_lam t)
+let strip_lam_n n t = snd (decompose_lam_n n t)
+
+(***************************)
+(* Arities                 *)
+(***************************)
+
+(* An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort.
+   Such a term can canonically be seen as the pair of a context of types
+   and of a sort *)
+
+type arity = rel_context * sorts
+
+let destArity = 
+  let rec prodec_rec l c =
+    match kind_of_term c with
+    | Prod (x,t,c)    -> prodec_rec ((x,None,t)::l) c
+    | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c
+    | Cast (c,_,_)      -> prodec_rec l c
+    | Sort s          -> l,s
+    | _               -> anomaly "destArity: not an arity"
+  in 
+  prodec_rec []
+
+let mkArity (sign,s) = it_mkProd_or_LetIn (mkSort s) sign
+
+let rec isArity c =
+  match kind_of_term c with
+  | Prod (_,_,c)    -> isArity c
+  | LetIn (_,b,_,c) -> isArity (subst1 b c)
+  | Cast (c,_,_)      -> isArity c
+  | Sort _          -> true
+  | _               -> false
 
 (*******************************)
 (*  alpha conversion functions *)                         
diff --git a/kernel/term.mli b/kernel/term.mli
index 5d75df4bf..6a6a4ad28 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -331,6 +331,18 @@ val fold_named_declaration :
 val fold_rel_declaration :
   (constr -> 'a -> 'a) -> rel_declaration -> 'a -> 'a
 
+(*s Contexts of declarations referred to by de Bruijn indices *)
+
+(* In [rel_context], more recent declaration is on top *)
+type rel_context = rel_declaration list
+
+val empty_rel_context : rel_context
+val add_rel_decl : rel_declaration -> rel_context -> rel_context
+
+val lookup_rel : int -> rel_context -> rel_declaration
+val rel_context_length : rel_context -> int
+val rel_context_nhyps : rel_context -> int
+
 (* Constructs either [(x:t)c] or [[x=b:t]c] *)
 val mkProd_or_LetIn : rel_declaration -> types -> types
 val mkNamedProd_or_LetIn : named_declaration -> types -> types
@@ -368,7 +380,7 @@ val lamn : int -> (name * constr) list -> constr -> constr
 
 (* [compose_lam l b] = $[x_1:T_1]..[x_n:T_n]b$
    where $l = [(x_n,T_n);\dots;(x_1,T_1)]$.
-   Inverse of [decompose_lam] *)
+   Inverse of [it_destLam] *)
 val compose_lam : (name * constr) list -> constr -> constr
 
 (* [to_lambda n l] 
@@ -387,6 +399,9 @@ val to_prod : int -> constr -> constr
 val prod_appvect : constr -> constr array -> constr
 val prod_applist : constr -> constr list -> constr
 
+val it_mkLambda_or_LetIn : constr -> rel_context -> constr
+val it_mkProd_or_LetIn : types -> rel_context -> types
+
 (*s Other term destructors. *)
 
 (* Transforms a product term $(x_1:T_1)..(x_n:T_n)T$ into the pair
@@ -407,13 +422,44 @@ val decompose_prod_n : int -> constr -> (name * constr) list * constr
    $[x_1:T_1]..[x_n:T_n]T$ into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$ *)
 val decompose_lam_n : int -> constr -> (name * constr) list * constr
 
+(* Extract the premisses and the conclusion of a term of the form 
+   "(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let *)
+val decompose_prod_assum : types -> rel_context * types
+
+(* Idem with lambda's *)
+val decompose_lam_assum : constr -> rel_context * constr
+
+(* Idem but extract the first [n] premisses *)
+val decompose_prod_n_assum : int -> types -> rel_context * types
+val decompose_lam_n_assum : int -> constr -> rel_context * constr
+
 (* [nb_lam] $[x_1:T_1]...[x_n:T_n]c$ where $c$ is not an abstraction
    gives $n$ (casts are ignored) *)
 val nb_lam : constr -> int
 
-(* similar to [nb_lam], but gives the number of products instead *)
+(* Similar to [nb_lam], but gives the number of products instead *)
 val nb_prod : constr -> int
 
+(* Returns the premisses/parameters of a type/term (let-in included) *)
+val prod_assum : types -> rel_context
+val lam_assum : constr -> rel_context
+
+(* Returns the first n-th premisses/parameters of a type/term (let included)*)
+val prod_n_assum : int -> types -> rel_context
+val lam_n_assum : int -> constr -> rel_context
+
+(* Remove the premisses/parameters of a type/term *)
+val strip_prod : types -> types
+val strip_lam : constr -> constr
+
+(* Remove the first n-th premisses/parameters of a type/term *)
+val strip_prod_n : int -> types -> types
+val strip_lam_n : int -> constr -> constr
+
+(* Remove the premisses/parameters of a type/term (including let-in) *)
+val strip_prod_assum : types -> types
+val strip_lam_assum : constr -> constr
+
 (* flattens application lists *)
 val collapse_appl : constr -> constr
 
@@ -428,6 +474,21 @@ val under_casts : (constr -> constr) -> constr -> constr
 (* Apply a function under components of Cast if any *)
 val under_outer_cast : (constr -> constr) -> constr -> constr
 
+(*s An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort.
+    Such a term can canonically be seen as the pair of a context of types
+    and of a sort *)
+
+type arity = rel_context * sorts
+
+(* Build an "arity" from its canonical form *)
+val mkArity : arity -> types
+
+(* Destructs an "arity" into its canonical form *)
+val destArity : types -> arity
+
+(* Tells if a term has the form of an arity *)
+val isArity : types -> bool
+
 (*s Occur checks *)
 
 (* [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *)
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 5bb0dee1d..23c755690 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -25,7 +25,7 @@ val infer_type : env -> types        -> unsafe_type_judgment * constraints
 
 val infer_local_decls :
   env -> (identifier * local_entry) list
-    -> env * Sign.rel_context * constraints
+    -> env * rel_context * constraints
 
 (*s Basic operations of the typing machine. *)