diff options
| author | Emilio Jesus Gallego Arias | 2020-03-09 06:32:00 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-30 19:05:36 -0400 |
| commit | 5f937b2f8532b2ccf36c62557934cc2c9150005b (patch) | |
| tree | 3c08d6e963654ad191b4b313f989976ed84a5efb /plugins | |
| parent | 5749a2360f9d0d7c8901a1264863339442964ca7 (diff) | |
[proof] Miscellaneous cleanup on proof info handling
After the refactorings proof information is organized in a slightly
different way thus the lower layers don't need to pass info back
anymore.
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 446026c4c8..28cf5c7d98 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 { name; 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 (fun x -> x)) lemma in match entries with | [entry] -> entry, hook |