diff options
| author | coq | 2000-07-19 12:17:12 +0000 |
|---|---|---|
| committer | coq | 2000-07-19 12:17:12 +0000 |
| commit | 19b494e50ce36127782c4147c64e330a06387279 (patch) | |
| tree | b49529b1e3756111265adfebca110e374fda4660 /kernel | |
| parent | a03c49aaa432c87569315569cc041b2756796e43 (diff) | |
Quelques (*i*) pour ne pas casser oczmlweb
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@557 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index fc36c7f1d7..72ba6f5114 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -433,7 +433,7 @@ val nb_lam : constr -> int (* similar to [nb_lam], but gives the number of products instead *) val nb_prod : constr -> int -(* Trop compliqué +(*i*)(* Trop compliqué (*s Various utility functions for implementing terms with bindings. *) val extract_lifted : int * constr -> constr @@ -507,7 +507,7 @@ val lam_and_popl_named : properly lifted, and then push back the products, but as lambda- abstractions *) val lambda_ize : int ->'a oper term -> 'a oper term -> 'a oper term -*) +*)(*i*) (*s Flattening and unflattening of embedded applications and casts. *) |