From 28fc9aff20c39a04ad0e58e1bb8ec52c13631b61 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 3 Apr 2020 00:54:53 -0400
Subject: [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.
---
 stm/stm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm')

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.
-- 
cgit v1.2.3