diff options
Diffstat (limited to 'library/libnames.mli')
| -rw-r--r-- | library/libnames.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/library/libnames.mli b/library/libnames.mli index 890a442e3..399387dd7 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -25,6 +25,7 @@ type global_reference = val isVarRef : global_reference -> bool +val subst_constructor : substitution -> constructor -> constructor * constr val subst_global : substitution -> global_reference -> global_reference * constr (* Turn a global reference into a construction *) |