- 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

8 files changed, 11 insertions, 11 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 7417535217..b998daa742 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -446,7 +446,7 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) =
 	  if hintlist' == hintlist then obj else
 	    (local,name,AddTactic hintlist')
 	      
-let classify_autohint (_,((local,name,hintlist) as obj)) =
+let classify_autohint ((local,name,hintlist) as obj) =
   if local or hintlist = (AddTactic []) then Dispose else Substitute obj
 
 let export_autohint ((local,name,hintlist) as obj) =
@@ -548,7 +548,7 @@ let interp_hints h =
       HintsTransparencyEntry (List.map fr lhints, b)
   | HintsConstructors lqid ->
       let constr_hints_of_ind qid =
-        let isp = inductive_of_reference qid in
+        let isp = global_inductive qid in
         let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in
         list_tabulate (fun i -> None, true, mkConstruct (isp,i+1))
 	  (Array.length consnames) in
@@ -1121,7 +1121,7 @@ let superauto n to_add argl  =
 
 let interp_to_add gl r =
   let r = Syntax_def.locate_global_with_alias (qualid_of_reference r) in
-  let id = id_of_global r in
+  let id = basename_of_global r in
   (next_ident_away id (pf_ids_of_hyps gl), constr_of_global r)
 
 let gen_superauto nopt l a b gl =
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 04c4ed1611..63481abde4 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -224,7 +224,7 @@ let subst_hintrewrite (_,subst,(rbase,list as node)) =
     if list' == list then node else
       (rbase,list')
       
-let classify_hintrewrite (_,x) = Libobject.Substitute x
+let classify_hintrewrite x = Libobject.Substitute x
 
 
 (* Declaration of the Hint Rewrite library object *)
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 3d34a2d688..be4343b4f0 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -206,7 +206,7 @@ let cache_dd (_,(_,na,dd)) =
       (str"The code which adds destructor hints broke;" ++ spc () ++ 
 	 str"this is not supposed to happen")
 
-let classify_dd (_,(local,_,_ as o)) =
+let classify_dd (local,_,_ as o) =
   if local then Dispose else Substitute o
 
 let export_dd (local,_,_ as x) = if local then None else Some x
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index f1c2551548..c6c9bdd105 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -408,7 +408,7 @@ let (inTransitivity,_) =
     cache_function = cache_transitivity_lemma;
     open_function = (fun i o -> if i=1 then cache_transitivity_lemma o);
     subst_function = subst_transitivity_lemma;
-    classify_function = (fun (_,o) -> Substitute o);       
+    classify_function = (fun o -> Substitute o);       
     export_function = (fun x -> Some x) }
 
 (* Synchronisation with reset *)
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 43ae99203d..385e865878 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -67,7 +67,7 @@ let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
 
 let try_find_global_reference dir s =
   let sp = Libnames.make_path (make_dir ("Coq"::dir)) (id_of_string s) in
-    Nametab.absolute_reference sp
+    Nametab.global_of_path sp
       
 let try_find_reference dir s =
   constr_of_global (try_find_global_reference dir s)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 32c69ddcdc..e79174c66b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -374,7 +374,7 @@ let loc_of_by_notation f = function
 let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
 
 let intern_inductive_or_by_notation = function
-  | AN r -> Nametab.inductive_of_reference r
+  | AN r -> Nametab.global_inductive r
   | ByNotation (loc,ntn,sc) ->
       destIndRef (Notation.interp_notation_as_global_reference loc
         (function IndRef ind -> true | _ -> false) ntn sc)
@@ -2847,7 +2847,7 @@ let (inMD,outMD) =
      load_function   = load_md;
      open_function   = open_md;
      subst_function = subst_md;
-     classify_function = (fun (_,o) -> Substitute o);       
+     classify_function = (fun o -> Substitute o);       
      export_function = (fun x -> Some x)}
 
 let print_ltac id =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ca64a8d3d2..663c426f97 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2054,7 +2054,7 @@ let make_up_names n ind_opt cname =
     if is_hyp then 
       match ind_opt with
 	| None -> id_of_string ind_prefix
-	| Some ind_id -> add_prefix ind_prefix (Nametab.id_of_global ind_id)
+	| Some ind_id -> add_prefix ind_prefix (Nametab.basename_of_global ind_id)
     else add_prefix ind_prefix cname in
   let hyprecname = make_base n base_ind in
   let avoid =
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index bbc1285e2b..ad2fd90093 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -277,7 +277,7 @@ let tauto_classical nnpp g =
 
 let tauto g =
   try 
-    let nnpp = constr_of_global (Nametab.absolute_reference coq_nnpp_path) in
+    let nnpp = constr_of_global (Nametab.global_of_path coq_nnpp_path) in
     (* try intuitionistic version first to avoid an axiom if possible *)
     tclORELSE tauto_intuitionistic (tauto_classical nnpp) g
   with Not_found ->