diff options
Diffstat (limited to 'checker/cic.mli')
| -rw-r--r-- | checker/cic.mli | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index 14fa7c774..59dd5bc4d 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -182,8 +182,6 @@ type ('a, 'b) declaration_arity = | RegularArity of 'a | TemplateArity of 'b -type constant_type = (constr, rel_context * template_arity) declaration_arity - (** Inlining level of parameters at functor applications. This is ignored by the checker. *) @@ -226,7 +224,7 @@ type typing_flags = { type constant_body = { const_hyps : section_context; (** New: younger hyp at top *) const_body : constant_def; - const_type : constant_type; + const_type : constr; const_body_code : to_patch_substituted; const_universes : constant_universes; const_proj : projection_body option; |