- added arrow notation

- typo fixed ("Pi" vs "pi")

diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index 934223e5ce276644c3875d145d83a5d339fa279e..b0b1dd4f792930f9427f2468a1cfecab20ceebfe 100644 (file)
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -28,7 +28,7 @@
 (*                           PROJECT HELM                                 *)
 (*                                                                        *)
 (*                Andrea Asperti <asperti@cs.unibo.it>                    *)
-(*                             28/6/2003                                   *)
+(*                             28/6/2003                                  *)
 (*                                                                        *)
 (**************************************************************************)
 
@@ -130,6 +130,15 @@ and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) =
           [Box.Text([],"(");
             Box.V([],List.map ast2box l);
             Box.Text([],")")])
+    | A.Binder (`Forall, (Cic.Anonymous, typ), body)
+    | A.Binder (`Pi, (Cic.Anonymous, typ), body) ->
+       Box.V(map_attributes attr,
+             [Box.H([],[(match typ with
+                         | None -> Box.Text([], "?")
+                         | Some typ -> ast2box typ);
+                        Box.smallskip;
+                         Box.Text([], "\\to")]);
+               Box.indent(ast2box body)])
     | A.Binder(kind, var, body) ->
        Box.V(map_attributes attr,
              [Box.H([],[resolve_binder kind;
@@ -161,9 +170,18 @@ and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) =
                    [Box.V([], 
                           (make_rule "[" r)::(List.map (make_rule "|") tl));
                     Box.Text([],"]")]) in
+        let ty_box =
+          match ty with
+          | Some ty ->
+              [ Box.H([],[Box.Text([],"[");
+                         ast2box ty;
+                         Box.Text([],"]")]) ]
+          | None -> []
+        in
        if is_big arg then
          Box.V(map_attributes attr,
-               [Box.Text([],"match");
+                 ty_box @
+                 [Box.Text([],"match");
                 Box.H([],[Box.skip;
                           bigast2box arg;
                           Box.smallskip;
@@ -171,6 +189,7 @@ and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) =
                 plbox])
        else
          Box.V(map_attributes attr,
+                ty_box @
                [Box.H(map_attributes attr,
                       [Box.Text([],"match");
                        Box.smallskip;

diff --git a/helm/ocaml/cic_transformations/cicAstPp.ml b/helm/ocaml/cic_transformations/cicAstPp.ml
index ee60c427963aa3a191cd4f06c25451330b2b3c8b..02cf5511cd963a07b84c4c65b3902b0fde0f62fb 100644 (file)
--- a/helm/ocaml/cic_transformations/cicAstPp.ml
+++ b/helm/ocaml/cic_transformations/cicAstPp.ml
@@ -27,7 +27,7 @@ open Printf
 
 let pp_binder = function
   | `Lambda -> "lambda"
-  | `Pi -> "pi"
+  | `Pi -> "Pi"
   | `Exists -> "exists"
   | `Forall -> "forall"