From 4341f37cf3c51ed82c23f05846c8e6e8823d3cd6 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 10 Mar 2016 19:02:16 +0100 Subject: Primitive projections: protect kernel from erroneous definitions. E.g., Inductive foo := mkFoo { bla : foo } allowed to define recursive records with eta for which conversion is incomplete. - Eta-conversion only applies to BiFinite inductives - Finiteness information is now checked by the kernel (the constructor types must be strictly non recursive for BiFinite declarations). --- pretyping/evarconv.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 637a9e50e..690b974be 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -854,7 +854,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with - | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> + | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite -> let pars = mib.Declarations.mind_nparams in (try let l1' = Stack.tail pars sk1 in -- cgit v1.2.3 From 8f5ca2a6100eb243d2a9842a13e02b793ee0aea1 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 14 Mar 2016 11:13:21 +0100 Subject: Try eta-expansion of records only on non-recursive ones --- pretyping/unification.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 31fd711bf..9b6e856b8 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -609,7 +609,7 @@ let is_eta_constructor_app env ts f l1 term = | Construct (((_, i as ind), j), u) when i == 0 && j == 1 -> let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with - | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite && + | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite && Array.length projs == Array.length l1 - mib.Declarations.mind_nparams -> (** Check that the other term is neutral *) is_neutral env ts term -- cgit v1.2.3