Minor code uniformization.

[helm.git] / matita / components / content / notationUtil.ml

diff --git a/matita/components/content/notationUtil.ml b/matita/components/content/notationUtil.ml
index 9b663dfc680568c6f10b8e31f8bc0056295a1943..98e1ba663b9adaac3868f9e4ac8879e3cb5054f0 100644 (file)
--- a/matita/components/content/notationUtil.ml
+++ b/matita/components/content/notationUtil.ml
@@ -328,21 +328,13 @@ let dressn ~sep:sauces =
 let find_appl_pattern_uris ap =
   let rec aux acc =
     function
-    | Ast.UriPattern uri -> `Uri uri :: acc
-    | Ast.NRefPattern nref -> `NRef nref :: acc
+    | Ast.NRefPattern nref -> nref :: acc
     | Ast.ImplicitPattern
     | Ast.VarPattern _ -> acc
     | Ast.ApplPattern apl -> List.fold_left aux acc apl
   in
   let uris = aux [] ap in
-  let cmp u1 u2 =
-   match u1,u2 with
-      `Uri u1, `Uri u2 -> UriManager.compare u1 u2
-    | `NRef r1, `NRef r2 -> NReference.compare r1 r2
-    | `Uri _,`NRef _ -> -1
-    | `NRef _, `Uri _ -> 1
-  in
-  HExtlib.list_uniq (List.fast_sort cmp uris)
+  HExtlib.list_uniq (List.fast_sort NReference.compare uris)
 
 let rec find_branch =
   function
@@ -350,19 +342,6 @@ let rec find_branch =
     | Ast.Magic (Ast.If (_, t, _)) -> find_branch t
     | t -> t
 
-let cic_name_of_name = function
-  | Ast.Ident ("_", None) -> Cic.Anonymous
-  | Ast.Ident (name, None) -> Cic.Name name
-  | _ -> assert false
-
-let name_of_cic_name =
-(*   let add_dummy_xref t = Ast.AttributedTerm (`IdRef "", t) in *)
-  (* ZACK why we used to generate dummy xrefs? *)
-  let add_dummy_xref t = t in
-  function
-  | Cic.Name s -> add_dummy_xref (Ast.Ident (s, None))
-  | Cic.Anonymous -> add_dummy_xref (Ast.Ident ("_", None))
-
 let fresh_index = ref ~-1
 
 type notation_id = int