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/recdef.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/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index c62aa0cf6b..4c5eab1a9b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1332,9 +1332,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type let lemma = build_proof env (Evd.from_env env) start_tac end_tac in Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None in - let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decls.(IsProof Lemma)) - () in + let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in let lemma = Lemmas.start_lemma ~name:na ~poly:false (* FIXME *) ~info @@ -1376,7 +1374,7 @@ let com_terminate nb_args ctx hook = let start_proof env ctx tac_start tac_end = - let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:Decls.(IsProof Lemma) () in + let info = Lemmas.Info.make ~hook () in let lemma = Lemmas.start_lemma ~name:thm_name ~poly:false (*FIXME*) ~info |