X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationUtil.ml;h=d4a55b353adf41221cd44958e294c6ef38ee59a9;hb=bcf9a65332d321c25761207e2fb17110dbdc8241;hp=51acf758f080d427cb43ff4370a00b0c63eba833;hpb=1bbc2dd649df75e33f2cd7fb3e5ecb15f526a442;p=helm.git diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml index 51acf758f..d4a55b353 100644 --- a/helm/software/components/acic_content/cicNotationUtil.ml +++ b/helm/software/components/acic_content/cicNotationUtil.ml @@ -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