aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-11 20:29:16 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-28 14:16:52 +0200
commit0ade32f84b28d2190360ec79520788142755b5b7 (patch)
tree46b2d11c817707c3b84653b490de3b0aaad42038 /engine
parentbd8606189268c3fcdd3506872d459cb9032a33bf (diff)
[api] Deprecate a couple of aliases that we missed.
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 28c9dd3c2..8ee3b9050 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -108,7 +108,7 @@ val mkLetIn : Name.t * t * t * t -> t
val mkApp : t * t array -> t
val mkConst : Constant.t -> t
val mkConstU : Constant.t * EInstance.t -> t
-val mkProj : (projection * t) -> t
+val mkProj : (Projection.t * t) -> t
val mkInd : inductive -> t
val mkIndU : inductive * EInstance.t -> t
val mkConstruct : constructor -> t
@@ -173,7 +173,7 @@ val destEvar : Evd.evar_map -> t -> t pexistential
val destInd : Evd.evar_map -> t -> inductive * EInstance.t
val destConstruct : Evd.evar_map -> t -> constructor * EInstance.t
val destCase : Evd.evar_map -> t -> case_info * t * t * t array
-val destProj : Evd.evar_map -> t -> projection * t
+val destProj : Evd.evar_map -> t -> Projection.t * t
val destFix : Evd.evar_map -> t -> (t, t) pfixpoint
val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint