diff options
| author | Pierre-Marie Pédrot | 2018-05-24 01:05:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-05-24 01:05:09 +0200 |
| commit | 9df6df865fc71ed9840fc569d3aa3cc7cf4750aa (patch) | |
| tree | 8965b5d9bc37bc7d0be341dc311fef6df43c3616 /proofs | |
| parent | b74d9500e5943317f1baf4f36b3d979d40f6105f (diff) | |
| parent | b4b515c2e61bc6ea662b48e84eb319ec8252b07d (diff) | |
Merge PR #6515: [api] Move `Vernacexpr` to parsing.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 4 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 4 |
2 files changed, 6 insertions, 2 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 97cfccb8de..d5cb5b09f9 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -78,9 +78,11 @@ type proof_object = { universes: UState.t; } +type opacity_flag = Opaque | Transparent + type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t - | Proved of Vernacexpr.opacity_flag * + | Proved of opacity_flag * Misctypes.lident option * proof_object diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index bf35fd6599..de4cec488a 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -48,10 +48,12 @@ type proof_object = { universes: UState.t; } +type opacity_flag = Opaque | Transparent + type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t - | Proved of Vernacexpr.opacity_flag * + | Proved of opacity_flag * Misctypes.lident option * proof_object type proof_terminator |