From 43f3634a0e75381ca473aea08415e3d262e4c066 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 11 Feb 2019 23:25:31 +0100
Subject: [vernac] Allow path for `save_proof` where no proof state is present.

In that case the terminator and proof object have to be supplied in
the ?proof argument, or else we get an anomaly.

Co-authored-by: Maxime Dénès <mail@maximedenes.fr>
---
 plugins/funind/functional_principles_proofs.ml | 2 +-
 plugins/funind/invfun.ml                       | 4 ++--
 plugins/funind/recdef.ml                       | 8 +++-----
 3 files changed, 6 insertions(+), 8 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 499005a4db..287a374ab1 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1000,7 +1000,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   lemma_type
   in
   let pstate,_ = Pfedit.by (Proofview.V82.tactic prove_replacement) pstate in
-  let pstate = Lemmas.save_proof ~pstate (Vernacexpr.(Proved(Proof_global.Transparent,None))) in
+  let pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in
   pstate, evd
 
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 136848eb67..edb698280f 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -811,7 +811,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
          let pstate = fst @@ Pfedit.by
 		   (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
                                                       (proving_tac i))) pstate in
-         let _ = Lemmas.save_proof ~pstate (Vernacexpr.(Proved(Proof_global.Transparent,None))) in
+         let _ = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt: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
@@ -871,7 +871,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
          let pstate = fst (Pfedit.by
 	   (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
               (proving_tac i))) pstate) in
-         let _pstate = Lemmas.save_proof ~pstate (Vernacexpr.(Proved(Proof_global.Transparent,None))) in
+         let _pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt: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
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 43073fe07c..0b1ae90237 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -72,7 +72,7 @@ let declare_fun f_id kind ?univs value =
   let ce = definition_entry ?univs value (*FIXME *) in
     ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
 
-let defined pstate = Lemmas.save_proof ~pstate (Vernacexpr.(Proved (Proof_global.Transparent,None)))
+let defined pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None
 
 let def_of_const t =
    match (Constr.kind t) with
@@ -1367,7 +1367,7 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type
 	       )
       		 g)
     in
-    let _pstate = Lemmas.save_proof ~pstate (Vernacexpr.Proved(opacity,None)) in
+    let _pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:opacity ~idopt:None in
     ()
   in
   let pstate = Lemmas.start_proof ~ontop:(Some pstate)
@@ -1401,8 +1401,6 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type
   with UserError _ ->
     defined pstate
 
-
-
 let com_terminate
     tcc_lemma_name
     tcc_lemma_ref
@@ -1501,7 +1499,7 @@ let (com_eqn : int -> Id.t ->
        )) pstate in
      (* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *)
 (*      Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *)
-    let _ = Flags.silently (fun () -> Lemmas.save_proof ~pstate (Vernacexpr.Proved(opacity,None))) () in
+    let _ = Flags.silently (fun () -> Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:opacity ~idopt:None) () in
     ()
 (*      Pp.msgnl (fun _ _ -> str "eqn finished"); *)
 
-- 
cgit v1.2.3