From 0bfa187edddb0de9bb75c55e1b3d0f08830c7ac8 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Wed, 5 Jun 2013 13:26:51 +0000
Subject: Replacing lists by maps in matching interpretation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16561 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/himsg.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index afd04f8b91..4de5f3cc22 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1080,12 +1080,12 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
 	     function (id,None) -> None | (id,Some id') -> Some(id,([],mkVar id')) in
 	   let unboundvars = List.map_filter filter unboundvars in
 	   quote (pr_glob_constr_env (Global.env()) c) ++
-	     (if not (List.is_empty unboundvars) || not (List.is_empty vars) then
+	     (if not (List.is_empty unboundvars) || not (Id.Map.is_empty vars) then
 		strbrk " (with " ++
 		  prlist_with_sep pr_comma
 		  (fun (id,c) ->
 		     pr_id id ++ str ":=" ++ Printer.pr_lconstr_under_binders c)
-		  (List.rev vars @ unboundvars) ++ str ")"
+		  (List.rev (Id.Map.bindings vars) @ unboundvars) ++ str ")"
 	      else mt())) ++
       (if Int.equal n 2 then str " (repeated twice)"
        else if n>2 then str " (repeated "++int n++str" times)"
-- 
cgit v1.2.3