diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
| commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
| tree | 591e9e512063e34099782e2518573f15ffeac003 /pretyping/recordops.mli | |
| parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) | |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'pretyping/recordops.mli')
| -rwxr-xr-x | pretyping/recordops.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 91bc2ba1..0a05aef6 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: recordops.mli 9032 2006-07-07 16:30:34Z herbelin $ i*) +(*i $Id: recordops.mli 9082 2006-08-24 17:03:28Z herbelin $ i*) (*i*) open Names @@ -22,7 +22,7 @@ open Library constructor (the name of which defaults to Build_S) *) val declare_structure : - inductive * identifier * int * bool list * constant option list -> unit + inductive * identifier * bool list * constant option list -> unit (* [lookup_projections isp] returns the projections associated to the inductive path [isp] if it corresponds to a structure, otherwise |