From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 16 Feb 2004 09:42:44 +0000 (+0000)
Subject: - added arrow notation
X-Git-Tag: v0_0_4~199
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fd4eed43223b7aeabc680d94f06db9e2a87f4a4c;p=helm.git

- 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 934223e5c..b0b1dd4f7 100644
--- 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 ee60c4279..02cf5511c 100644
--- 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"