From 6f40831dc1d0fecfbaf9fbc8116da0e74b6e8726 Mon Sep 17 00:00:00 2001
From: jforest
Date: Thu, 9 Apr 2015 22:19:31 +0200
Subject: Function now supports puniveres

---
 interp/constrintern.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'interp')

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
-- 
cgit v1.2.3