From e8fbc417cb1d2f63a0ec33cb967b7e0258084d48 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 24 Jan 2018 13:22:19 +0100 Subject: Fix #6621: Anomaly on fixpoint with primitive projections The implementation of the subterm relation for primitive projections was a bit wrong. I found the problem independently of this bug, and tried to see if a proof of False could be derived, but I don't think so, due to another check (check_is_subterm) that saves the kernel at the last minute. --- kernel/inductive.ml | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 28a09b81b..722705bd7 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -796,18 +796,18 @@ let rec subterm_specif renv stack t = | Proj (p, c) -> let subt = subterm_specif renv stack c in - (match subt with - | Subterm (s, wf) -> - (* We take the subterm specs of the constructor of the record *) - let wf_args = (dest_subterms wf).(0) in - (* We extract the tree of the projected argument *) - let kn = Projection.constant p in - let cb = lookup_constant kn renv.env in - let pb = Option.get cb.const_proj in - let n = pb.proj_arg in - Subterm (Strict, List.nth wf_args n) - | Dead_code -> Dead_code - | Not_subterm -> Not_subterm) + (match subt with + | Subterm (s, wf) -> + (* We take the subterm specs of the constructor of the record *) + let wf_args = (dest_subterms wf).(0) in + (* We extract the tree of the projected argument *) + let kn = Projection.constant p in + let cb = lookup_constant kn renv.env in + let pb = Option.get cb.const_proj in + let n = pb.proj_arg in + spec_of_tree (List.nth wf_args n) + | Dead_code -> Dead_code + | Not_subterm -> Not_subterm) | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _ | Construct _ | CoFix _ -> Not_subterm -- cgit v1.2.3