plugins/coma/coma_typing.mli

   1 (********************************************************************)
   2 (*                                                                  *)
   3 (*  The Why3 Verification Platform   /   The Why3 Development Team  *)
   4 (*  Copyright 2010-2024 --  Inria - CNRS - Paris-Saclay University  *)
   5 (*                                                                  *)
   6 (*  This software is distributed under the terms of the GNU Lesser  *)
   7 (*  General Public License version 2.1, with the special exception  *)
   8 (*  on linking described in file LICENSE.                           *)
   9 (*                                                                  *)
  10 (********************************************************************)
  11
  12 open Why3
  13 open Coma_logic
  14 open Coma_syntax
  15
  16 val type_defn_list : Pmodule.pmodule_uc -> bool -> pdefn list ->
  17                      Pmodule.pmodule_uc * (bool * defn list) list