Revision 36454535
Added by Pierre-Loïc Garoche over 10 years ago
src/lustreSpec.ml | ||
---|---|---|
1 | 1 |
open Format |
2 | 2 |
|
3 | 3 |
type ident = Utils.ident |
4 |
type label = Utils.ident |
|
5 | 4 |
type rat = Utils.rat |
6 | 5 |
type tag = Utils.tag |
6 |
type label = Utils.ident |
|
7 | 7 |
|
8 | 8 |
type type_dec = |
9 | 9 |
{ty_dec_desc: type_dec_desc; |
... | ... | |
117 | 117 |
type assert_t = |
118 | 118 |
{ |
119 | 119 |
assert_expr: expr; |
120 |
assert_loc: Location.t |
|
120 |
assert_loc: Location.t;
|
|
121 | 121 |
} |
122 | 122 |
|
123 | 123 |
type node_desc = |
... | ... | |
177 | 177 |
| Already_bound_symbol of ident |
178 | 178 |
|
179 | 179 |
|
180 |
|
|
181 | 180 |
(* Local Variables: *) |
182 | 181 |
(* compile-command:"make -C .." *) |
183 | 182 |
(* End: *) |
Also available in: Unified diff
Merged horn_traces branch