diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 4de5f3cc22..66eda3e80c 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1076,9 +1076,11 @@ let explain_ltac_call_trace (nrep,last,trace,loc) = quote (Pptactic.pr_glob_tactic (Global.env()) (Tacexpr.TacAtom (Loc.ghost,te))) | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) -> - let filter = - function (id,None) -> None | (id,Some id') -> Some(id,([],mkVar id')) in - let unboundvars = List.map_filter filter unboundvars in + let fold id v accu = match v with + | None -> accu + | Some id' -> (id, ([], mkVar id')) :: accu + in + let unboundvars = Id.Map.fold fold unboundvars [] in quote (pr_glob_constr_env (Global.env()) c) ++ (if not (List.is_empty unboundvars) || not (Id.Map.is_empty vars) then strbrk " (with " ++ |