aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/indtypes.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/indtypes.mli')
-rw-r--r--kernel/indtypes.mli5
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index ebb1e1f67..8a200aab0 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -3,6 +3,7 @@
(*i*)
open Names
+open Univ
open Term
open Inductive
open Environ
@@ -18,5 +19,5 @@ val sort_of_arity : 'a unsafe_env -> constr -> sorts
val cci_inductive :
'a unsafe_env -> 'a unsafe_env -> path_kind -> int -> bool ->
(identifier * typed_type * identifier list * bool * bool * constr) list ->
- mutual_inductive_body
-
+ constraints ->
+ mutual_inductive_body