From 07a0ec4416fae0f98c610752bc73a30a30f1bd64 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 13 Mar 2020 06:31:58 -0400
Subject: [lemmas] Remove workaround for non-uniform mutual body

In previous versions of Coq `abstract` could create non-uniform bodies
for mutually recursive definitions (c.f. bug #5065)

Thanks to changes to the trusted base this is not the case anymore,
thus we can remove the workaround.

This way mutual bodies are handled the same in the interactive and
non-interactive case.
---
 vernac/lemmas.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index a7cf1bfb76..638e6ecb54 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -231,14 +231,11 @@ end = struct
       in
       Mutual pe
 
-  let rec select_body i t =
+  let select_body i t =
     let open Constr in
     match Constr.kind t with
     | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
     | CoFix (0,decls) -> mkCoFix (i,decls)
-    | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, select_body i t2)
-    | Lambda(na,ty,t) -> mkLambda(na,ty, select_body i t)
-    | App (t, args) -> mkApp (select_body i t, args)
     | _ ->
       CErrors.anomaly
         Pp.(str "Not a proof by induction: " ++
-- 
cgit v1.2.3