From 17ba18d81e5fe3dc153b1c12ac1b8daeb5474d48 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 2 May 2019 06:10:29 +0200
Subject: [lemmas] Turn Lemmas.info into a proper type with constructor.

Lemmas.info was a bit out of hand, as well as the parameters to the
`start_*` family. Most of the info is not needed and should hopefully
remain constrained to special cases, most callers only set the hook,
and obligations should be better served by a `start_obligation`
function soon.
---
 plugins/ltac/rewrite.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index f977ba34d2..49265802ae 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2007,9 +2007,10 @@ let add_morphism_interactive atts m n : Lemmas.t =
     | _ -> assert false
   in
   let hook = DeclareDef.Hook.make hook in
+  let info = Lemmas.Info.make ~hook () in
   Flags.silently
     (fun () ->
-       let lemma = Lemmas.start_lemma ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+       let lemma = Lemmas.start_lemma ~name:instance_id ~kind ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in
        fst (Lemmas.by (Tacinterp.interp tac) lemma)) ()
 
 let add_morphism atts binders m s n =
-- 
cgit v1.2.3