diff options
| author | Emilio Jesus Gallego Arias | 2020-04-03 00:54:53 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-15 11:12:39 -0400 |
| commit | 28fc9aff20c39a04ad0e58e1bb8ec52c13631b61 (patch) | |
| tree | 3895a0ad5d966d53d66cfcb54c0e2c24474ea9c9 /stm | |
| parent | 4a9d1b4b190e2cb3fb034882a703aa54c5059035 (diff) | |
[proof] Merge `Pfedit` into proofs.
If we remove all the legacy proof engine stuff, that would remove the
need for the view on proof almost entirely.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 076810c750..8dcd7bbfd5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2310,7 +2310,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = Option.iter PG_compat.unfreeze lemmas; PG_compat.with_current_proof (fun _ p -> feedback ~id:id Feedback.AddedAxiom; - fst (Pfedit.solve Goal_select.SelectAll None tac p), ()); + fst (Proof.solve Goal_select.SelectAll None tac p), ()); (* STATE SPEC: * - start: Modifies the input state adding a proof. * - end : maybe after recovery command. |