diff options
| author | ppedrot | 2013-06-22 15:21:01 +0000 |
|---|---|---|
| committer | ppedrot | 2013-06-22 15:21:01 +0000 |
| commit | 34e80b356fcccd938f114925e91c53cb33b2bd19 (patch) | |
| tree | 517da7072e340d0c36d05a2908079393e431dc43 /toplevel | |
| parent | bd7da353ea503423206e329af7a56174cb39f435 (diff) | |
Generalizing the use of maps instead of lists in the interpretation
of tactics.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16602 85f007b7-540e-0410-9357-904b9bb8a0f7
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 " ++ |