diff options
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index dcd86716..d49b64d9 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: inductiveops.mli 8845 2006-05-23 07:41:58Z herbelin $ i*) +(*i $Id: inductiveops.mli 9194 2006-10-01 09:25:19Z herbelin $ i*) open Names open Term @@ -66,6 +66,8 @@ val constructor_nrealhyps : env -> constructor -> int val get_full_arity_sign : env -> inductive -> rel_context +val allowed_sorts : env -> inductive -> sorts_family list + (* Extract information from an inductive family *) type constructor_summary = { |