discriminate.mli 1.07 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2012   --   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
val meta_inst   : Theory.meta
val meta_lskept : Theory.meta
14 15
val meta_lsinst : Theory.meta

16 17 18 19
module Lsmap : sig
  type t
  val empty : t
  val add : Term.lsymbol -> Ty.ty list -> Ty.ty option -> t -> t
20 21
end

22 23 24
val ft_select_inst   : (Env.env,Ty.Sty.t) Trans.flag_trans
val ft_select_lskept : (Env.env,Term.Sls.t) Trans.flag_trans
val ft_select_lsinst : (Env.env,Lsmap.t) Trans.flag_trans