module Trace:sig
..end
Certificate traces for external verifiers
module type S =sig
..end
The interface of certificate generators
module AltErgo:S
A certificate generator for the SMT solver Alt-Ergo
module Why3:S
A certificate generator for the deductive platform Why3.
module Selected:S
The certificate generator selected by the command line options.