From 46a8fe0ef1c06ff1b64082ff87b8725dbbd4989b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 5 Dec 2018 01:50:37 +0100
Subject: [plugins] [funind] Adapt to removal of imperative proof state.

---
 plugins/funind/invfun.ml | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 37dbfec4c9..136848eb67 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -802,16 +802,16 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
 	     Ensures by: obvious
 	 i*)
 	 let lem_id = mk_correct_id f_id in
-	 let (typ,_) = lemmas_types_infos.(i) in 
-	 Lemmas.start_proof
+         let (typ,_) = lemmas_types_infos.(i) in
+         let pstate = Lemmas.start_proof ~ontop:None
 	   lem_id
            (Decl_kinds.Global,false,((Decl_kinds.Proof Decl_kinds.Theorem)))
            !evd
-           typ;
-	 ignore (Pfedit.by
+           typ in
+         let pstate = fst @@ Pfedit.by
 		   (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
-						      (proving_tac i))));
-         (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))));
+                                                      (proving_tac i))) pstate in
+         let _ = Lemmas.save_proof ~pstate (Vernacexpr.(Proved(Proof_global.Transparent,None))) in
 	 let finfo = find_Function_infos (fst f_as_constant) in
 	 (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *)
 	 let _,lem_cst_constr = Evd.fresh_global
@@ -865,13 +865,13 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
 	     Ensures by: obvious
 	   i*)
 	 let lem_id = mk_complete_id f_id in
-	 Lemmas.start_proof lem_id
+         let pstate = Lemmas.start_proof ~ontop:None lem_id
            (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) sigma
-         (fst lemmas_types_infos.(i));
-	 ignore (Pfedit.by
+         (fst lemmas_types_infos.(i)) in
+         let pstate = fst (Pfedit.by
 	   (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
-	      (proving_tac i)))) ;
-         (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))));
+              (proving_tac i))) pstate) in
+         let _pstate = Lemmas.save_proof ~pstate (Vernacexpr.(Proved(Proof_global.Transparent,None))) in
 	 let finfo = find_Function_infos (fst f_as_constant) in
 	 let _,lem_cst_constr = Evd.fresh_global
 				  (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
-- 
cgit v1.2.3