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

7 files changed, 21 insertions, 13 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 6177040cc..156629c19 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -12,6 +12,7 @@ open Util
 open Names
 open Nameops
 open Term
+open Vars
 open Termops
 open Namegen
 open Environ
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 7948020a9..6b794c147 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -9,6 +9,8 @@
 open Util
 open Pp
 open Term
+open Vars
+open Context
 
 (* This module implements the abstract interface to goals *)
 (* A general invariant of the module, is that a goal whose associated
@@ -64,7 +66,7 @@ let rec advance sigma g =
       | Evd.Evar_defined c -> c
       | _ -> Errors.anomaly (Pp.str "Some goal is marked as 'cleared' but is uninstantiated")
     in
-    let (e,_) = Term.destEvar v in
+    let (e,_) = destEvar v in
     let g' = { g with content = e } in
     advance sigma g'
   else
@@ -141,7 +143,7 @@ module Refinable = struct
 
   let mkEvar handle env typ _ rdefs _ _ =
     let ev = Evarutil.e_new_evar rdefs env typ in
-    let (e,_) = Term.destEvar ev in
+    let (e,_) = destEvar ev in
     handle := e::!handle;
     ev
 
@@ -260,7 +262,7 @@ let clear ids env rdefs gl info =
   let (hyps,concl) = Evarutil.clear_hyps_in_evi rdefs hyps concl ids in
   let cleared_env = Environ.reset_with_named_context hyps env in
   let cleared_concl = Evarutil.e_new_evar rdefs cleared_env concl in
-  let (cleared_evar,_) = Term.destEvar cleared_concl in
+  let (cleared_evar,_) = destEvar cleared_concl in
   let cleared_goal = descendent gl cleared_evar in
   rdefs := Evd.define gl.content cleared_concl !rdefs;
   { subgoals = [cleared_goal] }
@@ -396,7 +398,7 @@ let convert_hyp check (id,b,bt as d) env rdefs gl info =
   let new_constr =
     Evarutil.e_new_evar rdefs new_env (concl env rdefs gl info)
   in
-  let (new_evar,_) = Term.destEvar new_constr in
+  let (new_evar,_) = destEvar new_constr in
   let new_goal = descendent gl new_evar in
   rdefs := Evd.define gl.content new_constr !rdefs;
   { subgoals = [new_goal] }
@@ -409,7 +411,7 @@ let convert_concl check cl' env rdefs gl info =
     let new_constr =
       Evarutil.e_new_evar rdefs env cl'
     in
-    let (new_evar,_) = Term.destEvar new_constr in
+    let (new_evar,_) = destEvar new_constr in
     let new_goal = descendent gl new_evar in
     rdefs := Evd.define gl.content new_constr !rdefs;
     { subgoals = [new_goal] }
@@ -431,10 +433,10 @@ let rename_hyp id1 id2 env rdefs gl info =
        Errors.error ((Names.Id.to_string id2)^" is already used.");
   let new_hyps = rename_hyp_sign id1 id2 hyps in
   let new_env = Environ.reset_with_named_context new_hyps env in
-  let new_concl = Term.replace_vars [id1,mkVar id2] (concl env rdefs gl info) in
+  let new_concl = Vars.replace_vars [id1,mkVar id2] (concl env rdefs gl info) in
   let new_subproof = Evarutil.e_new_evar rdefs new_env new_concl in
-  let new_subproof = Term.replace_vars [id2,mkVar id1] new_subproof in
-  let (new_evar,_) = Term.destEvar new_subproof in
+  let new_subproof = Vars.replace_vars [id2,mkVar id1] new_subproof in
+  let (new_evar,_) = destEvar new_subproof in
   let new_goal = descendent gl new_evar in
   rdefs := Evd.define gl.content new_subproof !rdefs;
   { subgoals = [new_goal] }
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 6b587959a..4cd3e4746 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -111,7 +111,7 @@ val clear_body : Names.Id.t list -> subgoals sensitive
 
 (* Changes an hypothesis of the goal with a convertible type and body.
    Checks convertibility if the boolean argument is true. *)
-val convert_hyp : bool -> Term.named_declaration -> subgoals sensitive
+val convert_hyp : bool -> Context.named_declaration -> subgoals sensitive
 
 (* Changes the conclusion of the goal with a convertible type and body.
    Checks convertibility if the boolean argument is true. *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 7ec1b684b..a0781ae6a 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -12,6 +12,8 @@ open Util
 open Names
 open Nameops
 open Term
+open Vars
+open Context
 open Termops
 open Environ
 open Reductionops
@@ -538,7 +540,7 @@ let prim_refiner r sigma goal =
 	     push_named_context_val (id,None,t) sign,cl,sigma) in
         let (sg2,ev2,sigma) = 
 	  Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
-	let oterm = Term.mkApp (Term.mkNamedLambda id t ev2 , [| ev1 |]) in
+	let oterm = Term.mkApp (mkNamedLambda id t ev2 , [| ev1 |]) in
 	let sigma = Goal.V82.partial_solution sigma goal oterm in
         if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
 
@@ -579,7 +581,7 @@ let prim_refiner r sigma goal =
 	let (gls_evs,sigma) =  mk_sign sign all in
 	let (gls,evs) = List.split gls_evs in
 	let ids = List.map pi1 all in
-	let evs = List.map (Term.subst_vars (List.rev ids)) evs in
+	let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
 	let indxs = Array.of_list (List.map (fun n -> n-1) (List.map pi2 all)) in
 	let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
 	let typarray = Array.of_list (List.map pi3 all) in
@@ -622,7 +624,7 @@ let prim_refiner r sigma goal =
 	let (gls_evs,sigma) =  mk_sign sign all in
 	let (gls,evs) = List.split gls_evs in
 	let (ids,types) = List.split all in
-	let evs = List.map (Term.subst_vars (List.rev ids)) evs in
+	let evs = List.map (Vars.subst_vars (List.rev ids)) evs in
 	let funnames = Array.of_list (List.map (fun i -> Name i) ids) in
 	let typarray = Array.of_list types in
 	let bodies = Array.of_list evs in
@@ -695,7 +697,7 @@ let prim_refiner r sigma goal =
         let sign' = rename_hyp id1 id2 sign in
         let cl' = replace_vars [id1,mkVar id2] cl in
 	let (gl,ev,sigma) = mk_goal sign' cl' in
-	let ev = Term.replace_vars [(id2,mkVar id1)] ev in
+	let ev = Vars.replace_vars [(id2,mkVar id1)] ev in
 	let sigma = Goal.V82.partial_solution sigma goal ev in
           ([gl], sigma)
 
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index af50059b8..954e2fdb7 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -10,6 +10,7 @@
 open Evd
 open Names
 open Term
+open Context
 open Tacexpr
 open Glob_term
 open Nametab
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 063599535..33945052f 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -11,6 +11,7 @@ open Evd
 open Names
 open Libnames
 open Term
+open Context
 open Pp
 open Tacexpr
 open Glob_term
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 328a3d65b..5b502f2c9 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Term
+open Context
 open Sign
 open Environ
 open Evd