From 59462251fec623636b3a5396253e38f6d29bf747 Mon Sep 17 00:00:00 2001
From: puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 8 Aug 2011 08:46:34 +0000
Subject: 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
---
 kernel/esubst.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/esubst.ml')

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
-- 
cgit v1.2.3