]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - ocaml/problems.ml
Added second problem with bombs and pacmans: it works!
[fireball-separation.git] / ocaml / problems.ml
index 15fe980880a155791384577cac5cda70f52d3cba..b604231c89bae9fb0be52c3b78abe940720953d7 100644 (file)
@@ -336,13 +336,10 @@ let n3 () = magic_conv
 
 (* ************************************************************************** *)
 
-(* let o1 () = magic_conv (Some"BOT") [] [] ["*"];; *)
-
-let o1 () = magic_conv None [] ["x BOT"] ["*"];;
-
 let o1 () = magic_conv None [] ["x a b"; "x (_. BOT) c"] ["*"];;
+let o2 () = magic_conv None [] ["x (y (_. BOT) a) c"; "x (y a PAC) d"] ["*"];;
 
-main [o1() ];;
+main [o1() ; o2() ];;
 
 (* main ([
  p2 ; p4 ; p5 ; p6 ; p7 ; p8 ; p9 ; p10 ; p11 ; p12 ; p13 ;