diff options
Diffstat (limited to 'kernel/instantiate.ml')
| -rw-r--r-- | kernel/instantiate.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml index ab818d0e52..e6a25e6a3c 100644 --- a/kernel/instantiate.ml +++ b/kernel/instantiate.ml @@ -26,7 +26,7 @@ let instantiate_constr sign c args = replace_vars inst c let instantiate_type sign tty args = - typed_app (fun c -> instantiate_constr sign c args) tty + type_app (fun c -> instantiate_constr sign c args) tty (* Constants. *) |