Splitting Term into five unrelated interfaces:

1. sorts.ml: A small file utility for sorts;

2. constr.ml: Really low-level terms, essentially kind_of_constr, smart
constructor and basic operators;

3. vars.ml: Everything related to term variables, that is, occurences
and substitution;

4. context.ml: Rel/Named context and all that;

5. term.ml: derived utility operations on terms; also includes constr.ml
up to some renaming, and acts as a compatibility layer, to be deprecated.

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

1 files changed, 4 insertions, 3 deletions

diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index c95cf94b67..5a3880b015 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -59,6 +59,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
  (*CSC: functions used do checks that we do not need                       *)
  let rec execute env sigma cstr expectedty =
   let module T = Term in
+  let module V = Vars in
   let module E = Environ in
    (* the type part is the synthesized type *)
    let judgement =
@@ -84,7 +85,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
                 (function (m,bo,ty) ->
                   (* Warning: the substitution should be performed also on bo *)
                   (* This is not done since bo is not used later yet          *)
-                  (m,bo,Unshare.unshare (T.replace_vars [n,he1] ty))
+                  (m,bo,Unshare.unshare (V.replace_vars [n,he1] ty))
                 ) tl2
               in
                iter tl1 tl2'
@@ -161,7 +162,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
               match T.kind_of_term (Reduction.whd_betadeltaiota env typ) with
                  T.Prod (_,c1,c2) ->
                   (Some (Reductionops.nf_beta sigma c1)) ::
-                   (aux (T.subst1 hj c2) restjl)
+                   (aux (V.subst1 hj c2) restjl)
                | _ -> assert false
          in
           Array.of_list (aux j.Environ.uj_type (Array.to_list args))
@@ -249,7 +250,7 @@ if Acic.CicHash.mem subterms_to_types cstr then
    let lara = Array.map (assumption_of_judgment env sigma) larj in
    let env1 = Environ.push_rec_types (names,lara,vdef) env in
    let expectedtypes =
-    Array.map (function i -> Some (Term.lift length i)) lar
+    Array.map (function i -> Some (Vars.lift length i)) lar
    in
    let vdefj = execute_array env1 sigma vdef expectedtypes in
    let vdefv = Array.map Environ.j_val vdefj in