diff options
Diffstat (limited to 'plugins/funind/gen_principle.ml')
| -rw-r--r-- | plugins/funind/gen_principle.ml | 16 |
1 files changed, 2 insertions, 14 deletions
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 570b72136c..6011af74e5 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1387,15 +1387,7 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) = i*) let lem_id = mk_correct_id f_id in let (typ,_) = lemmas_types_infos.(i) in - let info = Lemmas.Info.make - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:(Decls.(IsProof Theorem)) () in - let lemma = Lemmas.start_lemma - ~name:lem_id - ~poly:false - ~info - !evd - typ in + let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false !evd typ in let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (proving_tac i)) lemma in let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None in @@ -1456,11 +1448,7 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) = Ensures by: obvious i*) let lem_id = mk_complete_id f_id in - let info = Lemmas.Info.make - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decls.(IsProof Theorem) () in - let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false ~info - sigma (fst lemmas_types_infos.(i)) in + let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false sigma (fst lemmas_types_infos.(i)) in let lemma = fst (Lemmas.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i))) lemma) in |