diff options
Diffstat (limited to 'kernel/instantiate.mli')
| -rw-r--r-- | kernel/instantiate.mli | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli new file mode 100644 index 0000000000..e0279abb1a --- /dev/null +++ b/kernel/instantiate.mli @@ -0,0 +1,19 @@ + +(* $Id$ *) + +open Names +open Term +open Environ + +val instantiate_constr : + identifier list -> constr -> constr list -> constr +val instantiate_type : + identifier list -> typed_type -> constr list -> typed_type + +val constant_value : 'a unsafe_env -> constr -> constr +val constant_type : 'a unsafe_env -> constr -> typed_type + +val const_or_ex_value : 'a unsafe_env -> constr -> constr +val const_or_ex_type : 'a unsafe_env -> constr -> constr + +val const_abst_opt_value : 'a unsafe_env -> constr -> constr option |