diff options
| author | Emilio Jesus Gallego Arias | 2020-03-26 17:04:16 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-31 05:17:16 -0400 |
| commit | 0eadf776ba78dcfdcab842f38f5de871ed337376 (patch) | |
| tree | d45d4b138a56b303ee40d0013911be115c538268 /vernac/vernacstate.ml | |
| parent | 7a2e41abd8559d0bd4683e513dcb0b83987a9128 (diff) | |
[proof] [stm] Force `opaque` in `close_future_proof`
Following an observation by Enrico Tassi, we remove the `opaque`
parameter from `close_future_proof`, it should never be called with
transparent constants.
We will enforce this thru typing at the proof layer soon.
Diffstat (limited to 'vernac/vernacstate.ml')
| -rw-r--r-- | vernac/vernacstate.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index b722acd1ad..a4e9c8e1ab 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -167,8 +167,8 @@ module Proof_global = struct let return_proof () = cc return_proof let return_partial_proof () = cc return_partial_proof - let close_future_proof ~opaque ~feedback_id pf = - cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~opaque ~feedback_id st pf) pt, + let close_future_proof ~feedback_id pf = + cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~feedback_id st pf) pt, Internal.get_info pt) let close_proof ~opaque ~keep_body_ucst_separate = |