diff options
| author | Emilio Jesus Gallego Arias | 2018-12-05 01:50:37 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-27 23:56:18 +0100 |
| commit | 46a8fe0ef1c06ff1b64082ff87b8725dbbd4989b (patch) | |
| tree | f21203d72c419fa92da5abb01ff866da8eb20792 /plugins/funind/invfun.ml | |
| parent | 2d8f2cc01d8d35baa39144274a700a9ebc66f794 (diff) | |
[plugins] [funind] Adapt to removal of imperative proof state.
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 22 |
1 files changed, 11 insertions, 11 deletions
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 |