From 5e6145c871eea1e94566b252b4bfc4cd752f42d5 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 23 Oct 2013 22:17:07 +0000
Subject: cList: set-as-list functions are now with an explicit comparison

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/patternops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/patternops.ml')

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index e6a95a03e1..329af85266 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -212,7 +212,7 @@ let instantiate_pattern sigma lvar c =
 	with Not_found (* List.index failed *) ->
 	  let vars =
 	    List.map_filter (function Name id -> Some id | _ -> None) vars in
-	  error_instantiate_pattern id (List.subtract ctx vars)
+	  error_instantiate_pattern id (List.subtract Id.equal ctx vars)
        with Not_found (* Map.find failed *) ->
 	 x)
   | (PFix _ | PCoFix _) -> error ("Non instantiable pattern.")
-- 
cgit v1.2.3