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

---
 plugins/funind/indfun_common.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/funind/indfun_common.ml')

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 76f8c6d219..738ade8ca3 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -108,7 +108,7 @@ let const_of_id id =
   let _,princ_ref =
     qualid_of_reference (Libnames.Ident (Loc.ghost,id))
   in
-  try Nametab.locate_constant princ_ref
+  try Constrintern.locate_reference princ_ref
   with Not_found -> Errors.error ("cannot find "^ Id.to_string id)
 
 let def_of_const t =
@@ -380,9 +380,9 @@ let find_Function_of_graph ind =
   Indmap.find ind !from_graph
 
 let update_Function finfo =
-(*   Pp.msgnl (pr_info finfo); *)
+  (* Pp.msgnl (pr_info finfo); *)
   Lib.add_anonymous_leaf (in_Function finfo)
-
+			 
 
 let add_Function is_general f =
   let f_id = Label.to_id (con_label f) in
-- 
cgit v1.2.3