diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/libnames.ml | 8 | ||||
| -rw-r--r-- | library/libnames.mli | 8 | ||||
| -rwxr-xr-x | library/nametab.mli | 4 |
3 files changed, 18 insertions, 2 deletions
diff --git a/library/libnames.ml b/library/libnames.ml index c7d484d1e..0404d7cd8 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -23,6 +23,14 @@ type global_reference = | ConstructRef of constructor let isVarRef = function VarRef _ -> true | _ -> false +let isConstRef = function ConstRef _ -> true | _ -> false +let isIndRef = function IndRef _ -> true | _ -> false +let isConstructRef = function ConstructRef _ -> true | _ -> false + +let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef" +let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef" +let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef" +let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destConstructRef" let subst_constructor subst ((kn,i),j as ref) = let kn' = subst_kn subst kn in 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 diff --git a/library/nametab.mli b/library/nametab.mli index 5367bfdd8..774b148a5 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -21,12 +21,12 @@ open Libnames There are three classes of names: 1a- internal kernel names: [kernel_name], [constant], [inductive], - [module_path] + [module_path], [dir_path] 1b- other internal names: [global_reference], [syndef_name], [extended_global_reference], [global_dir_reference], ... - 2- full, non ambiguous user names: [full_path] and [dir_path] + 2- full, non ambiguous user names: [full_path] 3- non necessarily full, possibly ambiguous user names: [reference] and [qualid] |