1 files changed, 24 insertions, 11 deletions

diff --git a/kernel/term.mli b/kernel/term.mli
index d60716410c..972a67ebed 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -262,14 +262,34 @@ val to_lambda : int -> constr -> constr
    where [l] is [fun (x_1:T_1)...(x_n:T_n) => T] *)
 val to_prod : int -> constr -> constr
 
+val it_mkLambda_or_LetIn : constr -> rel_context -> constr
+val it_mkProd_or_LetIn : types -> rel_context -> types
+
+(** In [lambda_applist c args], [c] is supposed to have the form
+    [λΓ.c] with [Γ] without let-in; it returns [c] with the variables
+    of [Γ] instantiated by [args]. *)
+val lambda_applist : constr -> constr list -> constr
+val lambda_appvect : constr -> constr array -> constr
+
+(** In [lambda_applist_assum n c args], [c] is supposed to have the
+    form [λΓ.c] with [Γ] of length [m] and possibly with let-ins; it
+    returns [c] with the assumptions of [Γ] instantiated by [args] and
+    the local definitions of [Γ] expanded. *)
+val lambda_applist_assum : int -> constr -> constr list -> constr
+val lambda_appvect_assum : int -> constr -> constr array -> constr
+
 (** pseudo-reduction rule *)
 
 (** [prod_appvect] [forall (x1:B1;...;xn:Bn), B] [a1...an] @return [B[a1...an]] *)
 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
+(** In [prod_appvect_assum n c args], [c] is supposed to have the
+    form [∀Γ.c] with [Γ] of length [m] and possibly with let-ins; it
+    returns [c] with the assumptions of [Γ] instantiated by [args] and
+    the local definitions of [Γ] expanded. *)
+val prod_appvect_assum : int -> constr -> constr array -> constr
+val prod_applist_assum : int -> constr -> constr list -> constr
 
 (** {5 Other term destructors. } *)
 
@@ -308,13 +328,6 @@ val decompose_lam_n_assum : int -> constr -> rel_context * constr
 (** Idem, counting let-ins *)
 val decompose_lam_n_decls : 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 *)
-val nb_prod : constr -> int
-
 (** Return the premisses/parameters of a type/term (let-in included) *)
 val prod_assum : types -> rel_context
 val lam_assum : constr -> rel_context
@@ -436,11 +449,11 @@ val eq_constr : constr -> constr -> bool
 
 (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts,
    application grouping and the universe constraints in [u]. *)
-val eq_constr_univs : constr Univ.check_function
+val eq_constr_univs : constr UGraph.check_function
 
 (** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo 
     alpha, casts, application grouping and the universe constraints in [u]. *)
-val leq_constr_univs : constr Univ.check_function
+val leq_constr_univs : constr UGraph.check_function
 
 (** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts,
    application grouping and ignoring universe instances. *)