X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationEnv.ml;h=5b4190eb87b1abecc2782b7de23acb4336d9eecb;hb=16f2f9f9915f483089fd0f532e25ff51e2252bac;hp=5a1c4c9458d1f216ba047643e380349b4bdaec81;hpb=bcf9a65332d321c25761207e2fb17110dbdc8241;p=helm.git diff --git a/helm/software/components/acic_content/cicNotationEnv.ml b/helm/software/components/acic_content/cicNotationEnv.ml index 5a1c4c945..5b4190eb8 100644 --- a/helm/software/components/acic_content/cicNotationEnv.ml +++ b/helm/software/components/acic_content/cicNotationEnv.ml @@ -35,7 +35,7 @@ type value = | ListValue of value list type value_type = - | TermType of (int * Gramext.g_assoc) option + | TermType of int | StringType | NumType | OptType of value_type @@ -98,7 +98,7 @@ let list_declaration (n, ty) = (n, ListType ty) let declaration_of_var = function | Ast.NumVar s -> s, NumType | Ast.IdentVar s -> s, StringType - | Ast.TermVar (s,l) -> s, TermType l + | Ast.TermVar (s,(Ast.Self l|Ast.Level l)) -> s, TermType l | _ -> assert false let value_of_term = function