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