blob: 47b6cc9b9687f0fea0d56467d3b93817c0c6c0df (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
*** Linearize.ml.orig 2006-02-09 11:47:55.000000000 +0100
--- Linearize.ml 2006-02-09 11:58:42.000000000 +0100
***************
*** 28,35 ****
(** val enumerate : LTL.coq_function -> node list **)
let enumerate f =
positive_rec Coq_nil (fun pc nodes ->
! match Maps.PMap.get pc (reachable f) with
| true -> Coq_cons (pc, nodes)
| false -> nodes) (coq_Psucc f.fn_entrypoint)
--- 28,36 ----
(** val enumerate : LTL.coq_function -> node list **)
let enumerate f =
+ let reach = reachable f in
positive_rec Coq_nil (fun pc nodes ->
! match Maps.PMap.get pc reach with
| true -> Coq_cons (pc, nodes)
| false -> nodes) (coq_Psucc f.fn_entrypoint)
|
