eureka! match x with [ C gfds fsd fdg fdg fdg fd gfdg fd => c ] is

[helm.git] / helm / software / components / acic_content / cicNotationPp.ml

diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml
index cfd8c8a308956cdef0466d57f5adc231c85e36ab..4d68dadf9f682e89743593f00bcc0a2322494247 100644 (file)
--- a/helm/software/components/acic_content/cicNotationPp.ml
+++ b/helm/software/components/acic_content/cicNotationPp.ml
@@ -153,6 +153,7 @@ let rec pp_term ?(pp_parens = true) t =
     | Ast.Sort `Prop -> "Prop"
     | Ast.Sort (`Type _) -> "Type"
     | Ast.Sort (`CProp _)-> "CProp"
+    | Ast.Sort (`NType s)-> "Type[" ^ s ^ "]"
     | Ast.Symbol (name, _) -> "'" ^ name
 
     | Ast.UserInput -> ""
@@ -222,6 +223,14 @@ and pp_layout = function
         (String.concat " " (List.map pp_term terms))
   | Ast.Group terms ->
       sprintf "\\GROUP [%s]" (String.concat " " (List.map pp_term terms))
+  | Ast.Mstyle (l,terms) -> 
+      sprintf "\\MSTYLE %s [%s]" 
+        (String.concat " " (List.map (fun (k,v) -> k^"="^v) l))
+        (String.concat " " (List.map pp_term terms))
+  | Ast.Mpadded (l,terms) -> 
+      sprintf "\\MSTYLE %s [%s]" 
+        (String.concat " " (List.map (fun (k,v) -> k^"="^v) l))
+        (String.concat " " (List.map pp_term terms))
 
 and pp_magic = function
   | Ast.List0 (t, sep_opt) ->