]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_content/cicNotationPp.ml
notation support fixed to parentesize in a more sane way and
[helm.git] / helm / software / components / acic_content / cicNotationPp.ml
index 4f94fa742464fa6bd3787c3cd693de347c231587..a0f9dc2f12a8fb7e61ca82756e8f3c463a3519de 100644 (file)
@@ -250,8 +250,8 @@ and pp_sep_opt = function
 and pp_variable = function
   | Ast.NumVar s -> "number " ^ s
   | Ast.IdentVar s -> "ident " ^ s
-  | Ast.TermVar (s,None) -> s
-  | Ast.TermVar (s,Some l) -> "term " ^string_of_int l 
+  | Ast.TermVar (s,Ast.Self _) -> s
+  | Ast.TermVar (s,Ast.Level l) -> "term " ^string_of_int l 
   | Ast.Ascription (t, n) -> assert false
   | Ast.FreshVar n -> "fresh " ^ n
 
@@ -328,8 +328,7 @@ let rec pp_value = function
 
 let rec pp_value_type =
   function
-  | Env.TermType None -> "Term"
-  | Env.TermType (Some l) -> "Term "^string_of_int l
+  | Env.TermType l -> "Term "^string_of_int l
   | Env.StringType -> "String"
   | Env.NumType -> "Number"
   | Env.OptType t -> "Maybe " ^ pp_value_type t