From 7ceed3c76e5ac752321827300f80ee974acbb54c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 24 Jan 2017 17:24:39 +0100
Subject: Fix SR breakage due to allowing fixpoints on non-rec values

We limit fixpoints to Finite inductive types, so that BiFinite
inductives (non-recursive records) are excluded from fixpoint
construction. This is a regression in the sense that e.g. fixpoints
on unit records were allowed before. Primitive records with
eta-conversion are included in the BiFinite types.

Fix deprecation

Fix error message, the inductive type needs to be recursive for fix to work
---
 kernel/inductive.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 722705bd70..a2ce3dd4a0 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1067,6 +1067,9 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
                   try find_inductive env a
                   with Not_found ->
 		    raise_err env i (RecursionNotOnInductiveType a) in
+                let mib,_ = lookup_mind_specif env (out_punivs mind) in
+                if mib.mind_finite != Finite then
+                  raise_err env i (RecursionNotOnInductiveType a);
                 (mind, (env', b))
 	      else check_occur env' (n+1) b
             else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.")
-- 
cgit v1.2.3