diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.mli | 4 |
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 |