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.
---
 stm/stm.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 2fefb7fbb3..b73d3dcdeb 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1537,7 +1537,7 @@ end = struct (* {{{ *)
 
           let st = Vernacstate.freeze_interp_state ~marshallable:false in
           stm_vernac_interp stop
-            ~proof:(pobject, Lemmas.default_lemma_info) st
+            ~proof:(pobject, Lemmas.Info.make ()) st
             { verbose = false; indentation = 0; strlen = 0;
               expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in
         ignore(Future.join checked_proof);
@@ -1677,7 +1677,7 @@ end = struct (* {{{ *)
       let pterm, _info =
         PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
 
-      let proof = pterm, Lemmas.default_lemma_info in
+      let proof = pterm, Lemmas.Info.make () in
 
       (* We jump at the beginning since the kernel handles side effects by also
        * looking at the ones that happen to be present in the current env *)
-- 
cgit v1.2.3