diff options
| -rw-r--r-- | proofs/proof_global.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index d94bc86cd7..dd0e146497 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -333,7 +333,7 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = const_entry_polymorphic = poly}) fpl initial_goals in { id = pid; entries = entries; persistence = strength; universes = universes }, - Ephemeron.get terminator + fun pr_ending -> Ephemeron.get terminator pr_ending type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context |