[comFixpoing] Refactor hybrid interactive command modality

3 files changed, 17 insertions, 16 deletions

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index c266178594..3f77cb4cca 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -259,12 +259,11 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
         { Lemmas.Recthm.name; typ
         ; args = List.map RelDecl.get_name ctx; impargs})
       fixnames fixtypes fiximps in
-  let init_tac =
-    Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in
+  let init_terms = Some fixdefs in
   let evd = Evd.from_ctx ctx in
   let lemma =
     Lemmas.start_lemma_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl
-      evd (Some(cofix,indexes,init_tac)) thms None in
+      evd (Some(cofix,indexes,init_terms)) thms None in
   (* Declare notations *)
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   lemma
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 9b8bf6528b..3646e73ce1 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -144,18 +144,22 @@ let rec_tac_initializer finite guard thms snl =
 let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recguard thms snl =
   let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in
   let init_tac, compute_guard = match recguard with
-  | Some (finite,guard,init_tac) ->
+  | Some (finite,guard,init_terms) ->
     let rec_tac = rec_tac_initializer finite guard thms snl in
-    Some (match init_tac with
-        | None ->
-          Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms)
-        | Some tacl ->
-          Tacticals.New.tclTHENS rec_tac
-            List.(map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms)
-      ),guard
+    let term_tac =
+      match init_terms with
+      | None ->
+        List.map intro_tac thms
+      | Some init_terms ->
+        (* This is the case for hybrid proof mode / definition
+           fixpoint, where terms for some constants are given with := *)
+        let tacl = List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) init_terms in
+        List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms
+    in
+    Tacticals.New.tclTHENS rec_tac term_tac, guard
   | None ->
     let () = match thms with [_] -> () | _ -> assert false in
-    Some (intro_tac (List.hd thms)), [] in
+    intro_tac (List.hd thms), [] in
   match thms with
   | [] -> CErrors.anomaly (Pp.str "No proof to start.")
   | { Recthm.name; typ; impargs; _}::other_thms ->
@@ -170,9 +174,7 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua
            } in
     let lemma = start_lemma ~name ~poly ~udecl ~info sigma (EConstr.of_constr typ) in
     pf_map (Proof_global.map_proof (fun p ->
-        match init_tac with
-        | None -> p
-        | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p)) lemma
+        pi1 @@ Proof.run_tactic Global.(env ()) init_tac p)) lemma
 
 (************************************************************************)
 (* Commom constant saving path, for both Qed and Admitted               *)
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 67230e30f7..471c955311 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -103,7 +103,7 @@ val start_lemma_with_initialization
   -> kind:Decls.logical_kind
   -> udecl:UState.universe_decl
   -> Evd.evar_map
-  -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option
+  -> (bool * lemma_possible_guards * Constr.t option list option) option
   -> Recthm.t list
   -> int list option
   -> t