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 --- vernac/himsg.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/himsg.ml') diff --git a/vernac/himsg.ml b/vernac/himsg.ml index f00c1e604..6e827c303 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -423,7 +423,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj = str "Not enough abstractions in the definition" | RecursionNotOnInductiveType c -> str "Recursive definition on" ++ spc () ++ pr_lconstr_env env sigma c ++ - spc () ++ str "which should be an inductive type" + spc () ++ str "which should be a recursive inductive type" | RecursionOnIllegalTerm(j,(arg_env, arg),le,lt) -> let arg_env = make_all_name_different arg_env sigma in let called = -- cgit v1.2.3