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 | |
| 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')
| -rw-r--r-- | vernac/vernacstate.ml | 4 | ||||
| -rw-r--r-- | vernac/vernacstate.mli | 1 |
2 files changed, 2 insertions, 3 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 = diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index b6b24c9275..9c4de7720c 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -71,7 +71,6 @@ module Proof_global : sig type closed_proof = Proof_global.proof_object * Lemmas.Info.t val close_future_proof : - opaque:Proof_global.opacity_flag -> feedback_id:Stateid.t -> Proof_global.closed_proof_output Future.computation -> closed_proof |