From 9c73e11bdcea5880501572c31d3ee66abf95299d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 26 Nov 2018 03:10:40 +0100
Subject: [ssreflect] Export more parsing witnesses.

This is needed in order to serialize ssreflect programs properly,
similar to #6795.
---
 plugins/ssr/ssrparser.mli | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

(limited to 'plugins/ssr/ssrparser.mli')

diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index 862a93765d..a2cbd3c9c8 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -28,10 +28,22 @@ open Ssrmatching
 open Ssrast
 open Ssrequality
 
+type ssrfwdview = ast_closure_term list
+type ssreqid = ssripat option
+type ssrarg = ssrfwdview * (ssreqid * (cpattern ssragens * ssripats))
+
+val wit_ssripatrep : ssripat Genarg.uniform_genarg_type
+val wit_ssrarg : ssrarg Genarg.uniform_genarg_type
 val wit_ssrrwargs : ssrrwarg list Genarg.uniform_genarg_type
 val wit_ssrclauses : clauses Genarg.uniform_genarg_type
 val wit_ssrcasearg : (cpattern ssragens) ssrmovearg Genarg.uniform_genarg_type
 val wit_ssrmovearg : (cpattern ssragens) ssrmovearg Genarg.uniform_genarg_type
 val wit_ssrapplyarg : ssrapplyarg Genarg.uniform_genarg_type
 val wit_ssrhavefwdwbinders :
-  (Tacexpr.raw_tactic_expr fwdbinders, Tacexpr.glob_tactic_expr fwdbinders, Tacinterp.Value.t fwdbinders) Genarg.genarg_type
+  (Tacexpr.raw_tactic_expr fwdbinders,
+   Tacexpr.glob_tactic_expr fwdbinders,
+   Tacinterp.Value.t fwdbinders) Genarg.genarg_type
+val wit_ssrhintarg :
+  (Tacexpr.raw_tactic_expr ssrhint,
+   Tacexpr.glob_tactic_expr ssrhint,
+   Tacinterp.Value.t ssrhint) Genarg.genarg_type
-- 
cgit v1.2.3