From 0b1032f2acdb6f7d92c84ba3afcbf3818cc107a9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 20 Feb 2018 20:39:27 +0100
Subject: [ssreflect] Export parsing witnesses in mli file.

This is needed in order to manipulate/serialize SSR's AST.

A quicker [and maybe better] alternative would be to just remove
`ssrparser.mli`, as there are many grammar entries that still need
exporting.
---
 plugins/ssr/ssrparser.mli | 13 +++++++++++++
 1 file changed, 13 insertions(+)

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

diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index a52248614e..1305503888 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -20,3 +20,16 @@ val pr_ssrtclarg : 'a -> 'b -> (Notation_term.tolerability -> 'c -> 'd) -> 'c ->
 
 val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type
 
+(* Parsing witnesses, needed to serialize ssreflect syntax *)
+open Ssrmatching_plugin
+open Ssrmatching
+open Ssrast
+open Ssrequality
+
+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
-- 
cgit v1.2.3