]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/content2presMatcher.ml
parameter sintax added to axiom statement
[helm.git] / helm / software / components / content_pres / content2presMatcher.ml
index 0e85618896833b254b52e12970ff81f6a3f96b72..23f62092496d16eb7b47dd086d0ba0b017671616 100644 (file)
@@ -36,7 +36,7 @@ let get_tag term0 =
   let subterms = ref [] in
   let map_term t =
     subterms := t :: !subterms ; 
-    Ast.Implicit
+    Ast.Implicit `JustOne
   in
   let rec aux t = 
     CicNotationUtil.visit_ast