diff options
Diffstat (limited to 'kernel/declarations.mli')
| -rw-r--r-- | kernel/declarations.mli | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 3a85e7e05f..3be72f3fd1 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -22,7 +22,7 @@ type constant_value = lazy_constant_value ref type constant_body = { const_kind : path_kind; const_body : constant_value option; - const_type : typed_type; + const_type : types; const_hyps : named_context; (* New: younger hyp at top *) const_constraints : constraints; mutable const_opaque : bool } @@ -56,10 +56,10 @@ type recarg = type one_inductive_body = { mind_consnames : identifier array; mind_typename : identifier; - mind_nf_lc : typed_type array; (* constrs and arity with pre-expanded ccl *) - mind_nf_arity : typed_type; - mind_user_lc : typed_type array option; - mind_user_arity : typed_type option; + mind_nf_lc : types array; (* constrs and arity with pre-expanded ccl *) + mind_nf_arity : types; + mind_user_lc : types array option; + mind_user_arity : types option; mind_sort : sorts; mind_nrealargs : int; mind_kelim : sorts list; @@ -76,8 +76,8 @@ type mutual_inductive_body = { mind_nparams : int } val mind_type_finite : mutual_inductive_body -> int -> bool -val mind_user_lc : one_inductive_body -> typed_type array -val mind_user_arity : one_inductive_body -> typed_type +val mind_user_lc : one_inductive_body -> types array +val mind_user_arity : one_inductive_body -> types val mind_nth_type_packet : mutual_inductive_body -> int -> one_inductive_body val mind_arities_context : mutual_inductive_body -> rel_declaration list |