diff options
Diffstat (limited to 'plugins/ltac/profile_ltac.ml')
| -rw-r--r-- | plugins/ltac/profile_ltac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 58123f63e..bcb28f77c 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -374,7 +374,7 @@ let data = ref SM.empty let _ = Feedback.(add_feeder (function - | { id = State s; contents = Custom (_, "ltacprof_results", xml) } -> + | { id = s; contents = Custom (_, "ltacprof_results", xml) } -> let results = to_ltacprof_results xml in let other_results = (* Multi success can cause this *) try SM.find s !data |