aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEnrico Tassi2016-06-05 14:00:43 +0200
committerEnrico Tassi2016-06-06 14:04:33 -0400
commite47f9b21b656fa31154bd52b1e155ccf059e89a3 (patch)
tree799e088ce62e2a6d261df6695d695bbd53db36c9
parentca833edfb9ce2a40b0b83b11a825ae5dc833c4cb (diff)
rebase on trunk
-rw-r--r--stm/stm.ml2
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;