swh:1:snp:f92f30fa3090eae65efe8d40c3d27dad22819990
Tip revision: 73afe4fd59a1bb6609c7550047158a58deea2fd1 authored by Benjamin Gregoire on 04 June 2021, 05:35:25 UTC
improve error msg for proc
improve error msg for proc
Tip revision: 73afe4f
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 : use_tuple:bool -> s_pat -> backward
val t_inline_hoare : use_tuple:bool -> s_pat -> backward
val t_inline_equiv : use_tuple:bool -> side -> s_pat -> backward
(* -------------------------------------------------------------------- *)
val process_inline : inline_info -> backward