- 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/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 25e664336..876f3de4b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1386,7 +1386,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let tcc_lemma_constr = ref None in 
 (*   let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
   let hook _ _ =   
-    let term_ref = Nametab.locate (make_short_qualid term_id) in
+    let term_ref = Nametab.locate (qualid_of_ident term_id) in
     let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
 (*     message "start second proof"; *)
     let stop = ref false in 
@@ -1404,7 +1404,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
     end;
     if not !stop
     then
-      let eq_ref = Nametab.locate (make_short_qualid equation_id ) in
+      let eq_ref = Nametab.locate (qualid_of_ident equation_id ) in
       let f_ref = destConst (constr_of_global f_ref) 
       and functional_ref = destConst (constr_of_global functional_ref) 
       and eq_ref = destConst (constr_of_global eq_ref) in