X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationUtil.ml;h=b426863cf613e7f77d1123bb89cf747fe4ac18cf;hb=72cd94b68037956a70b98cfa54f316fd54e52bae;hp=60fe6357d5f1c4c878187f12e086c6ce49cd3006;hpb=f524a0d716de2bdc0874aace8f82f6289034eccf;p=helm.git diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml index 60fe6357d..b426863cf 100644 --- a/helm/software/components/acic_content/cicNotationUtil.ml +++ b/helm/software/components/acic_content/cicNotationUtil.ml @@ -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