Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 229 insertions, 96 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 1f3d2635..68565659 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: term.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id$ *)
 
 (* This module instantiates the structure of generic deBruijn terms to Coq *)
 
@@ -26,7 +26,7 @@ type metavariable = int
 (* This defines Cases annotations *)
 type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
 type case_printing =
-  { ind_nargs : int; (* number of real args of the inductive type *)
+  { ind_nargs : int; (* length of the arity of the inductive type *)
     style     : case_style }
 type case_info =
   { ci_ind        : inductive;
@@ -42,7 +42,7 @@ type contents = Pos | Null
 type sorts =
   | Prop of contents                      (* proposition types *)
   | Type of universe
-      
+
 let prop_sort = Prop Null
 let set_sort = Prop Pos
 let type1_sort = Type type1_univ
@@ -58,7 +58,7 @@ let family_of_sort = function
 (*       Constructions as implemented                               *)
 (********************************************************************)
 
-type cast_kind = VMcast | DEFAULTcast 
+type cast_kind = VMcast | DEFAULTcast
 
 (* [constr array] is an instance matching definitional [named_context] in
    the same order (i.e. last argument first) *)
@@ -93,7 +93,7 @@ type ('constr, 'types) kind_of_term =
 (* Experimental *)
 type ('constr, 'types) kind_of_type =
   | SortType   of sorts
-  | CastType   of 'types * 'types 
+  | CastType   of 'types * 'types
   | ProdType   of name * 'types * 'types
   | LetInType  of name * 'constr * 'types * 'types
   | AtomicType of 'constr * 'constr array
@@ -118,7 +118,7 @@ type fixpoint = (int array * int) * rec_declaration
 type cofixpoint = int * rec_declaration
 
 (***************************)
-(* hash-consing functions  *)                         
+(* hash-consing functions  *)
 (***************************)
 
 let comp_term t1 t2 =
@@ -184,7 +184,7 @@ module Hconstr =
       type t = constr
       type u = (constr -> constr) *
                ((sorts -> sorts) * (constant -> constant) *
-               (kernel_name -> kernel_name) * (name -> name) *
+               (mutual_inductive -> mutual_inductive) * (name -> name) *
                (identifier -> identifier))
       let hash_sub = hash_term
       let equal = comp_term
@@ -211,7 +211,7 @@ let mkVar id = Var id
 let mkSort s = Sort s
 
 (* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *)
-(* (that means t2 is declared as the type of t1) 
+(* (that means t2 is declared as the type of t1)
    [s] is the strategy to use when *)
 let mkCast (t1,k2,t2) =
   match t1 with
@@ -230,14 +230,14 @@ let mkLetIn (x,c1,t,c2) = LetIn (x,c1,t,c2)
 (* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *)
 (* We ensure applicative terms have at least one argument and the
    function is not itself an applicative term *)
-let mkApp (f, a) = 
+let mkApp (f, a) =
   if Array.length a = 0 then f else
     match f with
       | App (g, cl) -> App (g, Array.append cl a)
       | _ -> App (f, a)
 
 
-(* Constructs a constant *) 
+(* Constructs a constant *)
 (* The array of terms correspond to the variables introduced in the section *)
 let mkConst c = Const c
 
@@ -248,7 +248,7 @@ let mkEvar e = Evar e
 (* The array of terms correspond to the variables introduced in the section *)
 let mkInd m = Ind m
 
-(* Constructs the jth constructor of the ith (co)inductive type of the 
+(* Constructs the jth constructor of the ith (co)inductive type of the
    block named kn. The array of terms correspond to the variables
    introduced in the section *)
 let mkConstruct c = Construct c
@@ -261,6 +261,7 @@ let mkFix fix = Fix fix
 let mkCoFix cofix = CoFix cofix
 
 let kind_of_term c = c
+let kind_of_term2 c = c
 
 (************************************************************************)
 (*    kind_of_term = constructions as seen by the user                 *)
@@ -284,7 +285,7 @@ type hnftype =
 (*          Non primitive term destructors                            *)
 (**********************************************************************)
 
-(* Destructor operations : partial functions 
+(* Destructor operations : partial functions
    Raise invalid_arg "dest*" if the const has not the expected form *)
 
 (* Destructs a DeBrujin index *)
@@ -348,8 +349,12 @@ let same_kind c1 c2 = (isprop c1 & isprop c2) or (is_Type c1 & is_Type c2)
 (* Tests if an evar *)
 let isEvar c = match kind_of_term c with Evar _ -> true | _ -> false
 
+let isEvar_or_Meta c = match kind_of_term c with
+  | Evar _ | Meta _ -> true
+  | _ -> false
+
 (* Destructs a casted term *)
-let destCast c = match kind_of_term c with 
+let destCast c = match kind_of_term c with
   | Cast (t1,k,t2) -> (t1,k,t2)
   | _ -> invalid_arg "destCast"
 
@@ -366,22 +371,22 @@ let isVar c = match kind_of_term c with Var _ -> true | _ -> false
 let isInd c = match kind_of_term c with Ind _ -> true | _ -> false
 
 (* Destructs the product (x:t1)t2 *)
-let destProd c = match kind_of_term c with 
-  | Prod (x,t1,t2) -> (x,t1,t2) 
+let destProd c = match kind_of_term c with
+  | Prod (x,t1,t2) -> (x,t1,t2)
   | _ -> invalid_arg "destProd"
 
 let isProd c = match kind_of_term c with | Prod _ -> true | _ -> false
 
 (* Destructs the abstraction [x:t1]t2 *)
-let destLambda c = match kind_of_term c with 
-  | Lambda (x,t1,t2) -> (x,t1,t2) 
+let destLambda c = match kind_of_term c with
+  | Lambda (x,t1,t2) -> (x,t1,t2)
   | _ -> invalid_arg "destLambda"
 
 let isLambda c = match kind_of_term c with | Lambda _ -> true | _ -> false
 
 (* Destructs the let [x:=b:t1]t2 *)
-let destLetIn c = match kind_of_term c with 
-  | LetIn (x,b,t1,t2) -> (x,b,t1,t2) 
+let destLetIn c = match kind_of_term c with
+  | LetIn (x,b,t1,t2) -> (x,b,t1,t2)
   | _ -> invalid_arg "destProd"
 
 let isLetIn c =  match kind_of_term c with LetIn _ -> true | _ -> false
@@ -430,13 +435,13 @@ let destCase c = match kind_of_term c with
 
 let isCase c =  match kind_of_term c with Case _ -> true | _ -> false
 
-let destFix c = match kind_of_term c with 
+let destFix c = match kind_of_term c with
   | Fix fix -> fix
   | _ -> invalid_arg "destFix"
 
 let isFix c =  match kind_of_term c with Fix _ -> true | _ -> false
 
-let destCoFix c = match kind_of_term c with 
+let destCoFix c = match kind_of_term c with
   | CoFix cofix -> cofix
   | _ -> invalid_arg "destCoFix"
 
@@ -466,7 +471,7 @@ let rec under_casts f c = match kind_of_term c with
 
 (* flattens application lists throwing casts in-between *)
 let rec collapse_appl c = match kind_of_term c with
-  | App (f,cl) -> 
+  | App (f,cl) ->
       let rec collapse_rec f cl2 =
         match kind_of_term (strip_outer_cast f) with
 	| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
@@ -482,12 +487,12 @@ let decompose_app c =
 
 (* strips head casts and flattens head applications *)
 let rec strip_head_cast c = match kind_of_term c with
-  | App (f,cl) -> 
+  | App (f,cl) ->
       let rec collapse_rec f cl2 = match kind_of_term f with
 	| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
 	| Cast (c,_,_) -> collapse_rec c cl2
 	| _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2)
-      in 
+      in
       collapse_rec f cl
   | Cast (c,_,_) -> strip_head_cast c
   | _ -> c
@@ -550,7 +555,7 @@ let iter_constr_with_binders g f n c = match kind_of_term c with
   | App (c,l) -> f n c; Array.iter (f n) l
   | Evar (_,l) -> Array.iter (f n) l
   | Case (_,p,c,bl) -> f n p; f n c; Array.iter (f n) bl
-  | Fix (_,(_,tl,bl)) -> 
+  | Fix (_,(_,tl,bl)) ->
       Array.iter (f n) tl;
       Array.iter (f (iterate g (Array.length tl) n)) bl
   | CoFix (_,(_,tl,bl)) ->
@@ -604,6 +609,7 @@ let map_constr_with_binders g f l c = match kind_of_term c with
    application associativity, binders name and Cases annotations are
    not taken into account *)
 
+
 let compare_constr f t1 t2 =
   match kind_of_term t1, kind_of_term t2 with
   | Rel n1, Rel n2 -> n1 = n2
@@ -619,15 +625,15 @@ let compare_constr f t1 t2 =
       if Array.length l1 = Array.length l2 then
         f c1 c2 & array_for_all2 f l1 l2
       else
-        let (h1,l1) = decompose_app t1 in        
+        let (h1,l1) = decompose_app t1 in
         let (h2,l2) = decompose_app t2 in
         if List.length l1 = List.length l2 then
           f h1 h2 & List.for_all2 f l1 l2
         else false
   | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2
-  | Const c1, Const c2 -> c1 = c2
-  | Ind c1, Ind c2 -> c1 = c2
-  | Construct c1, Construct c2 -> c1 = c2
+  | Const c1, Const c2 -> eq_constant c1 c2
+  | Ind c1, Ind c2 -> eq_ind c1 c2
+  | Construct c1, Construct c2 -> eq_constructor c1 c2
   | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
       f p1 p2 & f c1 c2 & array_for_all2 f bl1 bl2
   | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
@@ -642,7 +648,7 @@ let compare_constr f t1 t2 =
 
 type types = constr
 
-type strategy = types option 
+type strategy = types option
 
 type named_declaration = identifier * constr option * types
 type rel_declaration = name * constr option * types
@@ -653,6 +659,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                     *)
 (****************************************************************************)
@@ -666,11 +700,11 @@ exception LocalOccur
 (* (closedn n M) raises FreeVar if a variable of height greater than n
    occurs in M, returns () otherwise *)
 
-let closedn n c = 
+let closedn n c =
   let rec closed_rec n c = match kind_of_term c with
     | Rel m -> if m>n then raise LocalOccur
     | _ -> iter_constr_with_binders succ closed_rec n c
-  in 
+  in
   try closed_rec n c; true with LocalOccur -> false
 
 (* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
@@ -679,21 +713,21 @@ let closed0 = closedn 0
 
 (* (noccurn n M) returns true iff (Rel n) does NOT occur in term M  *)
 
-let noccurn n term = 
+let noccurn n term =
   let rec occur_rec n c = match kind_of_term c with
     | Rel m -> if m = n then raise LocalOccur
     | _ -> iter_constr_with_binders succ occur_rec n c
-  in 
+  in
   try occur_rec n term; true with LocalOccur -> false
 
-(* (noccur_between n m M) returns true iff (Rel p) does NOT occur in term M 
+(* (noccur_between n m M) returns true iff (Rel p) does NOT occur in term M
   for n <= p < n+m *)
 
-let noccur_between n m term = 
+let noccur_between n m term =
   let rec occur_rec n c = match kind_of_term c with
     | Rel(p) -> if n<=p && p<n+m then raise LocalOccur
     | _        -> iter_constr_with_binders succ occur_rec n c
-  in 
+  in
   try occur_rec n term; true with LocalOccur -> false
 
 (* Checking function for terms containing existential variables.
@@ -703,7 +737,7 @@ let noccur_between n m term =
  which may contain the CoFix variables. These occurrences of CoFix variables
  are not considered *)
 
-let noccur_with_meta n m term = 
+let noccur_with_meta n m term =
   let rec occur_rec n c = match kind_of_term c with
     | Rel p -> if n<=p & p<n+m then raise LocalOccur
     | App(f,cl) ->
@@ -728,18 +762,18 @@ let rec exliftn el c = match kind_of_term c with
 
 (* Lifting the binding depth across k bindings *)
 
-let liftn k n = 
+let liftn k n =
   match el_liftn (pred n) (el_shft k ELID) with
     | ELID -> (fun c -> c)
     | el -> exliftn el
- 
+
 let lift k = liftn k 1
 
 (*********************)
 (*   Substituting    *)
 (*********************)
 
-(* (subst1 M c) substitutes M for Rel(1) in c 
+(* (subst1 M c) substitutes M for Rel(1) in c
    we generalise it to (substl [M1,...,Mn] c) which substitutes in parallel
    M1,...,Mn for respectively Rel(1),...,Rel(n) in c *)
 
@@ -759,15 +793,15 @@ let rec lift_substituend depth s =
 let make_substituend c = { sinfo=Unknown; sit=c }
 
 let substn_many lamv n c =
-  let lv = Array.length lamv in 
+  let lv = Array.length lamv in
   if lv = 0 then c
-  else 
+  else
     let rec substrec depth c = match kind_of_term c with
       | Rel k     ->
           if k<=depth then c
           else if k-depth <= lv then lift_substituend depth lamv.(k-depth-1)
           else mkRel (k-lv)
-      | _ -> map_constr_with_binders succ substrec depth c in 
+      | _ -> map_constr_with_binders succ substrec depth c in
     substrec n c
 
 (*
@@ -791,21 +825,21 @@ let substl_named_decl = substl_decl
 
 let rec thin_val = function
   | [] -> []
-  | (((id,{ sit = v }) as s)::tl) when isVar v -> 
+  | (((id,{ sit = v }) as s)::tl) when isVar v ->
       if id = destVar v then thin_val tl else s::(thin_val tl)
   | h::tl -> h::(thin_val tl)
 
 (* (replace_vars sigma M) applies substitution sigma to term M *)
-let replace_vars var_alist = 
+let replace_vars var_alist =
   let var_alist =
     List.map (fun (str,c) -> (str,make_substituend c)) var_alist in
-  let var_alist = thin_val var_alist in 
+  let var_alist = thin_val var_alist in
   let rec substrec n c = match kind_of_term c with
     | Var x ->
         (try lift_substituend n (List.assoc x var_alist)
          with Not_found -> c)
     | _ -> map_constr_with_binders succ substrec n c
-  in 
+  in
   if var_alist = [] then (function x -> x) else substrec 0
 
 (*
@@ -910,7 +944,7 @@ let mkAppA v =
   if l=0 then anomaly "mkAppA received an empty array"
   else mkApp (v.(0), Array.sub v 1 (Array.length v -1))
 
-(* Constructs a constant *) 
+(* Constructs a constant *)
 (* The array of terms correspond to the variables introduced in the section *)
 let mkConst = mkConst
 
@@ -921,7 +955,7 @@ let mkEvar = mkEvar
 (* The array of terms correspond to the variables introduced in the section *)
 let mkInd = mkInd
 
-(* Constructs the jth constructor of the ith (co)inductive type of the 
+(* Constructs the jth constructor of the ith (co)inductive type of the
    block named kn. The array of terms correspond to the variables
    introduced in the section *)
 let mkConstruct = mkConstruct
@@ -930,15 +964,15 @@ let mkConstruct = mkConstruct
 let mkCase = mkCase
 let mkCaseL (ci, p, c, ac) = mkCase (ci, p, c, Array.of_list ac)
 
-(* If recindxs = [|i1,...in|] 
+(* If recindxs = [|i1,...in|]
       funnames = [|f1,...fn|]
       typarray = [|t1,...tn|]
       bodies   = [|b1,...bn|]
-   then    
+   then
 
       mkFix ((recindxs,i),(funnames,typarray,bodies))
-   
-   constructs the ith function of the block  
+
+   constructs the ith function of the block
 
     Fixpoint f1 [ctx1] : t1 := b1
     with     f2 [ctx2] : t2 := b2
@@ -953,12 +987,12 @@ let mkFix = mkFix
 (* If funnames = [|f1,...fn|]
       typarray = [|t1,...tn|]
       bodies   = [|b1,...bn|]
-   then 
+   then
 
       mkCoFix (i,(funnames,typsarray,bodies))
 
-   constructs the ith function of the block  
-   
+   constructs the ith function of the block
+
     CoFixpoint f1 : t1 := b1
     with       f2 : t2 := b2
     ...
@@ -984,7 +1018,7 @@ let prodn n env b =
     | (0, env, b)        -> b
     | (n, ((v,t)::l), b) -> prodrec (n-1,  l, mkProd (v,t,b))
     | _ -> assert false
-  in 
+  in
   prodrec (n,env,b)
 
 (* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *)
@@ -996,7 +1030,7 @@ let lamn n env b =
     | (0, env, b)        -> b
     | (n, ((v,t)::l), b) -> lamrec (n-1,  l, mkLambda (v,t,b))
     | _ -> assert false
-  in 
+  in
   lamrec (n,env,b)
 
 (* compose_lam [xn:Tn;..;x1:T1] b = [x1:T1]..[xn:Tn]b *)
@@ -1007,29 +1041,29 @@ let applist (f,l) = mkApp (f, Array.of_list l)
 let applistc f l = mkApp (f, Array.of_list l)
 
 let appvect = mkApp
-	    
+
 let appvectc f l = mkApp (f,l)
-		     
+
 (* to_lambda n (x1:T1)...(xn:Tn)T =
  * [x1:T1]...[xn:Tn]T *)
 let rec to_lambda n prod =
-  if n = 0 then 
-    prod 
-  else 
-    match kind_of_term prod with 
+  if n = 0 then
+    prod
+  else
+    match kind_of_term prod with
       | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd)
       | Cast (c,_,_) -> to_lambda n c
-      | _   -> errorlabstrm "to_lambda" (mt ())                      
+      | _   -> errorlabstrm "to_lambda" (mt ())
 
 let rec to_prod n lam =
-  if n=0 then 
+  if n=0 then
     lam
-  else   
-    match kind_of_term lam with 
+  else
+    match kind_of_term lam with
       | Lambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd)
       | Cast (c,_,_) -> to_prod n c
-      | _   -> errorlabstrm "to_prod" (mt ())                      
-	    
+      | _   -> errorlabstrm "to_prod" (mt ())
+
 (* pseudo-reduction rule:
  * [prod_app  s (Prod(_,B)) N --> B[N]
  * with an strip_outer_cast on the first argument to produce a product *)
@@ -1048,91 +1082,190 @@ 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        *)
 (*********************************)
 
 (* 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 = 
+let decompose_prod =
   let rec prodec_rec l c = match kind_of_term c with
     | Prod (x,t,c) -> prodec_rec ((x,t)::l) c
     | Cast (c,_,_)   -> prodec_rec l c
     | _              -> l,c
-  in 
+  in
   prodec_rec []
 
 (* 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 = 
+let decompose_lam =
   let rec lamdec_rec l c = match kind_of_term c with
     | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c
     | Cast (c,_,_)     -> lamdec_rec l c
     | _                -> l,c
-  in 
+  in
   lamdec_rec []
 
-(* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T 
+(* 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 n =
   if n < 0 then error "decompose_prod_n: 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 
+  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 ((x,t)::l) (n-1) c
       | Cast (c,_,_)   -> prodec_rec l n c
       | _ -> error "decompose_prod_n: not enough products"
-  in 
-  prodec_rec [] n 
+  in
+  prodec_rec [] n
 
-(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T 
+(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T
    into the pair ([(xn,Tn);...;(x1,T1)],T) *)
 let decompose_lam_n n =
   if n < 0 then error "decompose_lam_n: 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 
+  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 ((x,t)::l) (n-1) c
       | Cast (c,_,_)     -> lamdec_rec l n c
       | _ -> error "decompose_lam_n: not enough abstractions"
-  in 
-  lamdec_rec [] 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 = 
+let nb_lam =
   let rec nbrec n c = match kind_of_term c with
     | Lambda (_,_,c) -> nbrec (n+1) c
     | Cast (c,_,_) -> nbrec n c
     | _ -> n
-  in 
+  in
   nbrec 0
-    
+
 (* similar to nb_lam, but gives the number of products instead *)
-let nb_prod = 
+let nb_prod =
   let rec nbrec n c = match kind_of_term c with
     | Prod (_,_,c) -> nbrec (n+1) c
     | Cast (c,_,_) -> nbrec n c
     | _ -> n
-  in 
+  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 *)                         
+(*  alpha conversion functions *)
 (*******************************)
 
 (* alpha conversion : ignore print names and casts *)
 
-let rec eq_constr m n = 
+let rec eq_constr m n =
   (m==n) or
   compare_constr eq_constr m n
 
 let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *)
 
 (*******************)
-(*  hash-consing   *)                         
+(*  hash-consing   *)
 (*******************)
 
 module Htype =