diff options
| author |  puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-29 14:29:29 +0000 |
|---|---|---|
| committer | puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-07-29 14:29:29 +0000 |
| commit | b35899e2c208e19fd4a2f375080b5418c80fbd2c (patch) | |
| tree | 56ce600371a96720b2ed8e3d381247e8a0d57cdd /pretyping/evarutil.ml | |
| parent | 0cfb71569ad334822e9efcd82cd5215569301b27 (diff) | |
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
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index a13c24908..49a7b3a26 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 = |