diff options
Diffstat (limited to 'library/libnames.mli')
| -rw-r--r-- | library/libnames.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/library/libnames.mli b/library/libnames.mli index 92dd9cb28..b93ee87ee 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -24,6 +24,14 @@ type global_reference = | ConstructRef of constructor val isVarRef : global_reference -> bool +val isConstRef : global_reference -> bool +val isIndRef : global_reference -> bool +val isConstructRef : global_reference -> bool + +val destVarRef : global_reference -> variable +val destConstRef : global_reference -> constant +val destIndRef : global_reference -> inductive +val destConstructRef : global_reference -> constructor val subst_constructor : substitution -> constructor -> constructor * constr val subst_global : substitution -> global_reference -> global_reference * constr |