- 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, 4 insertions, 4 deletions

diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index bdec6bf45..1caa5db1c 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -20,15 +20,15 @@ let destructurate t =
   match Term.kind_of_term c, args with
     | Term.Const sp, args ->
 	Kapp (Names.string_of_id
-		(Nametab.id_of_global (Libnames.ConstRef sp)),
+		(Nametab.basename_of_global (Libnames.ConstRef sp)),
 	      args)
     | Term.Construct csp , args ->
 	Kapp (Names.string_of_id
-		(Nametab.id_of_global (Libnames.ConstructRef csp)),
+		(Nametab.basename_of_global (Libnames.ConstructRef csp)),
 	      args)
     | Term.Ind isp, args ->
 	Kapp (Names.string_of_id
-		(Nametab.id_of_global (Libnames.IndRef isp)),
+		(Nametab.basename_of_global (Libnames.IndRef isp)),
 	      args)
     | Term.Var id,[] -> Kvar(Names.string_of_id id)
     | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
@@ -46,7 +46,7 @@ let dest_const_apply t =
     | Term.Construct csp -> Libnames.ConstructRef csp
     | Term.Ind isp       -> Libnames.IndRef isp
     | _ -> raise Destruct
-  in  Nametab.id_of_global ref, args
+  in  Nametab.basename_of_global ref, args
 
 let logic_dir = ["Coq";"Logic";"Decidable"]