swh:1:snp:f92f30fa3090eae65efe8d40c3d27dad22819990
Tip revision: ad258e9680a2b8e8ba3b977ee8feb427417b44b8 authored by Clement Sartori on 27 March 2018, 12:38:51 UTC
no need for List.sort for maps
no need for List.sort for maps
Tip revision: ad258e9
ecPhlInline.mli
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcUtils
open EcParsetree
open EcCoreGoal.FApi
(* -------------------------------------------------------------------- *)
type i_pat =
| IPpat
| IPif of s_pat pair
| IPwhile of s_pat
and s_pat = (int * i_pat) list
(* -------------------------------------------------------------------- *)
val t_inline_bdhoare : s_pat -> backward
val t_inline_hoare : s_pat -> backward
val t_inline_equiv : side -> s_pat -> backward
(* -------------------------------------------------------------------- *)
val process_inline : inline_info -> backward