diff options
| author | Emilio Jesus Gallego Arias | 2020-03-13 06:31:58 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-30 19:05:36 -0400 |
| commit | 07a0ec4416fae0f98c610752bc73a30a30f1bd64 (patch) | |
| tree | a8b293bcf0cc6f8567cc2a111af7acb4822763da | |
| parent | 5da15336a01d1f74fac653f69cd0a509ba05a3ab (diff) | |
[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.
| -rw-r--r-- | vernac/lemmas.ml | 5 |
1 files changed, 1 insertions, 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: " ++ |