]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_content/cicNotationUtil.ml
initial support for notation that specifies the precedence of term variables, that...
[helm.git] / helm / software / components / acic_content / cicNotationUtil.ml
index 51acf758f080d427cb43ff4370a00b0c63eba833..d4a55b353adf41221cd44958e294c6ef38ee59a9 100644 (file)
@@ -136,7 +136,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 +229,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