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

diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index bbc1285e2..ad2fd9009 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 ->