aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-01-30 09:37:56 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-01-30 09:37:56 +0100
commitae2429e6cf0e4faa0e57bd3b1393efc3b532920a (patch)
tree3d116f422a928cfcf5f4eef9535297b3b7fa0fdb /kernel
parent76d51c51befc755d3ead6414c9609132189456e9 (diff)
parente8fbc417cb1d2f63a0ec33cb967b7e0258084d48 (diff)
Merge PR #6649: Fix #6621: Anomaly on fixpoint with primitive projections
Diffstat (limited to 'kernel')
-rw-r--r--kernel/inductive.ml24
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