diff options
| author | filliatr | 1999-08-19 08:17:17 +0000 |
|---|---|---|
| committer | filliatr | 1999-08-19 08:17:17 +0000 |
| commit | 10f4e87cca4f83700c9b6a8acffc081de66dc164 (patch) | |
| tree | 71d963bff3495ecd124abc9466890f83d42577f0 /kernel/generic.mli | |
| parent | 2178b546a941803548bd2699a860086ad8f5f1d5 (diff) | |
mise en place programmation literaire (generation de doc/coq.tex)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |