diff options
Diffstat (limited to 'kernel/term.ml')
| -rw-r--r-- | kernel/term.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index 3b6b69a289..ab678666fa 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -89,7 +89,7 @@ type ('constr, 'types) kind_of_term = ('constr, 'types) Constr.kind_of_term = | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint - | Proj of constant * 'constr + | Proj of projection * 'constr type values = Constr.values |