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/vernacinterp.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/vernacinterp.ml')
| -rw-r--r-- | vernac/vernacinterp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index eb299222dd..14f477663d 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -209,7 +209,7 @@ and interp_control ~st ({ CAst.v = cmd } as vernac) = let before_univs = Global.universes () in let pstack = interp_expr ~atts:cmd.attrs ~st cmd.expr in if before_univs == Global.universes () then pstack - else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack) + else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Declare.update_global_env) pstack) ~st (* XXX: This won't properly set the proof mode, as of today, it is @@ -251,7 +251,7 @@ let interp_gen ~verbosely ~st ~interp_fn cmd = try vernac_timeout (fun st -> let v_mod = if verbosely then Flags.verbosely else Flags.silently in let ontop = v_mod (interp_fn ~st) cmd in - Vernacstate.Proof_global.set ontop [@ocaml.warning "-3"]; + Vernacstate.Declare.set ontop [@ocaml.warning "-3"]; Vernacstate.freeze_interp_state ~marshallable:false ) st with exn -> |