From c248228f5e910e19114e827661abb255c77a2b01 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 24 Sep 2017 10:27:03 +0200
Subject: Cosmetic: using "types" rather "constr" in some types of term.mli.

This enforces the intended meaning of the corresponding functions
(prod_appvect*/prod_applist*).
---
 kernel/term.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel')

diff --git a/kernel/term.mli b/kernel/term.mli
index b0b5a15ac9..a48d3de9ef 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -251,15 +251,15 @@ 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 prod_appvect : types -> constr array -> types
+val prod_applist : types -> constr list -> types
 
 (** In [prod_appvect_assum n c args], [c] is supposed to have the
     form [∀Γ.c] with [Γ] of length [n] 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
+val prod_appvect_assum : int -> types -> constr array -> types
+val prod_applist_assum : int -> types -> constr list -> types
 
 (** {5 Other term destructors. } *)
 
-- 
cgit v1.2.3