diff options
| author | Maxime Dénès | 2019-09-18 10:23:07 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-09-18 10:23:07 +0200 |
| commit | c5ecc185ccb804e02ef78012fc6ae38c092cc80a (patch) | |
| tree | 9b68d0b597610ed2b72693768752c14c501e81bd /plugins/micromega/zify.mli | |
| parent | aa851dc5939af6febe7550b75b066af04905a7ab (diff) | |
| parent | dfff69ef604e02703575cb1cb15b2f77eda5f0f4 (diff) | |
Merge PR #9856: A 'zify' tactic as a ML plugin
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: maximedenes
Ack-by: ppedrot
Ack-by: vbgl
Diffstat (limited to 'plugins/micromega/zify.mli')
| -rw-r--r-- | plugins/micromega/zify.mli | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli new file mode 100644 index 0000000000..f7844f53bc --- /dev/null +++ b/plugins/micromega/zify.mli @@ -0,0 +1,25 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +open Constrexpr + +module type S = sig val register : constr_expr -> unit val print : unit -> unit end + +module InjTable : S +module UnOp : S +module BinOp : S +module CstOp : S +module BinRel : S +module PropOp : S +module Spec : S +module Saturate : S + +val zify_tac : unit Proofview.tactic +val saturate : unit Proofview.tactic +val iter_specs : Ltac_plugin.Tacinterp.Value.t -> unit Proofview.tactic |