diff options
| author | Pierre-Marie Pédrot | 2020-03-31 21:53:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-31 21:53:51 +0200 |
| commit | e98e8a03cae984a10fddc8acbe8fd781d4608b24 (patch) | |
| tree | 69e9890126ce32c0c856a35661365b88d5a9d1ae /plugins | |
| parent | ee82486472f39cbe4760a3e586d9efb152e85c24 (diff) | |
| parent | 7afd5e9fb7ba9e5fc41e41fd54eb90ee8cb13993 (diff) | |
Merge PR #11915: [proof] Split delayed and regular proof closing functions
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: ppedrot
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/gen_principle.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 568dfbe0f1..d38c3c869b 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -199,7 +199,7 @@ let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_ (* end; *) let open Proof_global in - let { entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in + let { entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false) lemma in match entries with | [entry] -> entry, hook |