diff options
| author | jforest | 2015-04-09 22:19:31 +0200 |
|---|---|---|
| committer | jforest | 2015-04-14 20:56:32 +0200 |
| commit | 6f40831dc1d0fecfbaf9fbc8116da0e74b6e8726 (patch) | |
| tree | 64e84a45fc215d458bc220366399f65ef67307ae /interp | |
| parent | efbc8eef69dd66c51d7f4b666d7b3ffeb99a35c7 (diff) | |
Function now supports puniveres
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 792e6f6322..0d33d43345 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -174,6 +174,7 @@ val interp_context_evars : (** Locating references of constructions, possibly via a syntactic definition (these functions do not modify the glob file) *) +val locate_reference : Libnames.qualid -> Globnames.global_reference val is_global : Id.t -> bool val construct_reference : named_context -> Id.t -> constr val global_reference : Id.t -> constr |