Esubst: make types of substitutions & lifts private

Allows to be sure that we apply the smart constructors.
Propagate the change to Closure, Reduction, Term, Cbv and Newring

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14386 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 13 insertions, 7 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 8d4758cfd..143d6eb49 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -514,7 +514,7 @@ let optimise_closure env c =
     let (c',(_,s)) = compact_constr (0,[]) c 1 in
     let env' =
       Array.map (fun i -> clos_rel env i) (Array.of_list s) in
-    (subs_cons (env', ESID 0),c')
+    (subs_cons (env', subs_id 0),c')
 
 let mk_lambda env t =
   let (env,t) = optimise_closure env t in
@@ -647,7 +647,7 @@ let term_of_fconstr =
       | FFix(fx,e) when is_subs_id e & is_lift_id lfts -> mkFix fx
       | FCoFix(cfx,e) when is_subs_id e & is_lift_id lfts -> mkCoFix cfx
       | _ -> to_constr term_of_fconstr_lift lfts v in
-  term_of_fconstr_lift ELID
+  term_of_fconstr_lift el_id
 
 
 
@@ -963,7 +963,7 @@ let whd_val info v =
 let norm_val info v =
   with_stats (lazy (kl info v))
 
-let inject = mk_clos (ESID 0)
+let inject = mk_clos (subs_id 0)
 
 let whd_stack infos m stk =
   let k = kni infos m stk in
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index 2e1b42d43..cbce04d62 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -23,6 +23,8 @@ type lift =
   | ELLFT of int * lift  (* ELLFT(n,l)  == apply l to de Bruijn > n *)
                          (*                 i.e under n binders *)
 
+let el_id = ELID
+
 (* compose a relocation of magnitude n *)
 let rec el_shft_rec n = function
   | ELSHFT(el,k) -> el_shft_rec (k+n) el
@@ -69,6 +71,8 @@ type 'a subs =
  * Needn't be recursive if we always use these functions
  *)
 
+let subs_id i = ESID i
+
 let subs_cons(x,s) = if Array.length x = 0 then s else CONS(x,s)
 
 let subs_liftn n = function
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index e605fa212..fe978261e 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -16,13 +16,14 @@
     - SHIFT(n,S)          = (^n o S) terms in S are relocated with n vars
     - LIFT(n,S)           = (%n S) stands for ((^n o S).n...1)
          (corresponds to S crossing n binders) *)
-type 'a subs =
+type 'a subs = private
   | ESID of int
   | CONS of 'a array * 'a subs
   | SHIFT of int * 'a subs
   | LIFT of int * 'a subs
 
 (** Derived constructors granting basic invariants *)
+val subs_id : int -> 'a subs
 val subs_cons: 'a array * 'a subs -> 'a subs
 val subs_shft: int * 'a subs -> 'a subs
 val subs_lift: 'a subs -> 'a subs
@@ -54,11 +55,12 @@ val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs
 (** Compact representation of explicit relocations
     - [ELSHFT(l,n)] == lift of [n], then apply [lift l].
     - [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *)
-type lift =
+type lift = private
   | ELID
   | ELSHFT of lift * int
   | ELLFT of int * lift
 
+val el_id : lift
 val el_shft : int -> lift -> lift
 val el_liftn : int -> lift -> lift
 val el_lift : lift -> lift
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c1c7f521a..1a286bb16 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -426,7 +426,7 @@ and convert_vect infos lft1 lft2 v1 v2 cuniv =
 
 let clos_fconv trans cv_pb evars env t1 t2 =
   let infos = trans, create_clos_infos ~evars betaiotazeta env in
-  ccnv cv_pb infos ELID ELID (inject t1) (inject t2) empty_constraint
+  ccnv cv_pb infos el_id el_id (inject t1) (inject t2) empty_constraint
 
 let trans_fconv reds cv_pb evars env t1 t2 =
   if eq_constr t1 t2 then empty_constraint
diff --git a/kernel/term.ml b/kernel/term.ml
index 99a0e6bb3..83c417d95 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -787,7 +787,7 @@ let rec exliftn el c = match kind_of_term c with
 (* Lifting the binding depth across k bindings *)
 
 let liftn n k =
-  match el_liftn (pred k) (el_shft n ELID) with
+  match el_liftn (pred k) (el_shft n el_id) with
     | ELID -> (fun c -> c)
     | el -> exliftn el