From de0085539583f59dc7c4bf4e272e18711d565466 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Thu, 13 Jul 2006 14:28:31 +0000 Subject: Imported Upstream version 8.0pl3+8.1beta.2 --- pretyping/recordops.mli | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) (limited to 'pretyping/recordops.mli') 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 -- cgit v1.2.3