diff options
Diffstat (limited to 'kernel/generic.mli')
| -rw-r--r-- | kernel/generic.mli | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/kernel/generic.mli b/kernel/generic.mli index c9d3dd73df..20b24c68a9 100644 --- a/kernel/generic.mli +++ b/kernel/generic.mli @@ -1,12 +1,17 @@ (* $Id$ *) +(*i*) open Util open Names +(*i*) exception FreeVar exception Occur +(* \label{generic_terms} + Generic terms, over any kind of operators. *) + type 'oper term = | DOP0 of 'oper (* atomic terms *) | DOP1 of 'oper * 'oper term (* operator of arity 1 *) @@ -42,9 +47,9 @@ val reloc_rel: int -> lift_spec -> int type 'a subs = | ESID (* ESID = identity *) | CONS of 'a * 'a subs (* CONS(t,S) = (S.t) parallel substitution *) - | SHIFT of int * 'a subs (* SHIFT(n,S) = (^n o S) terms in S are relocated *) + | SHIFT of int * 'a subs (* SHIFT(n,S)= (\^n o S) terms in S are relocated *) (* with n vars *) - | LIFT of int * 'a subs (* LIFT(n,S) = (%n S) stands for ((^n o S).n...1) *) + | LIFT of int * 'a subs (* LIFT(n,S)=(\%n S) stands for ((\^n o S).n...1) *) val subs_cons : 'a * 'a subs -> 'a subs val subs_lift : 'a subs -> 'a subs |