collect_data_model.mli 972 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
2
3
4
5
6
7
8
9
10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11
12
13

(* Debugging function *)
val print_table:
Sylvain Dailler's avatar
Sylvain Dailler committed
14
    Smt2_model_defs.correspondence_table -> unit
15
16
17

(* From the table generated by the parser, build a list of model_element *)
val create_list:
Sylvain Dailler's avatar
Sylvain Dailler committed
18
    Smt2_model_defs.correspondence_table -> Model_parser.model_element list