From 6624459e492164b3d189e3518864379ff985bf8c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 10 Sep 2014 12:56:12 +0200
Subject: Fix generation of inductive elimination principle for primitive
 records. Let r.(p) be a strict subterm of r during the guardness check.

---
 kernel/inductive.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 6975544acf..58909ce012 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -814,6 +814,13 @@ let rec subterm_specif renv stack t =
       (* Metas and evars are considered OK *)
     | (Meta _|Evar _) -> Dead_code
 
+    | Proj (p, c) -> 
+      let subt = subterm_specif renv stack c in
+	(match subt with
+	| Subterm (s, wf) -> Subterm (Strict, wf)
+	| Dead_code -> Dead_code
+	| Not_subterm -> Not_subterm)
+
       (* Other terms are not subterms *)
     | _ -> Not_subterm
 
-- 
cgit v1.2.3