Project

General

Profile

« Previous | Next » 

Revision 36454535

Added by Pierre-Loïc Garoche over 10 years ago

Merged horn_traces branch

View differences:

src/corelang.mli
80 80
| Expr_phclock of expr * rat
81 81
and call_t = ident * expr * (ident * label) option (* The third part denotes the reseting clock label and value *)
82 82

  
83
type assert_t = 
84
    {
85
      assert_expr: expr;
86
      assert_loc: Location.t
87
    } 
88

  
89 83
type eq =
90 84
    {eq_lhs: ident list;
91 85
     eq_rhs: expr;
92 86
     eq_loc: Location.t}
93 87

  
88
type assert_t = 
89
    {
90
      assert_expr: expr * eq list;
91
      assert_loc: Location.t
92
    } 
93

  
94 94
type node_desc =
95 95
    {node_id: ident;
96 96
     mutable node_type: Types.type_expr;
......
250 250

  
251 251
val update_expr_annot: expr -> LustreSpec.expr_annot -> expr
252 252

  
253
val substitute_expr: var_decl list -> eq list -> expr -> expr
253 254

  
254 255
(** Annotation expression related functions *)
255 256
val mkeexpr: Location.t ->  expr -> eexpr

Also available in: Unified diff