diff options
| author | Arnaud Spiwack | 2014-07-23 15:16:18 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-07-23 17:43:18 +0200 |
| commit | e143cffaeab1a294ca08a49443747c66bc963c29 (patch) | |
| tree | 604425df88d5cb36916d562b67b9426c7d30bd0d | |
| parent | 474197250baa3366385563bc5403a0871d106275 (diff) | |
When closing a proof, make sure that the types have their evar substituted.
When starting proofs with [start_dependent_proof], we may have initial goals with existential variables in their conclusion. They will be solved by the proof, but this information was not propagated in close proof, and the kernel failed on uninstanciated evars.
| -rw-r--r-- | proofs/proof_global.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 673f614e3a..bfbe3dd9ed 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -275,7 +275,11 @@ let close_proof ?feedback_id ~now fpl = if poly || now then Future.force univs else Proof.in_proof proof (fun x -> Evd.evar_universe_context x) in - let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None) + (* Because of dependent subgoals at the begining of proofs, we could + have existential variables in the initial types of goals, we need to + normalise them for the kernel. *) + let subst_evar k = Proof.in_proof proof (fun m -> Evd.existential_opt_value m k) in + let nf = Universes.nf_evars_and_universes_opt_subst subst_evar (Evd.evar_universe_context_subst universes) in let make_body = if poly || now then |