X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=b15c3603cc7457139424e0ba9a56a48819ee11f9;hb=b50b673e2ed5a8c21074cc5bdc55bb4989d45b0f;hp=3426b5acbde3d3d717a563d439b061d46accbe83;hpb=7051416c234181eaf79dedfd18005cdf0a3e0863;p=fireball-separation.git

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 3426b5a..b15c360 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -773,14 +773,13 @@ let solve (p, todo) =
    | `CompleteUnseparable s -> `Complete, `False s
    | `CompleteSeparable _ -> `Complete, `True
    | `Uncomplete -> `Uncomplete, `True in
-  match to_run with
-   | `False s -> completeness, `Unseparable s
-   | `True ->
-       try
-        let sigma = run p in
-        completeness, `Separable sigma
-       with
-       | Backtrack _ -> completeness, `Unseparable "backtrack"
+ completeness, match to_run with
+  | `False s -> `Unseparable s
+  | `True ->
+      try
+       `Separable (run p)
+      with
+       Backtrack _ -> `Unseparable "backtrack"
 ;;
 
 let check p =