Remove some uses of local modules (some were unused, some were costly).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16883 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 148 insertions, 177 deletions

diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index a7a181aa6..f98625b64 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -36,8 +36,7 @@ let get_module_path_of_full_path path =
 (*CSC: Problem: here we are using the wrong (???) hypothesis that there do *)
 (*CSC: not exist two modules whose dir_paths are one a prefix of the other *)
 let remove_module_dirpath_from_dirpath ~basedir dir =
- let module Ln = Libnames in
-  if Ln.is_dirpath_prefix_of basedir dir then
+  if Libnames.is_dirpath_prefix_of basedir dir then
    let ids = Names.DirPath.repr dir in
    let rec remove_firsts n l =
     match n,l with
@@ -57,14 +56,12 @@ let remove_module_dirpath_from_dirpath ~basedir dir =
 
 
 let get_uri_of_var v pvars =
- let module D = Decls in
- let module N = Names in
   let rec search_in_open_sections =
    function
       [] -> Errors.error ("Variable "^v^" not found")
     | he::tl as modules ->
-       let dirpath = N.DirPath.make modules in
-        if List.mem (N.Id.of_string v) (D.last_section_hyps dirpath) then
+       let dirpath = Names.DirPath.make modules in
+        if List.mem (Names.Id.of_string v) (Decls.last_section_hyps dirpath) then
          modules
         else
          search_in_open_sections tl
@@ -73,11 +70,11 @@ let get_uri_of_var v pvars =
     if List.mem v pvars then
       []
     else
-      search_in_open_sections (N.DirPath.repr (Lib.cwd ()))
+      search_in_open_sections (Names.DirPath.repr (Lib.cwd ()))
    in
     "cic:" ^
      List.fold_left
-      (fun i x -> "/" ^ N.Id.to_string x ^ i) "" path
+      (fun i x -> "/" ^ Names.Id.to_string x ^ i) "" path
 ;;
 
 type tag =
@@ -120,23 +117,20 @@ let subtract l1 l2 =
 ;;
 
 let token_list_of_path dir id tag =
- let module N = Names in
   let token_list_of_dirpath dirpath =
-   List.rev_map N.Id.to_string (N.DirPath.repr dirpath) in
-  token_list_of_dirpath dir @ [N.Id.to_string id ^ "." ^ (ext_of_tag tag)]
+   List.rev_map Names.Id.to_string (Names.DirPath.repr dirpath) in
+  token_list_of_dirpath dir @ [Names.Id.to_string id ^ "." ^ (ext_of_tag tag)]
 
 let token_list_of_kernel_name tag =
- let module N = Names in
- let module GN = Globnames in
  let id,dir = match tag with
    | Variable kn ->
-       N.Label.to_id (N.label kn), Lib.cwd ()
+       Names.Label.to_id (Names.label kn), Lib.cwd ()
    | Constant con ->
-       N.Label.to_id (N.con_label con),
-       Lib.remove_section_part (GN.ConstRef con)
+       Names.Label.to_id (Names.con_label con),
+       Lib.remove_section_part (Globnames.ConstRef con)
    | Inductive kn ->
-       N.Label.to_id (N.mind_label kn),
-       Lib.remove_section_part (GN.IndRef (kn,0))
+       Names.Label.to_id (Names.mind_label kn),
+       Lib.remove_section_part (Globnames.IndRef (kn,0))
  in
  token_list_of_path dir id (etag_of_tag tag)
 ;;
@@ -146,8 +140,7 @@ let uri_of_kernel_name tag =
    "cic:/" ^ String.concat "/" tokens
 
 let uri_of_declaration id tag =
- let module LN = Libnames in
- let dir = LN.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ()) in
+ let dir = Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ()) in
  let tokens = token_list_of_path dir id tag in
   "cic:/" ^ String.concat "/" tokens
 
@@ -322,16 +315,10 @@ let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids
  ids_to_father_ids ids_to_inner_sorts ids_to_inner_types
  ?(fake_dependent_products=false) env idrefs evar_map t expectedty
 =
- let module D = DoubleTypeInference in
- let module E = Environ in
- let module N = Names in
- let module A = Acic in
- let module T = Term in
- let module V = Vars in
   let fresh_id' = fresh_id seed ids_to_terms constr_to_ids ids_to_father_ids in
    (* CSC: do you have any reasonable substitute for 503? *)
    let terms_to_types = Acic.CicHash.create 503 in
-    D.double_type_of env evar_map t expectedty terms_to_types ;
+    DoubleTypeInference.double_type_of env evar_map t expectedty terms_to_types ;
     let rec aux computeinnertypes father passed_lambdas_or_prods_or_letins env
      idrefs ?(subst=None,[]) tt
     =
@@ -339,9 +326,9 @@ let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids
      let aux' = aux computeinnertypes (Some fresh_id'') [] in
       let string_of_sort_family =
        function
-          Coq_sort T.InProp -> "Prop"
-        | Coq_sort T.InSet  -> "Set"
-        | Coq_sort T.InType -> "Type"
+          Coq_sort Term.InProp -> "Prop"
+        | Coq_sort Term.InSet  -> "Set"
+        | Coq_sort Term.InType -> "Type"
         | CProp -> "CProp"
       in
       let string_of_sort t =
@@ -349,7 +336,8 @@ let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids
         (type_as_sort env evar_map t)
       in
        let ainnertypes,innertype,innersort,expected_available =
-        let {D.synthesized = synthesized; D.expected = expected} =
+        let {DoubleTypeInference.synthesized = synthesized;
+             DoubleTypeInference.expected = expected} =
          if computeinnertypes then
 try
           Acic.CicHash.find terms_to_types tt
@@ -361,11 +349,11 @@ Pp.msg_debug (Pp.(++) (Pp.str "BUG: this subterm was not visited during the doub
           (* type inference algorithm has not been applied.      *)
           (* We need to refresh the universes because we are doing *)
           (* type inference on an already inferred type.           *)
-          {D.synthesized =
+          {DoubleTypeInference.synthesized =
             Reductionops.nf_beta evar_map
              (CPropRetyping.get_type_of env evar_map
               (Termops.refresh_universes tt)) ;
-           D.expected = None}
+           DoubleTypeInference.expected = None}
         in
          let innersort =
           let synthesized_innersort =
@@ -470,19 +458,19 @@ print_endline "PASSATO" ; flush stdout ;
             if uninst_vars_length > 0 then
              (* Not enough arguments provided. We must eta-expand! *)
              let un_args,_ =
-              T.decompose_prod_n uninst_vars_length
+              Term.decompose_prod_n uninst_vars_length
                (CPropRetyping.get_type_of env evar_map tt)
              in
               let eta_expanded =
                let arguments =
-                List.map (V.lift uninst_vars_length) t @
+                List.map (Vars.lift uninst_vars_length) t @
                  Termops.rel_list 0 uninst_vars_length
                in
                 Unshare.unshare
-                 (T.lamn uninst_vars_length un_args
-                  (T.applistc h arguments))
+                 (Term.lamn uninst_vars_length un_args
+                  (Term.applistc h arguments))
               in
-               D.double_type_of env evar_map eta_expanded
+               DoubleTypeInference.double_type_of env evar_map eta_expanded
                 None terms_to_types ;
                Hashtbl.remove ids_to_inner_types fresh_id'' ;
                aux' env idrefs eta_expanded
@@ -492,48 +480,48 @@ print_endline "PASSATO" ; flush stdout ;
 
           (* Now that we have all the auxiliary functions we  *)
           (* can finally proceed with the main case analysis. *)
-          match T.kind_of_term tt with
-             T.Rel n ->
+          match Term.kind_of_term tt with
+             Term.Rel n ->
               let id =
-               match List.nth (E.rel_context env) (n - 1) with
-                  (N.Name id,_,_)   -> id
-                | (N.Anonymous,_,_) -> Nameops.make_ident "_" None
+               match List.nth (Environ.rel_context env) (n - 1) with
+                  (Names.Name id,_,_)   -> id
+                | (Names.Anonymous,_,_) -> Nameops.make_ident "_" None
               in
                Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
                if is_a_Prop innersort  && expected_available then
                 add_inner_type fresh_id'' ;
-               A.ARel (fresh_id'', n, List.nth idrefs (n-1), id)
-           | T.Var id ->
-	      let pvars = Termops.ids_of_named_context (E.named_context env) in
-	      let pvars = List.map N.Id.to_string pvars in
-              let path = get_uri_of_var (N.Id.to_string id) pvars in
+               Acic.ARel (fresh_id'', n, List.nth idrefs (n-1), id)
+           | Term.Var id ->
+	      let pvars = Termops.ids_of_named_context (Environ.named_context env) in
+	      let pvars = List.map Names.Id.to_string pvars in
+              let path = get_uri_of_var (Names.Id.to_string id) pvars in
                Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
                if is_a_Prop innersort  && expected_available then
                 add_inner_type fresh_id'' ;
-               A.AVar
-                (fresh_id'', path ^ "/" ^ (N.Id.to_string id) ^ ".var")
-           | T.Evar (n,l) ->
+               Acic.AVar
+                (fresh_id'', path ^ "/" ^ (Names.Id.to_string id) ^ ".var")
+           | Term.Evar (n,l) ->
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
               if is_a_Prop innersort  && expected_available then
                add_inner_type fresh_id'' ;
-              A.AEvar
+              Acic.AEvar
                (fresh_id'', n, Array.to_list (Array.map (aux' env idrefs) l))
-           | T.Meta _ -> Errors.anomaly (Pp.str "Meta met during exporting to XML")
-           | T.Sort s -> A.ASort (fresh_id'', s)
-           | T.Cast (v,_, t) ->
+           | Term.Meta _ -> Errors.anomaly (Pp.str "Meta met during exporting to XML")
+           | Term.Sort s -> Acic.ASort (fresh_id'', s)
+           | Term.Cast (v,_, t) ->
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
               if is_a_Prop innersort then
                add_inner_type fresh_id'' ;
-              A.ACast (fresh_id'', aux' env idrefs v, aux' env idrefs t)
-           | T.Prod (n,s,t) ->
+              Acic.ACast (fresh_id'', aux' env idrefs v, aux' env idrefs t)
+           | Term.Prod (n,s,t) ->
               let n' =
                match n with
-                  N.Anonymous -> N.Anonymous
+                  Names.Anonymous -> Names.Anonymous
                 | _ ->
-                  if not fake_dependent_products && V.noccurn 1 t then
-                   N.Anonymous
+                  if not fake_dependent_products && Vars.noccurn 1 t then
+                   Names.Anonymous
                   else
-                   N.Name
+                   Names.Name
                     (Namegen.next_name_away n (Termops.ids_of_context env))
               in
                Hashtbl.add ids_to_inner_sorts fresh_id''
@@ -549,7 +537,7 @@ print_endline "PASSATO" ; flush stdout ;
                      match
                       Term.kind_of_term (Hashtbl.find ids_to_terms father')
                      with
-                        T.Prod _ -> true
+                        Term.Prod _ -> true
                       | _ -> false
                 in
                  (fresh_id'', n', aux' env idrefs s)::
@@ -557,20 +545,20 @@ print_endline "PASSATO" ; flush stdout ;
                     passed_lambdas_or_prods_or_letins
                    else [])
                in
-                let new_env = E.push_rel (n', None, s) env in
+                let new_env = Environ.push_rel (n', None, s) env in
                 let new_idrefs = fresh_id''::idrefs in
                  (match Term.kind_of_term t with
-                     T.Prod _ ->
+                     Term.Prod _ ->
                       aux computeinnertypes (Some fresh_id'') new_passed_prods
                        new_env new_idrefs t
                    | _ ->
-                     A.AProds (new_passed_prods, aux' new_env new_idrefs t))
-           | T.Lambda (n,s,t) ->
+                     Acic.AProds (new_passed_prods, aux' new_env new_idrefs t))
+           | Term.Lambda (n,s,t) ->
               let n' =
                match n with
-                  N.Anonymous -> N.Anonymous
+                  Names.Anonymous -> Names.Anonymous
                 | _ ->
-                  N.Name (Namegen.next_name_away n (Termops.ids_of_context env))
+                  Names.Name (Namegen.next_name_away n (Termops.ids_of_context env))
               in
                Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
                let sourcetype = CPropRetyping.get_type_of env evar_map s in
@@ -583,7 +571,7 @@ print_endline "PASSATO" ; flush stdout ;
                     match
                      Term.kind_of_term (Hashtbl.find ids_to_terms father')
                     with
-                       T.Lambda _ -> true
+                       Term.Lambda _ -> true
                      | _ -> false
                in
                 if is_a_Prop innersort &&
@@ -594,10 +582,10 @@ print_endline "PASSATO" ; flush stdout ;
                   (if father_is_lambda then
                     passed_lambdas_or_prods_or_letins
                    else []) in
-                let new_env = E.push_rel (n', None, s) env in
+                let new_env = Environ.push_rel (n', None, s) env in
                 let new_idrefs = fresh_id''::idrefs in
                  (match Term.kind_of_term t with
-                     T.Lambda _ ->
+                     Term.Lambda _ ->
                       aux computeinnertypes (Some fresh_id'') new_passed_lambdas
                        new_env new_idrefs t
                    | _ ->
@@ -606,19 +594,19 @@ print_endline "PASSATO" ; flush stdout ;
                       (* can create nested Lambdas. Here we perform the *)
                       (* flattening.                                    *)
                       match t' with
-                         A.ALambdas (lambdas, t'') ->
-                          A.ALambdas (lambdas@new_passed_lambdas, t'')
+                         Acic.ALambdas (lambdas, t'') ->
+                          Acic.ALambdas (lambdas@new_passed_lambdas, t'')
                        | _ ->
-                         A.ALambdas (new_passed_lambdas, t')
+                         Acic.ALambdas (new_passed_lambdas, t')
                  )
-           | T.LetIn (n,s,t,d) ->
+           | Term.LetIn (n,s,t,d) ->
               let id =
                match n with
-                   N.Anonymous -> N.Id.of_string "_X"
-                 | N.Name id -> id
+                   Names.Anonymous -> Names.Id.of_string "_X"
+                 | Names.Name id -> id
               in
               let n' =
-               N.Name (Namegen.next_ident_away id (Termops.ids_of_context env))
+               Names.Name (Namegen.next_ident_away id (Termops.ids_of_context env))
               in
                Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
                let sourcesort =
@@ -634,7 +622,7 @@ print_endline "PASSATO" ; flush stdout ;
                     match
                      Term.kind_of_term (Hashtbl.find ids_to_terms father')
                     with
-                       T.LetIn _ -> true
+                       Term.LetIn _ -> true
                      | _ -> false
                in
                 if is_a_Prop innersort then
@@ -644,15 +632,15 @@ print_endline "PASSATO" ; flush stdout ;
                   (if father_is_letin then
                     passed_lambdas_or_prods_or_letins
                    else []) in
-                let new_env = E.push_rel (n', Some s, t) env in
+                let new_env = Environ.push_rel (n', Some s, t) env in
                 let new_idrefs = fresh_id''::idrefs in
                  (match Term.kind_of_term d with
-                     T.LetIn _ ->
+                     Term.LetIn _ ->
                       aux computeinnertypes (Some fresh_id'') new_passed_letins
                        new_env new_idrefs d
-                   | _ -> A.ALetIns
+                   | _ -> Acic.ALetIns
                            (new_passed_letins, aux' new_env new_idrefs d))
-           | T.App (h,t) ->
+           | Term.App (h,t) ->
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
               if is_a_Prop innersort then
                add_inner_type fresh_id'' ;
@@ -669,7 +657,7 @@ print_endline "PASSATO" ; flush stdout ;
                 (* maybe all the arguments were used for the explicit *)
                 (* named substitution                                 *)
                 if residual_args_not_empty then
-                 A.AApp (fresh_id'', h'::residual_args)
+                 Acic.AApp (fresh_id'', h'::residual_args)
                 else
                  h'
               in
@@ -679,48 +667,48 @@ print_endline "PASSATO" ; flush stdout ;
                 explicit_substitute_and_eta_expand_if_required h
                  (Array.to_list t) t'
                  compute_result_if_eta_expansion_not_required
-           | T.Const kn ->
+           | Term.Const kn ->
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
               if is_a_Prop innersort  && expected_available then
                add_inner_type fresh_id'' ;
               let compute_result_if_eta_expansion_not_required _ _ =
-               A.AConst (fresh_id'', subst, (uri_of_kernel_name (Constant kn)))
+               Acic.AConst (fresh_id'', subst, (uri_of_kernel_name (Constant kn)))
               in
                let (_,subst') = subst in
                 explicit_substitute_and_eta_expand_if_required tt []
                  (List.map snd subst')
                  compute_result_if_eta_expansion_not_required
-           | T.Ind (kn,i) ->
+           | Term.Ind (kn,i) ->
               let compute_result_if_eta_expansion_not_required _ _ =
-               A.AInd (fresh_id'', subst, (uri_of_kernel_name (Inductive kn)), i)
+               Acic.AInd (fresh_id'', subst, (uri_of_kernel_name (Inductive kn)), i)
               in
                let (_,subst') = subst in
                 explicit_substitute_and_eta_expand_if_required tt []
                  (List.map snd subst')
                  compute_result_if_eta_expansion_not_required
-           | T.Construct ((kn,i),j) ->
+           | Term.Construct ((kn,i),j) ->
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
               if is_a_Prop innersort  && expected_available then
                add_inner_type fresh_id'' ;
               let compute_result_if_eta_expansion_not_required _ _ =
-               A.AConstruct
+               Acic.AConstruct
                 (fresh_id'', subst, (uri_of_kernel_name (Inductive kn)), i, j)
               in
                let (_,subst') = subst in
                 explicit_substitute_and_eta_expand_if_required tt []
                  (List.map snd subst')
                  compute_result_if_eta_expansion_not_required
-           | T.Case ({T.ci_ind=(kn,i)},ty,term,a) ->
+           | Term.Case ({Term.ci_ind=(kn,i)},ty,term,a) ->
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
               if is_a_Prop innersort then
                add_inner_type fresh_id'' ;
               let a' =
                Array.fold_right (fun x i -> (aux' env idrefs x)::i) a []
               in
-               A.ACase
+               Acic.ACase
                 (fresh_id'', (uri_of_kernel_name (Inductive kn)), i,
                   aux' env idrefs ty, aux' env idrefs term, a')
-           | T.Fix ((ai,i),(f,t,b)) ->
+           | Term.Fix ((ai,i),(f,t,b)) ->
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
               if is_a_Prop innersort then add_inner_type fresh_id'' ;
               let fresh_idrefs =
@@ -732,29 +720,29 @@ print_endline "PASSATO" ; flush stdout ;
                 let ids = ref (Termops.ids_of_context env) in
                  Array.map
                   (function
-                      N.Anonymous -> Errors.error "Anonymous fix function met"
-                    | N.Name id as n ->
-                       let res = N.Name (Namegen.next_name_away n !ids) in
+                      Names.Anonymous -> Errors.error "Anonymous fix function met"
+                    | Names.Name id as n ->
+                       let res = Names.Name (Namegen.next_name_away n !ids) in
                         ids := id::!ids ;
                         res
                  ) f
                in
-                A.AFix (fresh_id'', i,
+                Acic.AFix (fresh_id'', i,
                  Array.fold_right
                   (fun (id,fi,ti,bi,ai) i ->
                     let fi' =
                      match fi with
-                        N.Name fi -> fi
-                      | N.Anonymous -> Errors.error "Anonymous fix function met"
+                        Names.Name fi -> fi
+                      | Names.Anonymous -> Errors.error "Anonymous fix function met"
                     in
                      (id, fi', ai,
                       aux' env idrefs ti,
-                      aux' (E.push_rec_types (f',t,b) env) new_idrefs bi)::i)
+                      aux' (Environ.push_rec_types (f',t,b) env) new_idrefs bi)::i)
                   (Array.mapi
                    (fun j x -> (fresh_idrefs.(j),x,t.(j),b.(j),ai.(j))) f'
                   ) []
                  )
-           | T.CoFix (i,(f,t,b)) ->
+           | Term.CoFix (i,(f,t,b)) ->
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
               if is_a_Prop innersort then add_inner_type fresh_id'' ;
               let fresh_idrefs =
@@ -766,24 +754,24 @@ print_endline "PASSATO" ; flush stdout ;
                 let ids = ref (Termops.ids_of_context env) in
                  Array.map
                   (function
-                      N.Anonymous -> Errors.error "Anonymous fix function met"
-                    | N.Name id as n ->
-                       let res = N.Name (Namegen.next_name_away n !ids) in
+                      Names.Anonymous -> Errors.error "Anonymous fix function met"
+                    | Names.Name id as n ->
+                       let res = Names.Name (Namegen.next_name_away n !ids) in
                         ids := id::!ids ;
                         res
                  ) f
                in
-                A.ACoFix (fresh_id'', i,
+                Acic.ACoFix (fresh_id'', i,
                  Array.fold_right
                   (fun (id,fi,ti,bi) i ->
                     let fi' =
                      match fi with
-                        N.Name fi -> fi
-                      | N.Anonymous -> Errors.error "Anonymous fix function met"
+                        Names.Name fi -> fi
+                      | Names.Anonymous -> Errors.error "Anonymous fix function met"
                     in
                      (id, fi',
                       aux' env idrefs ti,
-                      aux' (E.push_rec_types (f',t,b) env) new_idrefs bi)::i)
+                      aux' (Environ.push_rec_types (f',t,b) env) new_idrefs bi)::i)
                   (Array.mapi
                     (fun j x -> (fresh_idrefs.(j),x,t.(j),b.(j)) ) f'
                   ) []
@@ -807,7 +795,6 @@ let acic_of_cic_context metasenv context t =
 *)
 
 let acic_object_of_cic_object sigma obj =
- let module A = Acic in
   let ids_to_terms = Hashtbl.create 503 in
   let constr_to_ids = Acic.CicHash.create 503 in
   let ids_to_father_ids = Hashtbl.create 503 in
@@ -837,23 +824,23 @@ let acic_object_of_cic_object sigma obj =
   in
    let aobj =
     match obj with
-      A.Constant (id,bo,ty,params) ->
+      Acic.Constant (id,bo,ty,params) ->
        let abo =
         match bo with
            None -> None
          | Some bo' -> Some (acic_term_of_cic_term' bo' (Some ty))
        in
        let aty = acic_term_of_cic_term' ty None in
-        A.AConstant (fresh_id (),id,abo,aty,params)
-    | A.Variable (id,bo,ty,params) ->
+        Acic.AConstant (fresh_id (),id,abo,aty,params)
+    | Acic.Variable (id,bo,ty,params) ->
        let abo =
         match bo with
            Some bo -> Some (acic_term_of_cic_term' bo (Some ty))
          | None -> None
        in
        let aty = acic_term_of_cic_term' ty None in
-        A.AVariable (fresh_id (),id,abo,aty,params)
-    | A.CurrentProof (id,conjectures,bo,ty) ->
+        Acic.AVariable (fresh_id (),id,abo,aty,params)
+    | Acic.CurrentProof (id,conjectures,bo,ty) ->
        let aconjectures =
         List.map
          (function (i,canonical_context,term) as conjecture ->
@@ -870,7 +857,7 @@ let acic_object_of_cic_object sigma obj =
                    Hashtbl.add ids_to_hypotheses hid hyp ;
                    incr hypotheses_seed ;
                    match decl_or_def with
-                       A.Decl t ->
+                       Acic.Decl t ->
                         let final_env,final_idrefs,atl =
                          aux (Environ.push_rel (Names.Name n,None,t) env)
                           new_idrefs tl
@@ -878,8 +865,8 @@ let acic_object_of_cic_object sigma obj =
                          let at =
                           acic_term_of_cic_term_context' env idrefs sigma t None
                          in
-                          final_env,final_idrefs,(hid,(n,A.Decl at))::atl
-                     | A.Def (t,ty) ->
+                          final_env,final_idrefs,(hid,(n,Acic.Decl at))::atl
+                     | Acic.Def (t,ty) ->
                         let final_env,final_idrefs,atl =
                          aux
                           (Environ.push_rel (Names.Name n,Some t,ty) env)
@@ -890,10 +877,10 @@ let acic_object_of_cic_object sigma obj =
                          in
                          let dummy_never_used =
                           let s = "dummy_never_used" in
-                           A.ARel (s,99,s,Names.Id.of_string s)
+                           Acic.ARel (s,99,s,Names.Id.of_string s)
                          in
                           final_env,final_idrefs,
-                           (hid,(n,A.Def (at,dummy_never_used)))::atl
+                           (hid,(n,Acic.Def (at,dummy_never_used)))::atl
              in
               aux env [] canonical_context
             in
@@ -905,8 +892,8 @@ let acic_object_of_cic_object sigma obj =
          ) conjectures in
        let abo = acic_term_of_cic_term_context' env [] sigma bo (Some ty) in
        let aty = acic_term_of_cic_term_context' env [] sigma ty None in
-        A.ACurrentProof (fresh_id (),id,aconjectures,abo,aty)
-    | A.InductiveDefinition (tys,params,paramsno) ->
+        Acic.ACurrentProof (fresh_id (),id,aconjectures,abo,aty)
+    | Acic.InductiveDefinition (tys,params,paramsno) ->
        let env' =
         List.fold_right
          (fun (name,_,arity,_) env ->
@@ -930,7 +917,7 @@ let acic_object_of_cic_object sigma obj =
              (id,name,inductive,aty,acons)
          ) (List.rev idrefs) tys
        in
-       A.AInductiveDefinition (fresh_id (),atys,params,paramsno)
+       Acic.AInductiveDefinition (fresh_id (),atys,params,paramsno)
    in
     aobj,ids_to_terms,constr_to_ids,ids_to_father_ids,ids_to_inner_sorts,
      ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index 5a3880b01..d54308165 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -16,20 +16,17 @@
 type types = {synthesized : Term.types ; expected : Term.types option};;
 
 let cprop =
- let module N = Names in
-  N.make_con
-   (N.MPfile
+  Names.make_con
+   (Names.MPfile
      (Libnames.dirpath_of_string "CoRN.algebra.CLogic"))
-   (N.DirPath.empty)
-   (N.Label.make "CProp")
+   (Names.DirPath.empty)
+   (Names.Label.make "CProp")
 ;;
 
 let whd_betadeltaiotacprop env _evar_map ty =
- let module C = Closure in
- let module CR = C.RedFlags in
  (*** CProp is made Opaque ***)
- let flags = CR.red_sub C.betadeltaiota (CR.fCONST cprop) in
- C.whd_val (C.create_clos_infos flags env) (C.inject ty)
+ let flags = Closure.RedFlags.red_sub Closure.betadeltaiota (Closure.RedFlags.fCONST cprop) in
+ Closure.whd_val (Closure.create_clos_infos flags env) (Closure.inject ty)
 ;;
 
 
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index d065ba61a..abd6b3b73 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -53,7 +53,6 @@ let filter_params pvars hyps =
 (* better unless this function is reimplemented in the Declare   *)
 (* module.                                                       *)
 let search_variables () =
- let module N = Names in
   let cwd = Lib.cwd () in
   let cwdsp = Libnames.make_path cwd (Names.Id.of_string "dummy") in
   let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in
@@ -62,8 +61,8 @@ let search_variables () =
        [] -> []
      | he::tl as modules ->
         let one_section_variables =
-         let dirpath = N.DirPath.make (modules @ N.DirPath.repr modulepath) in
-          let t = List.map N.Id.to_string (Decls.last_section_hyps dirpath) in
+         let dirpath = Names.DirPath.make (modules @ Names.DirPath.repr modulepath) in
+          let t = List.map Names.Id.to_string (Decls.last_section_hyps dirpath) in
            [he,t]
         in
          one_section_variables @ aux tl
@@ -88,7 +87,6 @@ let rec join_dirs cwd =
 ;;
 
 let filename_of_path xml_library_root tag =
- let module N = Names in
   match xml_library_root with
      None -> None  (* stdout *)
    | Some xml_library_root' ->
@@ -109,11 +107,10 @@ let types_filename_of_filename =
 ;;
 
 let theory_filename xml_library_root =
- let module N = Names in
   match xml_library_root with
     None -> None  (* stdout *)
   | Some xml_library_root' ->
-     let toks = List.map N.Id.to_string (N.DirPath.repr (Lib.library_dp ())) in
+     let toks = List.map Names.Id.to_string (Names.DirPath.repr (Lib.library_dp ())) in
      (* theory from A/B/C/F.v goes into A/B/C/F.theory *)
      let alltoks = List.rev toks in
        Some (join_dirs xml_library_root' alltoks ^ ".theory")
@@ -160,10 +157,9 @@ let string_list_of_named_context_list =
 (* Used only for variables (since for constants and mutual *)
 (* inductive types this information is already available.  *)
 let find_hyps t =
- let module T = Term in
   let rec aux l t =
-   match T.kind_of_term t with
-      T.Var id when not (List.mem id l) ->
+   match Term.kind_of_term t with
+      Term.Var id when not (List.mem id l) ->
        let (_,bo,ty) = Global.lookup_named id in
         let boids =
          match bo with
@@ -171,27 +167,27 @@ let find_hyps t =
           | None -> l
         in
          id::(aux boids ty)
-    | T.Var _
-    | T.Rel _
-    | T.Meta _
-    | T.Evar _
-    | T.Sort _ -> l
-    | T.Cast (te,_, ty) -> aux (aux l te) ty
-    | T.Prod (_,s,t) -> aux (aux l s) t
-    | T.Lambda (_,s,t) -> aux (aux l s) t
-    | T.LetIn (_,s,_,t) -> aux (aux l s) t
-    | T.App (he,tl) -> Array.fold_left (fun i x -> aux i x) (aux l he) tl
-    | T.Const con ->
+    | Term.Var _
+    | Term.Rel _
+    | Term.Meta _
+    | Term.Evar _
+    | Term.Sort _ -> l
+    | Term.Cast (te,_, ty) -> aux (aux l te) ty
+    | Term.Prod (_,s,t) -> aux (aux l s) t
+    | Term.Lambda (_,s,t) -> aux (aux l s) t
+    | Term.LetIn (_,s,_,t) -> aux (aux l s) t
+    | Term.App (he,tl) -> Array.fold_left (fun i x -> aux i x) (aux l he) tl
+    | Term.Const con ->
        let hyps = (Global.lookup_constant con).Declarations.const_hyps in
         map_and_filter l hyps @ l
-    | T.Ind ind
-    | T.Construct (ind,_) ->
+    | Term.Ind ind
+    | Term.Construct (ind,_) ->
        let hyps = (fst (Global.lookup_inductive ind)).Declarations.mind_hyps in
         map_and_filter l hyps @ l
-    | T.Case (_,t1,t2,b) ->
+    | Term.Case (_,t1,t2,b) ->
        Array.fold_left (fun i x -> aux i x) (aux (aux l t1) t2) b
-    | T.Fix (_,(_,tys,bodies))
-    | T.CoFix (_,(_,tys,bodies)) ->
+    | Term.Fix (_,(_,tys,bodies))
+    | Term.CoFix (_,(_,tys,bodies)) ->
        let r = Array.fold_left (fun i x -> aux i x) l tys in
         Array.fold_left (fun i x -> aux i x) r bodies
   and map_and_filter l =
@@ -339,15 +335,14 @@ let kind_of_constant kn =
 ;;
 
 let kind_of_global r =
-  let module Gn = Globnames in
   match r with
-  | Gn.IndRef kn | Gn.ConstructRef (kn,_) ->
+  | Globnames.IndRef kn | Globnames.ConstructRef (kn,_) ->
       let isrecord =
 	try let _ = Recordops.lookup_projections kn in Declare.KernelSilent
         with Not_found -> Declare.KernelVerbose in
       kind_of_inductive isrecord (fst kn)
-  | Gn.VarRef id -> kind_of_variable id
-  | Gn.ConstRef kn -> kind_of_constant kn
+  | Globnames.VarRef id -> kind_of_variable id
+  | Globnames.ConstRef kn -> kind_of_constant kn
 ;;
 
 let print_object_kind uri (xmltag,variation) =
@@ -366,39 +361,31 @@ let print_object_kind uri (xmltag,variation) =
 (*       form of the definition (all the parameters are                   *)
 (*       lambda-abstracted, but the object can still refer to variables)  *)
 let print internal glob_ref kind xml_library_root =
- let module D = Declareops in
- let module De = Declare in
- let module G = Global in
- let module N = Names in
- let module Nt = Nametab in
- let module T = Term in
- let module X = Xml in
- let module Gn = Globnames in
   (* Variables are the identifiers of the variables in scope *)
   let variables = search_variables () in
   let tag,obj =
    match glob_ref with
-      Gn.VarRef id ->
+      Globnames.VarRef id ->
        (* this kn is fake since it is not provided by Coq *)
        let kn = Lib.make_kn id in
-       let (_,body,typ) = G.lookup_named id in
+       let (_,body,typ) = Global.lookup_named id in
         Cic2acic.Variable kn,mk_variable_obj id body typ
-    | Gn.ConstRef kn ->
-       let id = N.Label.to_id (N.con_label kn) in
-       let cb = G.lookup_constant kn in
-       let val0 = D.body_of_constant cb in
+    | Globnames.ConstRef kn ->
+       let id = Names.Label.to_id (Names.con_label kn) in
+       let cb = Global.lookup_constant kn in
+       let val0 = Declareops.body_of_constant cb in
        let typ = cb.Declarations.const_type in
        let hyps = cb.Declarations.const_hyps in
        let typ = Typeops.type_of_constant_type (Global.env()) typ in
         Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps
-    | Gn.IndRef (kn,_) ->
-       let mib = G.lookup_mind kn in
+    | Globnames.IndRef (kn,_) ->
+       let mib = Global.lookup_mind kn in
        let {Declarations.mind_nparams=nparams;
 	    Declarations.mind_packets=packs ;
             Declarations.mind_hyps=hyps;
             Declarations.mind_finite=finite} = mib in
           Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps finite
-    | Gn.ConstructRef _ ->
+    | Globnames.ConstructRef _ ->
        Errors.error ("a single constructor cannot be printed in XML")
   in
   let fn = filename_of_path xml_library_root tag in