From 0ade32f84b28d2190360ec79520788142755b5b7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 11 Mar 2018 20:29:16 +0100 Subject: [api] Deprecate a couple of aliases that we missed. --- kernel/constr.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel/constr.mli') diff --git a/kernel/constr.mli b/kernel/constr.mli index 98c0eaa28..0d464840c 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -122,7 +122,7 @@ val mkConst : Constant.t -> constr val mkConstU : pconstant -> constr (** Constructs a projection application *) -val mkProj : (projection * constr) -> constr +val mkProj : (Projection.t * constr) -> constr (** Inductive types *) @@ -220,7 +220,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint - | Proj of projection * 'constr + | Proj of Projection.t * 'constr (** User view of [constr]. For [App], it is ensured there is at least one argument and the function is not itself an applicative @@ -318,7 +318,7 @@ where [info] is pretty-printing information *) val destCase : constr -> case_info * constr * constr * constr array (** Destructs a projection *) -val destProj : constr -> projection * constr +val destProj : constr -> Projection.t * constr (** Destructs the {% $ %}i{% $ %}th function of the block [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1} -- cgit v1.2.3