From a84ff9806f0ee77e081954453ee6afb67921eb50 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek
Date: Fri, 18 Dec 2020 09:38:34 +0100
Subject: Make ssr datastructures cpattern and rpattern public

---
 plugins/ssrmatching/ssrmatching.mli | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 17b47227cb..1573998f6f 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -22,15 +22,9 @@ open Genintern
 
 (** The type of context patterns, the patterns of the [set] tactic and
     [:] tactical. These are patterns that identify a precise subterm. *)
-type cpattern
+type cpattern = char * Genintern.glob_constr_and_expr * Geninterp.interp_sign option
 val pr_cpattern : cpattern -> Pp.t
 
-(** The type of rewrite patterns, the patterns of the [rewrite] tactic.
-    These patterns also include patterns that identify all the subterms
-    of a context (i.e. "in" prefix) *)
-type rpattern
-val pr_rpattern : rpattern -> Pp.t
-
 (** Pattern interpretation and matching *)
 
 exception NoMatch
@@ -48,6 +42,12 @@ type ('ident, 'term) ssrpattern =
 type pattern = evar_map * (constr, constr) ssrpattern
 val pp_pattern : env -> pattern -> Pp.t
 
+(** The type of rewrite patterns, the patterns of the [rewrite] tactic.
+    These patterns also include patterns that identify all the subterms
+    of a context (i.e. "in" prefix) *)
+type rpattern = (cpattern, cpattern) ssrpattern
+val pr_rpattern : rpattern -> Pp.t
+
 (** Extracts the redex and applies to it the substitution part of the pattern.
   @raise Anomaly if called on [In_T] or [In_X_In_T] *)
 val redex_of_pattern :
-- 
cgit v1.2.3