snapshot (first version with working pattern matching both 3->2 and 2->1)

[helm.git] / helm / ocaml / cic_notation / cicNotationPp.ml

diff --git a/helm/ocaml/cic_notation/cicNotationPp.ml b/helm/ocaml/cic_notation/cicNotationPp.ml
index 5befd8ed2787d745ab125d3cf71943c958ab7ab9..4f79895164af5ff92e9dcdc16e3f95557cb40a19 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationPp.ml
+++ b/helm/ocaml/cic_notation/cicNotationPp.ml
@@ -28,6 +28,8 @@ open Printf
 open CicNotationEnv
 open CicNotationPt
 
+let print_attributes = true
+
 let pp_binder = function
   | `Lambda -> "lambda"
   | `Pi -> "Pi"
@@ -42,6 +44,8 @@ let pp_literal l =
     | `Number s -> s)
 
 let rec pp_term = function
+  | AttributedTerm (_, term) when print_attributes ->
+      sprintf "@[%s]" (pp_term term)
   | AttributedTerm (_, term) -> pp_term term
 
   | Appl terms ->