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

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 2f2796f1c6..52e2eb24e5 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -168,7 +168,7 @@ let (class_input,class_output) =
       cache_function = cache_class;
       load_function = (fun _ -> load_class);
       open_function = (fun _ -> load_class);
-      classify_function = (fun (_,x) -> Substitute x);
+      classify_function = (fun x -> Substitute x);
       discharge_function = (fun a -> Some (discharge_class a));
       rebuild_function = rebuild_class;
       subst_function = subst_class;
@@ -212,7 +212,7 @@ let (instance_input,instance_output) =
       cache_function = cache_instance;
       load_function = (fun _ -> load_instance);
       open_function = (fun _ -> load_instance);
-      classify_function = (fun (_,x) -> Substitute x);
+      classify_function = (fun x -> Substitute x);
       discharge_function = (fun a -> Some (discharge_instance a));
       rebuild_function = rebuild_instance;
       subst_function = subst_instance;