- 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

1 files changed, 3 insertions, 3 deletions

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 =