diff options
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 |