From ffa57bae1e18fd52d63e8512a352ac63db15a7a9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 6 Aug 2009 19:00:11 +0000
Subject: - Cleaning phase of the interfaces of libnames.ml and nametab.ml  
 (uniformisation of function names, classification). One of the most   visible
 change is the renaming of section_path into full_path (the   use of name
 section was obsolete due to the module system, but I   don't know if the new
 name is the best chosen one - especially it   remains some "sp" here and
 there). - Simplification of the interface of classify_object (first argument
 dropped). - Simplification of the code for vernac keyword "End". - Other
 small cleaning or dead code removal.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 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 b29bdf3f16..868a876be0 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -350,7 +350,7 @@ let subst_Function (_,subst,finfos) =
       is_general = finfos.is_general
     }
 
-let classify_Function (_,infos) = Libobject.Substitute infos
+let classify_Function infos = Libobject.Substitute infos
 
 let export_Function infos = Some infos
 
@@ -440,7 +440,7 @@ let _ =
 
 let find_or_none id = 
   try Some 
-    (match Nametab.locate (make_short_qualid id) with ConstRef c -> c | _ -> Util.anomaly "Not a constant" 
+    (match Nametab.locate (qualid_of_ident id) with ConstRef c -> c | _ -> Util.anomaly "Not a constant" 
     ) 
   with Not_found -> None
 
@@ -467,7 +467,7 @@ let add_Function is_general f =
   and rec_lemma = find_or_none (Nameops.add_suffix f_id "_rec")
   and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind")
   and graph_ind = 
-    match Nametab.locate (make_short_qualid (mk_rel_id f_id)) 
+    match Nametab.locate (qualid_of_ident (mk_rel_id f_id)) 
     with | IndRef ind -> ind | _ -> Util.anomaly "Not an inductive"
   in
   let finfos = 
-- 
cgit v1.2.3