diff options
| -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 a3e380c7b7..89d384fdd3 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2001,7 +2001,7 @@ let known_state ?(redefine_qed=false) ~cache id = | Valid { proof } -> Proof_global.unfreeze proof; Proof_global.with_current_proof (fun _ p -> - Pp.feedback ~state_id:id Feedback.AddedAxiom; + feedback ~id:(State id) Feedback.AddedAxiom; fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ()); Option.iter (fun expr -> vernac_interp id { verbose = true; loc = Loc.ghost; expr; indentation = 0; |