diff options
Diffstat (limited to 'toplevel/himsg.ml')
| -rw-r--r-- | toplevel/himsg.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 18638ad8b..c0f1903df 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1052,7 +1052,7 @@ let is_defined_ltac trace = let explain_ltac_call_trace (nrep,last,trace,loc) = let calls = - (nrep,last) :: List.rev (List.map(fun(n,_,ck)->(n,ck))trace) + (nrep,last) :: List.rev_map (fun(n,_,ck)->(n,ck)) trace in let pr_call (n,ck) = (match ck with |