diff options
Diffstat (limited to 'kernel/instantiate.mli')
| -rw-r--r-- | kernel/instantiate.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli index e0279abb1a..0bcdabf6d2 100644 --- a/kernel/instantiate.mli +++ b/kernel/instantiate.mli @@ -1,9 +1,13 @@ (* $Id$ *) +(*i*) open Names open Term open Environ +(*i*) + +(* Instantiation of constants and inductives on their real arguments. *) val instantiate_constr : identifier list -> constr -> constr list -> constr |