From b18b40878f071b6c7d67d1a2d031370f7a498d0b Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 3 Sep 2014 11:40:27 +0200 Subject: Print [Variant] types with the keyword [Variant]. Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced. --- kernel/subtyping.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/subtyping.ml') diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 61420d7ca..f1402a3db 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -168,7 +168,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 (arities_of_specif (mind,u) (mib2,p2)) in let check f test why = if not (test (f mib1) (f mib2)) then error (why (f mib2)) in - check (fun mib -> mib.mind_finite) (==) (fun x -> FiniteInductiveFieldExpected x); + check (fun mib -> mib.mind_finite<>Decl_kinds.CoFinite) (==) (fun x -> FiniteInductiveFieldExpected x); check (fun mib -> mib.mind_ntypes) Int.equal (fun x -> InductiveNumbersFieldExpected x); assert (List.is_empty mib1.mind_hyps && List.is_empty mib2.mind_hyps); assert (Array.length mib1.mind_packets >= 1 -- cgit v1.2.3