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

13 files changed, 16 insertions, 0 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index e05c5384a..470d2e6cf 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -13,6 +13,7 @@ open Names
 open Nameops
 open Namegen
 open Term
+open Vars
 open Termops
 open Inductiveops
 open Environ
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 2ec0c877d..a93f9be26 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Term
+open Context
 open Sign
 open Proof_type
 open Tacmach
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index f86c22bcf..cc1162168 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -48,6 +48,8 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
+open Context
 open Declarations
 open Environ
 open Inductive
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 0e4415344..18e582b31 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -12,6 +12,7 @@ open Util
 open Names
 open Nameops
 open Term
+open Vars
 open Termops
 open Namegen
 open Inductive
diff --git a/tactics/equality.mli b/tactics/equality.mli
index ddef64502..d341db4f4 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -10,6 +10,7 @@
 open Pp
 open Names
 open Term
+open Context
 open Sign
 open Evd
 open Environ
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 0ec167873..af04dcacb 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -271,6 +271,7 @@ END
 (* Hint Resolve                                                       *)
 
 open Term
+open Vars
 open Coqlib
 
 let project_hint pri l2r r =
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 7308b7091..b508fb83b 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -12,6 +12,8 @@ open Util
 open Names
 open Nameops
 open Term
+open Vars
+open Context
 open Termops
 open Namegen
 open Environ
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index c8a3ffd55..86651e76c 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -11,6 +11,7 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
 open Termops
 open Namegen
 open Sign
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 160bcfc70..03b697e8f 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -51,6 +51,7 @@ open Errors
 open Util
 open Names
 open Term
+open Vars
 open Termops
 open Namegen
 open Tacmach
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 19a2f390b..30daa03ea 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -15,6 +15,7 @@ open Names
 open Nameops
 open Namegen
 open Term
+open Vars
 open Termops
 open Reduction
 open Tacticals
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 1d97e2b94..3ab04dcbd 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -10,6 +10,7 @@ open Loc
 open Pp
 open Names
 open Term
+open Context
 open Sign
 open Tacmach
 open Proof_type
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c531a34fa..a4b89f865 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -13,6 +13,8 @@ open Names
 open Nameops
 open Sign
 open Term
+open Vars
+open Context
 open Termops
 open Namegen
 open Declarations
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 84040722e..f39ed97f8 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -10,6 +10,7 @@ open Loc
 open Pp
 open Names
 open Term
+open Context
 open Environ
 open Sign
 open Tacmach