]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_content/cicNotationUtil.ml
Huge commit with several changes:
[helm.git] / helm / software / components / acic_content / cicNotationUtil.ml
index 60fe6357d5f1c4c878187f12e086c6ce49cd3006..b426863cf613e7f77d1123bb89cf747fe4ac18cf 100644 (file)
@@ -62,6 +62,7 @@ let visit_ast ?(special_k = fun _ -> assert false)
       | Ast.Magic _
       | Ast.Variable _) as t -> special_k t
     | (Ast.Ident _
+      | Ast.NRef _
       | Ast.Implicit
       | Ast.Num _
       | Ast.Sort _
@@ -326,13 +327,21 @@ let dressn ~sep:sauces =
 let find_appl_pattern_uris ap =
   let rec aux acc =
     function
-    | Ast.UriPattern uri -> uri :: acc
+    | Ast.UriPattern uri -> `Uri uri :: acc
+    | Ast.NRefPattern nref -> `NRef nref :: acc
     | Ast.ImplicitPattern
     | Ast.VarPattern _ -> acc
     | Ast.ApplPattern apl -> List.fold_left aux acc apl
   in
   let uris = aux [] ap in
-  HExtlib.list_uniq (List.fast_sort UriManager.compare uris)
+  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)
 
 let rec find_branch =
   function