diff options
| author | Maxime Dénès | 2018-12-12 09:57:09 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-12-12 09:57:09 +0100 |
| commit | d87c4c472478fbcb30de6efabc68473ee36849a1 (patch) | |
| tree | 5b4e1cb66298db57b978374422822ffdf2673100 /proofs/proof_global.ml | |
| parent | 850dfbf59f52b0d3dcba237ee2af5ce99fd1bcd2 (diff) | |
| parent | d00472c59d15259b486868c5ccdb50b6e602a548 (diff) | |
Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 67e19df0e7..76a1e61ad2 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -422,9 +422,9 @@ let return_proof ?(allow_partial=false) () = let proofs = Proof.partial_proof proof in let _,_,_,_, evd = Proof.proof proof in let eff = Evd.eval_side_effects evd in - (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate - side-effects... This may explain why one need to uniquize side-effects - thereafter... *) + (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate + side-effects... This may explain why one need to uniquize side-effects + thereafter... *) let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in proofs, Evd.evar_universe_context evd end else @@ -432,9 +432,9 @@ let return_proof ?(allow_partial=false) () = let evd = Proof.return ~pid proof in let eff = Evd.eval_side_effects evd in let evd = Evd.minimize_universes evd in - (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate - side-effects... This may explain why one need to uniquize side-effects - thereafter... *) + (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate + side-effects... This may explain why one need to uniquize side-effects + thereafter... *) let proofs = List.map (fun (c, _) -> (EConstr.to_constr evd c, eff)) initial_goals in proofs, Evd.evar_universe_context evd |