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 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 --- plugins/funind/invfun.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/funind/invfun.ml') 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 -- cgit v1.2.3