Abstraction de constr

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

1 files changed, 6 insertions, 33 deletions

diff --git a/kernel/term.mli b/kernel/term.mli
index fa0d076730..5758942596 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -59,20 +59,9 @@ type 'a oper =
 (* [VAR] is used for named variables and [Rel] for variables as
    de Bruijn indices. *)
 
-type constr =
-  | DOP0 of sorts oper
-  | DOP1 of sorts oper * constr
-  | DOP2 of sorts oper * constr * constr
-  | DOPN of sorts oper * constr array
-  | DLAM of name * constr
-  | DLAMV of name * constr array
-  | CLam of name * typed_type * constr
-  | CPrd of name * typed_type * constr
-  | CLet of name * constr * typed_type * constr
-  | VAR of identifier
-  | Rel of int
-
-and typed_type
+type constr
+
+type typed_type
 
 type flat_arity = (name * constr) list * sorts
 
@@ -609,33 +598,17 @@ val subst_vars : identifier list -> constr -> constr
 val rel_vect : int -> int -> constr array
 val rel_list : int -> int -> constr list
 
-(*i************************************************************************i*)
-(*i Pour Closure 
-(* Explicit substitutions of type ['a]. [ESID] = 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
-  | 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_liftn  : int -> 'a subs -> 'a subs
-val subs_lift  : 'a subs -> 'a subs
-val subs_shft  : int * 'a subs -> 'a subs
-val expand_rel : int -> 'a subs -> (int * 'a, int) union
-i*)
-(*s Lifts. [ELSHFT(l,n)] == lift of [n], then apply [lift l].
+(*s Compact representation of implicit lifts. \\
+   [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_spec =
   | ELID
   | ELSHFT of lift_spec * int
   | ELLFT of int * lift_spec
 val el_shft : int -> lift_spec -> lift_spec
+val el_liftn : int -> lift_spec -> lift_spec
 val el_lift : lift_spec -> lift_spec
 val reloc_rel: int -> lift_spec -> int
-(*i*)
 
 (*s Occur check functions. *)