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.

1 files 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