diff options
| author | Pierre-Marie Pédrot | 2019-09-29 16:13:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-29 16:13:40 +0200 |
| commit | 41f3d8f0b0b6efbb7133cd4e44c70a1d9105c3e9 (patch) | |
| tree | 750554abbd024ea720dd4ebafbc9751f5d62325c /plugins/funind/gen_principle.ml | |
| parent | 884b413e91d293a6b2009da11f2996db0654e40f (diff) | |
| parent | 10b54c11e2db436ab077477fae862fe06e0d9395 (diff) | |
Merge PR #10673: [lemmas] Cleanup users of default proof information.
Ack-by: SkySkimmer
Reviewed-by: ppedrot
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 |