diff options
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index d97bb916bb..a48384389d 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -47,7 +47,7 @@ type recarg = type one_inductive_body = { mind_consnames : identifier array; mind_typename : identifier; - mind_lc : constr array; + mind_lc : typed_type array; mind_arity : typed_type; mind_sort : sorts; mind_nrealargs : int; |