diff options
| author | Emilio Jesus Gallego Arias | 2020-04-02 01:41:20 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-15 11:12:10 -0400 |
| commit | 0c748e670ef1a81cb35c1cc55892dba141c25930 (patch) | |
| tree | d90cc4362019557a74d6d1ac46701e0d6178e8ce /vernac/vernacexpr.ml | |
| parent | 9908ce57e15a316ff692ce31f493651734998ded (diff) | |
[proof] Merge `Proof_global` into `Declare`
We place creation and saving of interactive proofs in the same module;
this will allow to make `proof_entry` private, improving invariants
and control over clients, and to reduce the API [for example next
commit will move abstract declaration into this module, removing the
exported ad-hoc `build_constant_by_tactic`]
Next step will be to unify all the common code in the interactive /
non-interactive case; but we need to tweak the handling of obligations
first.
Diffstat (limited to 'vernac/vernacexpr.ml')
| -rw-r--r-- | vernac/vernacexpr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 27663a0681..c32ac414ba 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -202,7 +202,7 @@ type syntax_modifier = type proof_end = | Admitted (* name in `Save ident` when closing goal *) - | Proved of Proof_global.opacity_flag * lident option + | Proved of Declare.opacity_flag * lident option type scheme = | InductionScheme of bool * qualid or_by_notation * sort_expr |