diff options
Diffstat (limited to 'toplevel/libtypes.mli')
| -rw-r--r-- | toplevel/libtypes.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/libtypes.mli b/toplevel/libtypes.mli index a6a95ccfc..d3944c180 100644 --- a/toplevel/libtypes.mli +++ b/toplevel/libtypes.mli @@ -13,7 +13,7 @@ open Term (** results are the reference of the object, together with a context (constr+evar) and a substitution under this context *) -type result = Libnames.global_reference * (constr*existential_key) * Termops.subst +type result = Globnames.global_reference * (constr*existential_key) * Termops.subst (** this is the reduction function used in the indexing process *) val reduce : types -> types |