From 6007579ade085a60664e6b0d4596ff98c51aabf9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 17 Apr 2018 16:07:37 +0200 Subject: Using more general information for primitive records. This brings more compatibility with handling of mutual primitive records in the kernel. --- plugins/extraction/extraction.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index bbf56525a..71e09992c 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -488,7 +488,7 @@ and extract_really_ind env kn mib = Int.equal (List.length l) 1 && not (type_mem_kn kn (List.hd l)) then raise (I Singleton); if List.is_empty l then raise (I Standard); - if Option.is_empty mib.mind_record then raise (I Standard); + if mib.mind_record == Declarations.NotRecord then raise (I Standard); (* Now we're sure it's a record. *) (* First, we find its field names. *) let rec names_prod t = match Constr.kind t with -- cgit v1.2.3