diff options
| author | Pierre-Marie Pédrot | 2018-10-27 14:04:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-27 14:04:32 +0200 |
| commit | 788ff535ed27d5142cd18878f8478bfc161945cd (patch) | |
| tree | cd513a51eaaa0ed5552c319cdc38b875bf7f2abc /proofs/proof.ml | |
| parent | be144dcaa1d1d8ff22e9e39f49fd247e813ac1f8 (diff) | |
| parent | fb1c2a017ef8112e061771db14ccc6cc1f09d41c (diff) | |
Merge PR #8741: [typeclasses] functionalize typeclass evar handling
Diffstat (limited to 'proofs/proof.ml')
| -rw-r--r-- | proofs/proof.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 70a08e4966..8220949856 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -386,7 +386,7 @@ let run_tactic env tac pr = (* Check that retrieved given up is empty *) if not (List.is_empty retrieved_given_up) then CErrors.anomaly Pp.(str "Evars generated outside of proof engine (e.g. V82, clear, ...) are not supposed to be explicitly given up."); - let sigma = List.fold_left Proofview.Unsafe.mark_as_goal sigma retrieved in + let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in Proofview.Unsafe.tclEVARS sigma >>= fun () -> Proofview.tclUNIT retrieved in |