aboutsummaryrefslogtreecommitdiff
path: root/motus/js/motus.ml
diff options
context:
space:
mode:
authorSébastien Dailly <sebastien@dailly.me>2022-02-11 09:22:18 +0100
committerSébastien Dailly <sebastien@dailly.me>2022-02-11 09:28:26 +0100
commit82bb54622a47bb092094c8efab8200b12817c5b4 (patch)
treef160d66a09d2bf0e8f2bdbef5dbec17126ecd4a1 /motus/js/motus.ml
parentd20d14b4f4a903ef9aea4c01dd46fab5ecbab6ae (diff)
Hide structure in motus solver
Diffstat (limited to 'motus/js/motus.ml')
-rw-r--r--motus/js/motus.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/motus/js/motus.ml b/motus/js/motus.ml
index f2995df..a2bcbd3 100644
--- a/motus/js/motus.ml
+++ b/motus/js/motus.ml
@@ -172,7 +172,10 @@ let main
let last_element =
S.map
(fun ev ->
- match (ev.State.current_prop, ev.State.analysis.number) with
+ match
+ ( ev.State.current_prop
+ , Motus_lib.Persistence.list_size ev.State.analysis )
+ with
| [], _ | _, 1 -> Some (Jstr.v "true")
| _, _ -> None )
ev