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

1 files changed, 4 insertions, 0 deletions

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