X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fast2pres.ml;h=9679501ab460d2c8ae707edfbc36db396037ac22;hb=5a9b1f46a8e866382a71d686e689e9e5907f1824;hp=934223e5ce276644c3875d145d83a5d339fa279e;hpb=ac0a12080b434bf0daafc08e9da240eb57f47280;p=helm.git

diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index 934223e5c..9679501ab 100644
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -28,11 +28,10 @@
 (*                           PROJECT HELM                                 *)
 (*                                                                        *)
 (*                Andrea Asperti <asperti@cs.unibo.it>                    *)
-(*                             28/6/2003                                   *)
+(*                             28/6/2003                                  *)
 (*                                                                        *)
 (**************************************************************************)
 
-module P = Mpresentation;;
 module A = CicAst;;
 
 let symbol_table = Hashtbl.create 503;;
@@ -130,6 +129,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 +169,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 +188,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;
@@ -288,6 +306,7 @@ and make_subst start_txt varname body end_txt =
     [Box.Text([],end_txt)] 
 	  
 and pretty_append l ast tail =
+  prerr_endline("pretty riceve: " ^ (CicAstPp.pp_term ast));
   if is_big ast then
     [Box.H([],l);
      Box.H([],Box.skip::(bigast2box ast)::tail)]