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

6 files changed, 10 insertions, 5 deletions

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 557e9c25d0..89ba7b259f 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 f1f04fdb54..59b3633931 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 6c1709140b..5133801ee7 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 12b2304ac0..4b15dcae5d 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 8abf9d7e22..02a0dd20dd 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 75fd0261ac..e59f0419eb 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