notation fixed to be NON associative by default

[helm.git] / helm / software / components / content_pres / termContentPres.ml

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index 89dba29879c05208045c4685cc2e6c3f0e92b319..85edd595c2aed439e70b6e504afd0fb8bf1ee050 100644 (file)
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -98,17 +98,16 @@ let pp_ast0 t k =
   let rec aux =
     function
     | Ast.Appl ts ->
-        let rec aux_args pos =
+        let rec aux_args level =
           function
           | [] -> []
           | [ last ] ->
-              let last = k last in
-              [ last ]
+              [ Ast.AttributedTerm (`Level level,k last) ]
           | hd :: tl ->
-              (k hd) :: aux_args `Inner tl
+              (Ast.AttributedTerm (`Level level, k hd)) :: aux_args 71 tl
         in
         add_level_info Ast.apply_prec 
-          (hovbox true true (CicNotationUtil.dress break (aux_args `Left ts)))
+          (hovbox true true (CicNotationUtil.dress break (aux_args 70 ts)))
     | Ast.Binder (binder_kind, (id, ty), body) ->
         add_level_info Ast.binder_prec
           (hvbox false true