From 0c2dd4a32538ebda7c964c249f158054b6cc2e1a Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 5 Mar 2011 16:42:38 +0000 Subject: 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 --- kernel/reduction.mli | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'kernel/reduction.mli') 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 -- cgit v1.2.3