https://github.com/EasyCrypt/easycrypt
Revision aa75b1d7619c3372c05161f82c7bf6633fe36ee6 authored by Pierre-Yves Strub on 27 April 2018, 12:06:12 UTC, committed by Pierre-Yves Strub on 27 April 2018, 12:06:12 UTC
This makes 'seq' rules independent of hi-level tactics.
1 parent dcb1f2f
Tip revision: aa75b1d7619c3372c05161f82c7bf6633fe36ee6 authored by Pierre-Yves Strub on 27 April 2018, 12:06:12 UTC
Move the contents of process_trivial down in the API.
Move the contents of process_trivial down in the API.
Tip revision: aa75b1d
ecTerminal.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
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
type terminal
type status = [
| `ST_Ok
| `ST_Failure of exn
]
type loglevel = EcGState.loglevel
(* -------------------------------------------------------------------- *)
val interactive : terminal -> bool
val next : terminal -> EcParsetree.prog
val notice : immediate:bool -> loglevel -> string -> terminal -> unit
val finish : status -> terminal -> unit
val finalize : terminal -> unit
(* -------------------------------------------------------------------- *)
val from_channel : ?gcstats:bool -> name:string -> in_channel -> terminal
val from_tty : unit -> terminal
val from_emacs : unit -> terminal
Computing file changes ...