]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/components/content/notationUtil.ml
Matitaweb:
[helm.git] / matitaB / components / content / notationUtil.ml
index d047eb58e17f66a649ca89276c0ebacf6cc8c715..dc914932a62bc60085b0d9c3e7e9ddfc62aaff30 100644 (file)
@@ -157,7 +157,7 @@ let keywords_of_term t =
   let rec aux = function
     | Ast.AttributedTerm (_, t) -> aux t
     | Ast.Layout l -> Ast.Layout (visit_layout aux l)
-    | Ast.Literal (`Keyword (k,_)) as t ->
+    | Ast.Literal (_,`Keyword (k,_)) as t ->
         add_keyword k;
         t
     | Ast.Literal _ as t -> t
@@ -179,7 +179,7 @@ let rec strip_attributes t =
 
 let rec get_idrefs =
   function
-  | Ast.Symbol (_,Some (_,desc)) -> [desc]
+  | Ast.Symbol (csym,Some (uri,desc)) -> [csym,uri,desc]
   | _ -> []
 
 let meta_names_of_term term =