- 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/toplevel/command.ml b/toplevel/command.ml
index 48a5119d15..82fd9bc1aa 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -612,7 +612,7 @@ let eq_local_binders bl1 bl2 =
   List.length bl1 = List.length bl2 && List.for_all2 eq_local_binder bl1 bl2
 
 let extract_coercions indl =
-  let mkqid (_,((_,id),_)) = make_short_qualid id in
+  let mkqid (_,((_,id),_)) = qualid_of_ident id in
   let extract lc = List.filter (fun (iscoe,_) -> iscoe) lc in
   List.map mkqid (List.flatten(List.map (fun (_,_,_,lc) -> extract lc) indl))
 
@@ -930,7 +930,7 @@ requested
        let l1,l2 = split_scheme q in
     ( match t with
       | InductionScheme (x,y,z) ->
-             let ind = mkInd (Nametab.inductive_of_reference y) in
+             let ind = mkInd (Nametab.global_inductive y) in
              let sort_of_ind = family_of_sort (Typing.sort_of env Evd.empty ind)
 in
              let z' = family_of_sort (interp_sort z) in
@@ -969,7 +969,7 @@ let build_induction_scheme lnamedepindsort =
   let lrecspec =
     List.map
       (fun (_,dep,indid,sort) ->
-        let ind = Nametab.inductive_of_reference indid in
+        let ind = Nametab.global_inductive indid in
         let (mib,mip) = Global.lookup_inductive ind in
          (ind,mib,mip,dep,interp_elimination_sort sort)) 
       lnamedepindsort
@@ -998,7 +998,7 @@ tried to declare different schemes at once *)
     else (
       if ischeme <> [] then build_induction_scheme ischeme;
       List.iter ( fun indname -> 
-        let ind = Nametab.inductive_of_reference indname
+        let ind = Nametab.global_inductive indname
         in declare_eq_scheme (fst ind);
         try
            make_eq_decidability ind