]> matita.cs.unibo.it Git - helm.git/commitdiff
MutCase branches must be parsed and printed using \Rightarrow.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 5 Mar 2004 17:51:45 +0000 (17:51 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 5 Mar 2004 17:51:45 +0000 (17:51 +0000)
helm/ocaml/cic_transformations/ast2pres.ml

index dbbfff8e5e0432b2ce9e5064abbdeabf151df217..6541356993fdbeac13f725a1c1d7d442fbe4d24e 100644 (file)
@@ -153,14 +153,14 @@ and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) =
                                Box.smallskip; 
                                make_pattern constr vars;
                                Box.smallskip; 
-                               Box.Text([],"->")]);
+                               Box.Text([],"\Rightarrow")]);
                      Box.indent (bigast2box rhs)])
          else
            Box.H([],[Box.Text([],sep);
                      Box.smallskip; 
                      make_pattern constr vars;
                      Box.smallskip; 
-                     Box.Text([],"->");
+                     Box.Text([],"\Rightarrow");
                      Box.smallskip; 
                      Box.Object([],rhs)]) in
        let plbox = match pl with