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

34 files changed, 58 insertions, 11 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index e16e8e1cca..5d11dbc811 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -12,6 +12,8 @@ open Util
 open Names
 open Nameops
 open Term
+open Vars
+open Context
 open Termops
 open Namegen
 open Declarations
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index d9f9b9d76d..3e4b09148d 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -9,6 +9,7 @@
 open Pp
 open Names
 open Term
+open Context
 open Evd
 open Environ
 open Inductiveops
@@ -57,11 +58,11 @@ val compile_cases :
 val constr_of_pat : 
            Environ.env ->
            Evd.evar_map ref ->
-           Term.rel_declaration list ->
+           rel_declaration list ->
            Glob_term.cases_pattern ->
            Names.Id.t list ->
            Glob_term.cases_pattern *
-           (Term.rel_declaration list * Term.constr *
+           (rel_declaration list * Term.constr *
             (Term.types * Term.constr list) * Glob_term.cases_pattern) *
            Names.Id.t list
 
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index a84bbcc54a..1334fb2855 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -7,8 +7,9 @@
 (************************************************************************)
 
 open Util
-open Term
 open Names
+open Term
+open Vars
 open Closure
 open Esubst
 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 7d2ad487c9..e97e455808 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -18,6 +18,7 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
 open Reductionops
 open Environ
 open Typeops
@@ -80,7 +81,7 @@ let disc_subset x =
        Ind i ->
 	 let len = Array.length l in
 	 let sigty = delayed_force sig_typ in
-	   if Int.equal len 2 && eq_ind i (Term.destInd sigty)
+	   if Int.equal len 2 && eq_ind i (destInd sigty)
 	   then
 	     let (a, b) = pair_of_array l in
 	       Some (a, b)
@@ -190,7 +191,7 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
 		   (fun f ->
 		      mkLambda (name', a',
 				app_opt env' isevars c2
-				  (mkApp (Term.lift 1 f, [| coec1 |])))))
+				  (mkApp (lift 1 f, [| coec1 |])))))
 
       | App (c, l), App (c', l') ->
 	  (match kind_of_term c, kind_of_term c' with
@@ -200,9 +201,9 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
 	     let prod = delayed_force prod_typ in
 	       (* Sigma types *)
 	       if Int.equal len (Array.length l') && Int.equal len 2 && eq_ind i i'
-		 && (eq_ind i (Term.destInd sigT) || eq_ind i (Term.destInd prod))
+		 && (eq_ind i (destInd sigT) || eq_ind i (destInd prod))
 	       then
-		 if eq_ind i (Term.destInd sigT)
+		 if eq_ind i (destInd sigT)
 		 then
 		   begin
 		     let (a, pb), (a', pb') =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index cc900adb45..9483f0220d 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -11,6 +11,8 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
+open Context
 open Inductiveops
 open Environ
 open Glob_term
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 3a8f549046..f2f5c9effe 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -10,6 +10,7 @@ open Errors
 open Pp
 open Names
 open Term
+open Context
 open Sign
 open Environ
 open Glob_term
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 19bced3442..39e262a3c8 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -10,6 +10,7 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
 open Closure
 open Reduction
 open Reductionops
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index b3a2e2a39c..1d5dda69f7 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -11,6 +11,8 @@ open Util
 open Errors
 open Names
 open Term
+open Vars
+open Context
 open Environ
 open Termops
 open Evd
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 82dda8e0f4..5719d750e1 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -11,6 +11,8 @@ open Util
 open Pp
 open Names
 open Term
+open Vars
+open Context
 open Termops
 open Namegen
 open Pre_env
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 4db6fdd3e8..26d85ac947 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -11,6 +11,7 @@ open Util
 open Names
 open Glob_term
 open Term
+open Context
 open Sign
 open Evd
 open Environ
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 6efdf04559..28b6ac93b5 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -12,6 +12,7 @@ open Util
 open Names
 open Nameops
 open Term
+open Vars
 open Termops
 open Environ
 open Globnames
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 8904e2b7b2..c0c20a1e33 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -18,6 +18,8 @@ open Libnames
 open Globnames
 open Nameops
 open Term
+open Vars
+open Context
 open Namegen
 open Declarations
 open Declareops
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 610bde6877..b0637a972e 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -11,6 +11,8 @@ open Util
 open Names
 open Univ
 open Term
+open Vars
+open Context
 open Termops
 open Namegen
 open Declarations
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 4fcc6c6bd8..038bf465a7 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Term
+open Context
 open Declarations
 open Environ
 open Evd
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 5460d8ba1f..ab90b5601f 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -16,6 +16,8 @@ open Nameops
 open Termops
 open Reductionops
 open Term
+open Vars
+open Context
 open Pattern
 open Patternops
 open Misctypes
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index bf1adb3cf0..a2fa81750c 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -15,6 +15,7 @@
 open Util
 open Names
 open Term
+open Vars
 open Nametab
 open Nameops
 open Libnames
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index 6c982451ab..095c7a59fd 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Term
+open Context
 open Environ
 
 (*********************************************************************
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 9a2a8dce75..ed52f574ff 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -8,6 +8,7 @@
 open Pp
 open Errors
 open Term
+open Vars
 open Environ
 open Reduction
 open Univ
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index ef0869fe6f..d227e1f2af 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -12,6 +12,7 @@ open Names
 open Globnames
 open Nameops
 open Term
+open Vars
 open Glob_term
 open Glob_ops
 open Pp
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 72cc6502a2..d1a0aaf8dc 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -9,6 +9,7 @@
 open Util
 open Names
 open Term
+open Vars
 open Termops
 open Namegen
 open Environ
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d4afb3a5f6..26325872fa 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -28,6 +28,8 @@ open Names
 open Sign
 open Evd
 open Term
+open Vars
+open Context
 open Termops
 open Reductionops
 open Environ
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 6a94fa109f..b2a9bdcc55 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -10,6 +10,8 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
+open Context
 open Termops
 open Univ
 open Evd
@@ -54,7 +56,7 @@ let compare_stack_shape stk1 stk2 =
 let fold_stack2 f o sk1 sk2 =
   let rec aux o lft1 sk1 lft2 sk2 =
   let fold_array =
-    Array.fold_left2 (fun a x y -> f a (Term.lift lft1 x) (Term.lift lft2 y))
+    Array.fold_left2 (fun a x y -> f a (Vars.lift lft1 x) (Vars.lift lft2 y))
   in
   match sk1,sk2 with
   | [], [] -> o,lft1,lft2
@@ -63,11 +65,11 @@ let fold_stack2 f o sk1 sk2 =
   | Zapp [] :: q1, _ -> aux o lft1 q1 lft2 sk2
   | _, Zapp [] :: q2 -> aux o lft1 sk1 lft2 q2
   | Zapp (t1::l1) :: q1, Zapp (t2::l2) :: q2 ->
-    aux (f o (Term.lift lft1 t1) (Term.lift lft2 t2))
+    aux (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2))
       lft1 (Zapp l1 :: q1) lft2 (Zapp l2 :: q2)
   | Zcase (_,t1,a1,_) :: q1, Zcase (_,t2,a2,_) :: q2 ->
     aux (fold_array
-	   (f o (Term.lift lft1 t1) (Term.lift lft2 t2))
+	   (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2))
 	   a1 a2) lft1 q1 lft2 q2
   | Zfix ((_,(_,a1,b1)),s1,_) :: q1, Zfix ((_,(_,a2,b2)),s2,_) :: q2 ->
     let (o',_,_) = aux (fold_array (fold_array o b1 b2) a1 a2)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 1914b3b1ee..e95fc41c03 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Term
+open Context
 open Univ
 open Evd
 open Environ
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index d290d0a47e..a49e2026a1 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -10,6 +10,7 @@ open Pp
 open Errors
 open Util
 open Term
+open Vars
 open Inductive
 open Inductiveops
 open Names
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index efc2a7467f..08d2c7cdf4 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -11,6 +11,7 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
 open Libnames
 open Globnames
 open Termops
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 5056c31230..0128f8bde1 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -12,6 +12,8 @@ open Util
 open Names
 open Nameops
 open Term
+open Vars
+open Context
 open Environ
 open Locus
 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 97ac881839..9547231afb 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -10,10 +10,13 @@ open Util
 open Pp
 open Names
 open Term
+open Context
 open Sign
 open Environ
 open Locus
 
+(** TODO: merge this with Term *)
+
 (** Universes *)
 val new_univ_level : unit -> Univ.universe_level
 val new_univ : unit -> Univ.universe
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 86ff2a28fe..53171d02cb 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -11,6 +11,8 @@ open Names
 open Globnames
 open Decl_kinds
 open Term
+open Vars
+open Context
 open Sign
 open Evd
 open Environ
@@ -109,7 +111,7 @@ let dest_class_app env c =
     global_class_of_constr env cl, args
 
 let dest_class_arity env c =
-  let rels, c = Term.decompose_prod_assum c in
+  let rels, c = decompose_prod_assum c in
     rels, dest_class_app env c
 
 let class_of_constr c =
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 3f10200c03..af6824924f 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -10,6 +10,7 @@ open Names
 open Globnames
 open Decl_kinds
 open Term
+open Context
 open Sign
 open Evd
 open Environ
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index d0d90017fd..89eb217d28 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -9,6 +9,7 @@
 (*i*)
 open Names
 open Term
+open Context
 open Evd
 open Environ
 open Constrexpr
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 5155b71631..f80ff00fce 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -10,6 +10,7 @@ open Loc
 open Names
 open Decl_kinds
 open Term
+open Context
 open Sign
 open Evd
 open Environ
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 7cf7e58890..008b8b9a39 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -10,6 +10,7 @@ open Pp
 open Errors
 open Util
 open Term
+open Vars
 open Environ
 open Reductionops
 open Type_errors
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 31148ee39d..f3014424c4 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -10,6 +10,7 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
 open Termops
 open Namegen
 open Environ
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index fb8a05a97f..4b08f7517a 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -9,6 +9,7 @@
 open Names
 open Declarations
 open Term
+open Vars
 open Environ
 open Inductive
 open Reduction