diff options
Diffstat (limited to 'plugins/ssr/ssrequality.mli')
-rw-r--r-- | plugins/ssr/ssrequality.mli | 64 |
1 files changed, 64 insertions, 0 deletions
diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli new file mode 100644 index 00000000..bbcd6b90 --- /dev/null +++ b/plugins/ssr/ssrequality.mli @@ -0,0 +1,64 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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) *) +(************************************************************************) + +(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) + +open Ssrmatching_plugin +open Ssrast + +type ssrwkind = RWred of ssrsimpl | RWdef | RWeq +type ssrrule = ssrwkind * ssrterm +type ssrrwarg = (ssrdir * ssrmult) * ((ssrdocc * Ssrmatching.rpattern option) * ssrrule) + +val dir_org : ssrdir -> int + +val notimes : int +val nomult : ssrmult +val mkocc : ssrocc -> ssrdocc +val mkclr : ssrclear -> ssrdocc +val nodocc : ssrdocc +val noclr : ssrdocc + +val simpltac : Ssrast.ssrsimpl -> Tacmach.tactic + +val newssrcongrtac : + int * Ssrast.ssrterm -> + Ltac_plugin.Tacinterp.interp_sign -> + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma + + +val mk_rwarg : + Ssrast.ssrdir * (int * Ssrast.ssrmmod) -> + (Ssrast.ssrclear option * Ssrast.ssrocc) * Ssrmatching.rpattern option -> + ssrwkind * Ssrast.ssrterm -> ssrrwarg + +val norwmult : ssrdir * ssrmult +val norwocc : (Ssrast.ssrclear option * Ssrast.ssrocc) * Ssrmatching.rpattern option + +val ssrinstancesofrule : + Ltac_plugin.Tacinterp.interp_sign -> + Ssrast.ssrdir -> + Ssrast.ssrterm -> + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma + +val ssrrewritetac : + Ltac_plugin.Tacinterp.interp_sign -> + ((Ssrast.ssrdir * (int * Ssrast.ssrmmod)) * + (((Ssrast.ssrhyps option * Ssrmatching.occ) * + Ssrmatching.rpattern option) * + (ssrwkind * Ssrast.ssrterm))) + list -> Tacmach.tactic + +val ipat_rewrite : ssrocc -> ssrdir -> EConstr.t -> Tacmach.tactic + +val unlocktac : + Ltac_plugin.Tacinterp.interp_sign -> + (Ssrmatching.occ * Ssrast.ssrterm) list -> + Goal.goal Evd.sigma -> Goal.goal list Evd.sigma |