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

22 files changed, 44 insertions, 19 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 473199cb2..aba908d48 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -15,6 +15,7 @@ open Pp
 open Goptions
 open Names
 open Term
+open Vars
 open Tacmach
 open Evd
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index a5baa00f9..a7800667f 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -13,6 +13,7 @@ open Names
 open Inductiveops
 open Declarations
 open Term
+open Vars
 open Tacmach
 open Tactics
 open Tacticals
@@ -226,7 +227,7 @@ let build_projection intype outtype (cstr:constructor) special default gls=
   let lp=Array.length types in
   let ci=pred (snd cstr) in
   let branch i=
-    let ti=Term.prod_appvect types.(i) argv in
+    let ti= prod_appvect types.(i) argv in
     let rc=fst (decompose_prod_assum ti) in
     let head=
       if i=ci then special else default in
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 9d34dc99a..b9334801c 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -17,6 +17,7 @@ open Decl_mode
 open Pretyping
 open Glob_term
 open Term
+open Vars
 open Pp
 open Decl_kinds
 open Misctypes
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 2ef2c9756..5e55bcfb2 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -25,6 +25,7 @@ open Declarations
 open Tactics
 open Tacticals
 open Term
+open Vars
 open Termops
 open Namegen
 open Reductionops
@@ -301,7 +302,7 @@ let enstack_subsubgoals env se stack gls=
 	    let constructor = mkConstruct(ind,succ i)
 	      (* constructors numbering*) in
 	    let appterm = applist (constructor,params) in
-	    let apptype = Term.prod_applist gentyp params in
+	    let apptype = prod_applist gentyp params in
 	    let rc,_ = Reduction.dest_prod env apptype in
 	    let rec meta_aux last lenv = function
 		[] -> (last,lenv,[])
@@ -638,7 +639,7 @@ let rec build_applist prod = function
     [] -> [],prod
   | n::q ->
       let (_,typ,_) = destProd prod in
-      let ctx,head = build_applist (Term.prod_applist prod [mkMeta n]) q in
+      let ctx,head = build_applist (prod_applist prod [mkMeta n]) q in
 	(n,typ)::ctx,head
 
 let instr_suffices _then cut gls0 =
@@ -671,7 +672,7 @@ let conjunction_arity id gls =
           let gentypes=
             Inductive.arities_of_constructors ind (mib,oib) in
 	  let _ = if Array.length gentypes <> 1 then raise Not_found in
-	  let apptype = Term.prod_applist gentypes.(0) params in
+	  let apptype = prod_applist gentypes.(0) params in
 	  let rc,_ = Reduction.dest_prod env apptype in
 	    List.length rc
       | _ -> raise Not_found
@@ -1218,7 +1219,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	let gen_arities = Inductive.arities_of_constructors ind spec in
 	let f_ids typ =
 	  let sign =
-	    (prod_assum (Term.prod_applist typ params)) in
+	    (prod_assum (prod_applist typ params)) in
 	    find_intro_names sign gls in
 	let constr_args_ids = Array.map f_ids gen_arities in
 	let case_term =
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 903a647fc..a6a9838ae 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -10,6 +10,8 @@
 open Util
 open Names
 open Term
+open Vars
+open Context
 open Declarations
 open Declareops
 open Environ
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 557e9c25d..89ba7b259 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -9,6 +9,7 @@
 open Hipattern
 open Names
 open Term
+open Vars
 open Termops
 open Tacmach
 open Util
@@ -50,12 +51,11 @@ let construct_nhyps ind gls =
 (* indhyps builds the array of arrays of constructor hyps for (ind largs)*)
 let ind_hyps nevar ind largs gls=
   let types= Inductiveops.arities_of_constructors (pf_env gls) ind in
-  let lp=Array.length types in
-  let myhyps i=
-    let t1=Term.prod_applist types.(i) largs in
+  let myhyps t =
+    let t1=prod_applist t largs in
     let t2=snd (decompose_prod_n_assum nevar t1) in
       fst (decompose_prod_assum t2) in
-    Array.init lp myhyps
+    Array.map myhyps types
 
 let special_nf gl=
   let infos=Closure.create_clos_infos !red_flags (pf_env gl) in
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index f1f04fdb5..59b363393 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -6,8 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open Names
+open Term
+open Context
 open Globnames
 
 val qflag : bool ref
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 6c1709140..5133801ee 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -11,6 +11,7 @@ open Sequent
 open Rules
 open Instances
 open Term
+open Vars
 open Tacmach
 open Tacticals
 
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 12b2304ac..4b15dcae5 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -11,6 +11,7 @@ open Rules
 open Errors
 open Util
 open Term
+open Vars
 open Glob_term
 open Tacmach
 open Tactics
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 8abf9d7e2..02a0dd20d 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -10,6 +10,7 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
 open Tacmach
 open Tactics
 open Tacticals
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 75fd0261a..e59f0419e 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -8,6 +8,7 @@
 
 open Util
 open Term
+open Vars
 open Termops
 open Reductionops
 
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 74d719438..6913b40ea 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -2,6 +2,8 @@ open Printer
 open Errors
 open Util
 open Term
+open Vars
+open Context
 open Namegen
 open Names
 open Declarations
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 50a4703f6..f70ce0092 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -2,6 +2,8 @@ open Printer
 open Errors
 open Util
 open Term
+open Vars
+open Context
 open Namegen
 open Names
 open Declarations
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 1ccfe3c31..088b4a0cd 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -9,6 +9,7 @@
 open Compat
 open Util
 open Term
+open Vars
 open Names
 open Pp
 open Constrexpr
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index fe48cbd88..2b4b6245a 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -2,6 +2,7 @@ open Printer
 open Pp
 open Names
 open Term
+open Vars
 open Glob_term
 open Glob_ops
 open Globnames
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 16b1881f4..e46c1a15a 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -11,6 +11,7 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
 open Pp
 open Globnames
 open Tacticals
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index bf5eba63a..65b4101a0 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -18,6 +18,8 @@ open Vernacexpr
 open Pp
 open Names
 open Term
+open Vars
+open Context
 open Termops
 open Declarations
 open Glob_term
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index a8ffd51ef..34085dca2 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Term
+open Vars
 open Namegen
 open Environ
 open Declarations
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 597b6afb6..5a77bf967 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -298,7 +298,7 @@ let rtauto_tac gls=
 		      build_form formula;
 		      build_proof [] 0 prf|]) in
   let term=
-    Term.applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in
+    applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in
   let build_end_time=System.get_time () in
   let _ = if !verbose then
     begin
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 48741525d..670cd2c47 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -13,6 +13,7 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
 open Closure
 open Environ
 open Libnames
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index 98c485dba..a7a181aa6 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -170,6 +170,7 @@ let family_of_term ty =
 module CPropRetyping =
  struct
   module T = Term
+  module V = Vars
 
   let outsort env sigma t =
    family_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma t)
@@ -178,7 +179,7 @@ module CPropRetyping =
   | [] -> typ
   | h::rest ->
       match T.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma typ) with
-        | T.Prod (na,c1,c2) -> subst_type env sigma (T.subst1 h c2) rest
+        | T.Prod (na,c1,c2) -> subst_type env sigma (V.subst1 h c2) rest
         | _ -> Errors.anomaly (Pp.str "Non-functional construction")
 
 
@@ -198,7 +199,7 @@ let typeur sigma metamap =
            with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "this is not a well-typed term"))
     | T.Rel n ->
         let (_,_,ty) = Environ.lookup_rel n env in
-        T.lift n ty
+        V.lift n ty
     | T.Var id ->
         (try
           let (_,_,ty) = Environ.lookup_named id env in
@@ -222,7 +223,7 @@ let typeur sigma metamap =
     | T.Lambda (name,c1,c2) ->
           T.mkProd (name, c1, type_of (Environ.push_rel (name,None,c1) env) c2)
     | T.LetIn (name,b,c1,c2) ->
-         T.subst1 b (type_of (Environ.push_rel (name,Some b,c1) env) c2)
+         V.subst1 b (type_of (Environ.push_rel (name,Some b,c1) env) c2)
     | T.Fix ((_,i),(_,tys,_)) -> tys.(i)
     | T.CoFix (i,(_,tys,_)) -> tys.(i)
     | T.App(f,args)->
@@ -326,6 +327,7 @@ let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids
  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
@@ -473,7 +475,7 @@ print_endline "PASSATO" ; flush stdout ;
              in
               let eta_expanded =
                let arguments =
-                List.map (T.lift uninst_vars_length) t @
+                List.map (V.lift uninst_vars_length) t @
                  Termops.rel_list 0 uninst_vars_length
                in
                 Unshare.unshare
@@ -528,7 +530,7 @@ print_endline "PASSATO" ; flush stdout ;
                match n with
                   N.Anonymous -> N.Anonymous
                 | _ ->
-                  if not fake_dependent_products && T.noccurn 1 t then
+                  if not fake_dependent_products && V.noccurn 1 t then
                    N.Anonymous
                   else
                    N.Name
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index c95cf94b6..5a3880b01 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