From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 5 Oct 2005 16:09:58 +0000 (+0000)
Subject: uncommented find_cic_appl_pattern_uris
X-Git-Tag: V_0_7_2_3~245
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=df51c03d7dc9657be73fa83f3b7899ded2681402;p=helm.git

uncommented find_cic_appl_pattern_uris
---

diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml
index 966e02626..887f5bf05 100644
--- a/helm/ocaml/cic_notation/cicNotationUtil.ml
+++ b/helm/ocaml/cic_notation/cicNotationUtil.ml
@@ -303,19 +303,16 @@ let dressn ~sep:sauces =
   in
     aux
 
-(* let find_appl_pattern_uris ap =
+let find_appl_pattern_uris ap =
   let rec aux acc =
     function
-    | Ast.UriPattern uri ->
-        (try
-          ignore (List.find (fun uri' -> UriManager.eq uri uri') acc);
-          acc
-        with Not_found -> uri :: acc)
+    | Ast.UriPattern uri -> uri :: acc
     | Ast.ImplicitPattern
     | Ast.VarPattern _ -> acc
     | Ast.ApplPattern apl -> List.fold_left aux acc apl
   in
-  aux [] ap *)
+  let uris = aux [] ap in
+  HExtlib.list_uniq (List.fast_sort UriManager.compare uris)
 
 let rec find_branch =
   function
diff --git a/helm/ocaml/cic_notation/cicNotationUtil.mli b/helm/ocaml/cic_notation/cicNotationUtil.mli
index 2b035fab7..ad16a2eb6 100644
--- a/helm/ocaml/cic_notation/cicNotationUtil.mli
+++ b/helm/ocaml/cic_notation/cicNotationUtil.mli
@@ -69,8 +69,8 @@ val boxify: CicNotationPt.term list -> CicNotationPt.term
 val group: CicNotationPt.term list -> CicNotationPt.term
 val ungroup: CicNotationPt.term list -> CicNotationPt.term list
 
-(* val find_appl_pattern_uris:
-  CicNotationPt.cic_appl_pattern -> UriManager.uri list *)
+val find_appl_pattern_uris:
+  CicNotationPt.cic_appl_pattern -> UriManager.uri list
 
 val find_branch:
   CicNotationPt.term -> CicNotationPt.term