diff options
author | Samuel Mimram <smimram@debian.org> | 2006-07-13 14:28:31 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-07-13 14:28:31 +0000 |
commit | de0085539583f59dc7c4bf4e272e18711d565466 (patch) | |
tree | 347e1d95a2df56f79a01b303e485563588179e91 /pretyping/recordops.mli | |
parent | e978da8c41d8a3c19a29036d9c569fbe2a4616b0 (diff) |
Imported Upstream version 8.0pl3+8.1beta.2upstream/8.0pl3+8.1beta.2
Diffstat (limited to 'pretyping/recordops.mli')
-rwxr-xr-x | pretyping/recordops.mli | 15 |
1 files changed, 5 insertions, 10 deletions
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 1e061dc6..91bc2ba1 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 6748 2005-02-18 22:17:50Z herbelin $ i*) +(*i $Id: recordops.mli 9032 2006-07-07 16:30:34Z herbelin $ i*) (*i*) open Names @@ -21,18 +21,13 @@ open Library (*s A structure S is a non recursive inductive type with a single constructor (the name of which defaults to Build_S) *) -type struc_typ = { - s_CONST : identifier; - s_PARAM : int; - s_PROJKIND : bool list; - s_PROJ : constant option list } - val declare_structure : inductive * identifier * int * bool list * constant option list -> unit -(* [lookup_structure isp] returns the infos associated to inductive path - [isp] if it corresponds to a structure, otherwise fails with [Not_found] *) -val lookup_structure : inductive -> struc_typ +(* [lookup_projections isp] returns the projections associated to the + inductive path [isp] if it corresponds to a structure, otherwise + it fails with [Not_found] *) +val lookup_projections : inductive -> constant option list (* raise [Not_found] if not a projection *) val find_projection_nparams : global_reference -> int |