1 files changed, 42 insertions, 0 deletions
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
new file mode 100644
index 00000000..b02d747b
--- /dev/null
+++ b/kernel/esubst.mli
@@ -0,0 +1,42 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: esubst.mli,v 1.3.2.1 2004/07/16 19:30:25 herbelin Exp $ *)
+
+(*s 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 =
+  | ELID
+  | ELSHFT of lift * int
+  | ELLFT of int * lift
+
+val el_shft : int -> lift -> lift
+val el_liftn : int -> lift -> lift
+val el_lift : lift -> lift
+val reloc_rel : int -> lift -> int
+val is_lift_id : lift -> bool
+
+(*s Explicit substitutions of type ['a]. [ESID n] = %n~END = bounded identity. 
+  [CONS(t,S)] = $S.t$ i.e. parallel substitution. [SHIFT(n,S)] = 
+  $(\uparrow n~o~S)$ i.e. terms in S are relocated with n vars. 
+  [LIFT(n,S)] = $(\%n~S)$ stands for $((\uparrow n~o~S).n...1)$. *)
+type 'a subs =
+  | ESID of int
+  | CONS of 'a * 'a subs
+  | SHIFT of int * 'a subs
+  | LIFT of int * 'a subs
+
+val subs_cons: 'a * 'a subs -> 'a subs
+val subs_shft: int * 'a subs -> 'a subs
+val subs_lift: 'a subs -> 'a subs
+val subs_liftn: int -> 'a subs -> 'a subs
+val subs_shift_cons: int * 'a subs * 'a -> 'a subs
+val expand_rel: int -> 'a subs -> (int * 'a, int * int option) Util.union
+val is_subs_id: 'a subs -> bool
+val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs
+\ No newline at end of file