diff options
Diffstat (limited to 'kernel/term.ml')
| -rw-r--r-- | kernel/term.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index d274857af5..49d7afa22e 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -261,6 +261,7 @@ let mkFix fix = Fix fix let mkCoFix cofix = CoFix cofix let kind_of_term c = c +let kind_of_term2 c = c (************************************************************************) (* kind_of_term = constructions as seen by the user *) |