From f72efb3532caf189c55195265b16c564f9d6d3d9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 18 Jun 2020 21:05:46 +0200
Subject: [declare] Nit on regular lemma init.

---
 vernac/declare.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/vernac/declare.ml b/vernac/declare.ml
index 5a55757d34..0533689e01 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -222,11 +222,9 @@ let rec_tac_initializer finite guard thms snl =
        | _ -> assert false
 
 let start_proof_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma thm =
-  let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in
-  let init_tac = intro_tac thm in
-  let { Recthm.name; typ; impargs; _} = thm in
+  let { Recthm.name; typ; impargs; args } = thm in
+  let init_tac = Tactics.auto_intros_tac args in
   let info = Info.make ?hook ~scope ~kind ~udecl () in
-  let info = { info with Info.thms = [] } in
   (* start_lemma has the responsibility to add (name, impargs, typ)
        to thms, once Info.t is more refined this won't be necessary *)
   let lemma = start_proof ~name ~impargs ~poly ~info sigma (EConstr.of_constr typ) in
-- 
cgit v1.2.3