diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-24 10:27:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-12-14 15:57:51 +0100 |
| commit | c248228f5e910e19114e827661abb255c77a2b01 (patch) | |
| tree | 4bb1ba77ed70893c67015e46599bf38ac70d8ad0 | |
| parent | 63d582c6cd12bc3f8134a5aa9e3bdbca0dd2e9ca (diff) | |
Cosmetic: using "types" rather "constr" in some types of term.mli.
This enforces the intended meaning of the corresponding functions
(prod_appvect*/prod_applist*).
| -rw-r--r-- | kernel/term.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index b0b5a15ac..a48d3de9e 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. } *) |