From b35899e2c208e19fd4a2f375080b5418c80fbd2c Mon Sep 17 00:00:00 2001
From: puech
Date: Fri, 29 Jul 2011 14:29:29 +0000
Subject: Evarutil: replace generic list_distinct on constr by
 constr_list_distinct

This new function is a copy of Util's one, but working on Constrhash

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14365 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarutil.ml | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index a13c249081..49a7b3a266 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1258,6 +1258,21 @@ let rec expand_and_check_vars env = function
       else
 	raise Exit
 
+module Constrhash = Hashtbl.Make
+  (struct type t = constr
+	  let equal = eq_constr
+	  let hash = hash_constr
+   end)
+
+let rec constr_list_distinct l =
+  let visited = Constrhash.create 23 in
+  let rec loop = function
+    | h::t ->
+	if Constrhash.mem visited h then false
+	else (Constrhash.add visited h h; loop t)
+    | [] -> true
+  in loop l
+
 let is_unification_pattern_evar env (_,args) l t =
   List.for_all (fun x -> isRel x || isVar x) l (* common failure case *)
   &&
@@ -1280,7 +1295,7 @@ let is_unification_pattern_evar env (_,args) l t =
 	      | Var id -> List.mem id fv_ids
 	      | Rel n -> Intset.mem n fv_rels
 	      | _ -> assert false) l in
-	list_distinct deps
+	constr_list_distinct deps
     | None -> false
 
 let is_unification_pattern (env,nb) f l t =
-- 
cgit v1.2.3