aboutsummaryrefslogtreecommitdiff
path: root/engine/eConstr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/eConstr.mli')
-rw-r--r--engine/eConstr.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index e6270fa78f..cb671154c6 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -69,7 +69,7 @@ val mkInd : inductive -> t
val mkIndU : pinductive -> t
val mkConstruct : constructor -> t
val mkConstructU : pconstructor -> t
-(* val mkConstructUi : pinductive * int -> t *)
+val mkConstructUi : pinductive * int -> t
val mkCase : case_info * t * t * t array -> t
val mkFix : (t, t) pfixpoint -> t
val mkCoFix : (t, t) pcofixpoint -> t