X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationUtil.ml;h=5c3936d93b0771d5feb8f52c9dd16327a629c22d;hb=c04f852241510515f06e3bec8eb79acac6e4952e;hp=51acf758f080d427cb43ff4370a00b0c63eba833;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml
index 51acf758f..5c3936d93 100644
--- a/helm/software/components/acic_content/cicNotationUtil.ml
+++ b/helm/software/components/acic_content/cicNotationUtil.ml
@@ -85,11 +85,13 @@ let visit_layout k = function
   | Ast.Over (t1, t2) -> Ast.Over (k t1, k t2)
   | Ast.Atop (t1, t2) -> Ast.Atop (k t1, k t2)
   | Ast.Frac (t1, t2) -> Ast.Frac (k t1, k t2)
+  | Ast.InfRule (t1, t2, t3) -> Ast.InfRule (k t1, k t2, k t3)
   | Ast.Sqrt t -> Ast.Sqrt (k t)
   | Ast.Root (arg, index) -> Ast.Root (k arg, k index)
   | Ast.Break -> Ast.Break
   | Ast.Box (kind, terms) -> Ast.Box (kind, List.map k terms)
   | Ast.Group terms -> Ast.Group (List.map k terms)
+  | Ast.Mstyle (l, term) -> Ast.Mstyle (l, List.map k term)
 
 let visit_magic k = function
   | Ast.List0 (t, l) -> Ast.List0 (k t, l)
@@ -136,7 +138,7 @@ let names_of_term t =
   let aux = function
     | Ast.NumVar s
     | Ast.IdentVar s
-    | Ast.TermVar s -> s
+    | Ast.TermVar (s,_) -> s
     | _ -> assert false
   in
     List.map aux (variables_of_term t)
@@ -229,7 +231,7 @@ let meta_names_of_term term =
   and aux_variable = function
     | Ast.NumVar name -> add_name name
     | Ast.IdentVar name -> add_name name
-    | Ast.TermVar name -> add_name name
+    | Ast.TermVar (name,_) -> add_name name
     | Ast.FreshVar _ -> ()
     | Ast.Ascription _ -> assert false
   and aux_magic = function