diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-05 16:42:38 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-05 16:42:38 +0000 |
| commit | 0c2dd4a32538ebda7c964c249f158054b6cc2e1a (patch) | |
| tree | 86748aeff7f6a18ee4853af8945beb10343f7855 /kernel/reduction.mli | |
| parent | 8cff4906c3e6149063a6a6c9c570b1a54775dcc8 (diff) | |
Starting being more explicit on the reasons why module subtyping fails.
Note: I'm unsure about some subtyping error case apparently involving
aliases of inductive types (middle of Subtyping.check_inductive); I
bound it to some NotEqualInductiveAliases error, but this has to be
checked.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13885 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index e0f9c375b..525651493 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -76,5 +76,7 @@ val hnf_prod_applist : env -> types -> constr list -> types val dest_prod : env -> types -> rel_context * types val dest_prod_assum : env -> types -> rel_context * types -val dest_arity : env -> types -> arity +exception NotArity + +val dest_arity : env -> types -> arity (* raise NotArity if not an arity *) val is_arity : env -> types -> bool |