]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_content/cicNotationUtil.ml
- xml exportation activated for the brg kernel
[helm.git] / helm / software / components / acic_content / cicNotationUtil.ml
index b426863cf613e7f77d1123bb89cf747fe4ac18cf..4e5917a154aa87abdd493d46921e0c8bd07eccf0 100644 (file)
@@ -63,7 +63,7 @@ let visit_ast ?(special_k = fun _ -> assert false)
       | Ast.Variable _) as t -> special_k t
     | (Ast.Ident _
       | Ast.NRef _
-      | Ast.Implicit
+      | Ast.Implicit _
       | Ast.Num _
       | Ast.Sort _
       | Ast.Symbol _
@@ -208,7 +208,7 @@ let meta_names_of_term term =
     | Ast.Ident (_, Some substs) -> aux_substs substs
     | Ast.Meta (_, substs) -> aux_meta_substs substs
 
-    | Ast.Implicit
+    | Ast.Implicit _
     | Ast.Ident _
     | Ast.Num _
     | Ast.Sort _