Project

General

Profile

« Previous | Next » 

Revision dccec723

Added by LĂ©lio Brun over 3 years ago

a version that almost work for the k-inuctive two_counters example

View differences:

src/lustre_types.mli
140 140
  hand_loc : Location.t;
141 141
}
142 142

  
143
type proof_annotation = Kinduction of int
144

  
143 145
type contract_desc = {
144 146
  consts : var_decl list;
145 147
  locals : var_decl list;
......
149 151
  modes : contract_mode list;
150 152
  imports : contract_import list;
151 153
  spec_loc : Location.t;
154
  proof : proof_annotation option
152 155
}
153 156

  
154
type 'a node_spec_t = Contract of 'a | NodeSpec of ident * 'a option
157
type 'a node_spec_t = Contract of 'a | NodeSpec of ident
155 158

  
156 159
type node_desc = {
157 160
  node_id : ident;

Also available in: Unified diff