From 34c1fee1c980b433b069a59f408792142ba00f6e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Tue, 4 Apr 2017 11:54:37 +0200 Subject: Correct subtyping check for constructors --- kernel/indtypes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 91e6ec285..17ce5483c 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -375,7 +375,7 @@ let typecheck_inductive env mie = match arity with | RegularArity (_, full_arity, _) -> check_subtyping_arity_constructor envsb dosubst full_arity true; - Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt true) lc + Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt false) lc | TemplateArity _ -> () (* TODO: When disabling template polumorphism raise anomaly if this constructor is not removed from the code base *) ) inds -- cgit v1.2.3