Merge PR coq#18354: [plugins] (re)-export AST witnesses.

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <[email protected]>

plugins/extraction/g_extraction.mli

@@ -0,0 +1,13 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \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)         *)
+(************************************************************************)
+
+val wit_int_or_id: (Table.int_or_id, Table.int_or_id, Table.int_or_id) Genarg.genarg_type
+val wit_language: (Table.lang, unit, unit) Genarg.genarg_type
+val wit_mlname: (string, string, string) Genarg.genarg_type

plugins/ltac/extratactics.mli

@@ -7,3 +7,15 @@
 (*         *     GNU Lesser General Public License Version 2.1          *)
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
+
+type cmp =
+  | Eq
+  | Lt | Le
+  | Gt | Ge
+
+val wit_comparison : (cmp, cmp, cmp) Genarg.genarg_type
+
+type 'i test =
+  | Test of cmp * 'i * 'i
+
+val wit_test : (int Locus.or_var test, int Locus.or_var test, int test) Genarg.genarg_type

plugins/ssr/ssrparser.mli

@@ -227,3 +227,59 @@ module Internal : sig
   val pr_wgen : wgen -> Pp.t
 
 end
+
+val wit_ast_closure_lterm : ast_closure_term Genarg.uniform_genarg_type
+
+val wit_ast_closure_term : ast_closure_term Genarg.uniform_genarg_type
+
+val wit_ident_no_do  : Names.Id.t Genarg.uniform_genarg_type
+
+val wit_ssrbinder :
+  (ssrfwdfmt * Constrexpr.constr_expr,
+   ssrfwdfmt * Genintern.glob_constr_and_expr,
+   ssrfwdfmt * EConstr.constr) Genarg.genarg_type
+
+val wit_ssrbvar :
+  (Constrexpr.constr_expr, Genintern.glob_constr_and_expr, EConstr.constr) Genarg.genarg_type
+
+val wit_ssrclausehyps :
+  ((ssrhyps * ((ssrhyp_or_id * string) * cpattern option) option) list,
+   (ssrclear * ((ssrhyp_or_id * string) *cpattern option) option) list,
+   (ssrclear * ((ssrhyp_or_id * string) * cpattern option) option) list)
+    Genarg.genarg_type
+
+val wit_ssrclear_ne : (ssrhyps, ssrclear, ssrclear) Genarg.genarg_type
+
+val wit_ssrhoi_hyp : ssrhyp_or_id Genarg.uniform_genarg_type
+
+val wit_ssrhoi_id : ssrhyp_or_id Genarg.uniform_genarg_type
+
+val wit_ssrhyp : ssrhyp Genarg.uniform_genarg_type
+
+val wit_ssrindex : (int Locus.or_var) Genarg.uniform_genarg_type
+
+val wit_ssriorpat : ssripatss Genarg.uniform_genarg_type
+
+val wit_ssripat : ssripats Genarg.uniform_genarg_type
+val wit_ssripats : ssripats Genarg.uniform_genarg_type
+val wit_ssripats_ne  : ssripats Genarg.uniform_genarg_type
+val wit_ssrmult_ne : (int * ssrmmod) Genarg.uniform_genarg_type
+val wit_ssrortacarg :
+  (Tacexpr.raw_tactic_expr ssrhint,
+   bool * Ltac_plugin.Tacexpr.glob_tactic_expr option list,
+   bool * Geninterp.Val.t option list)
+    Genarg.genarg_type
+
+val wit_ssrortacs :
+  (Tacexpr.raw_tactic_expr option list,
+   Tacexpr.glob_tactic_expr option list,
+   Geninterp.Val.t option list)
+    Genarg.genarg_type
+
+val wit_ssrsimpl_ne :
+  ssrsimpl Genarg.uniform_genarg_type
+
+val wit_ssrstruct : Names.Id.t option Genarg.uniform_genarg_type
+
+val wit_ssrtac3arg :
+    (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type

plugins/ssr/ssrtacs.mli

@@ -35,3 +35,23 @@ val wit_ssrdgens : cpattern ssragens Genarg.uniform_genarg_type
 val wit_ssrdgens_tl : cpattern ssragens Genarg.uniform_genarg_type
 
 val wit_ssr_idcomma : Names.Id.t option option Genarg.uniform_genarg_type
+
+val wit_ssrgen :
+    (ssrdocc * cpattern, ssrdocc * cpattern, ssrdocc * cpattern) Genarg.genarg_type
+
+val wit_ssreqid : ssripat option Genarg.uniform_genarg_type
+
+val wit_ssragen :
+    (ssrdocc * ssrterm, ssrdocc * ssrterm, ssrdocc * ssrterm) Genarg.genarg_type
+
+val wit_ssragens :
+    ((ssrdocc * ssrterm) list list * ssrhyps,
+     (ssrdocc * ssrterm) list list * ssrclear,
+     (ssrdocc * ssrterm) list list * ssrclear)
+      Genarg.genarg_type
+
+val wit_ssrrwocc : ssrdocc Genarg.uniform_genarg_type
+val wit_ssrrule_ne : (ssrwkind * ssrterm) Genarg.uniform_genarg_type
+val wit_ssrrule : (ssrwkind * ssrterm) Genarg.uniform_genarg_type
+val wit_ssrpattern_squarep : (rpattern option) Genarg.uniform_genarg_type
+val wit_ssrpattern_ne_squarep : (rpattern option) Genarg.uniform_genarg_type

plugins/ssr/ssrvernac.mli

@@ -9,3 +9,20 @@
 (************************************************************************)
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+
+val wit_ssrhintref :
+  (Constrexpr.constr_expr, Genintern.glob_constr_and_expr,
+   EConstr.constr)
+    Genarg.genarg_type
+
+val wit_ssrviewpos :
+    (Ssrview.AdaptorDb.kind option,
+     Ssrview.AdaptorDb.kind option,
+     Ssrview.AdaptorDb.kind option)
+    Genarg.genarg_type
+
+val wit_ssrviewposspc :
+  (Ssrview.AdaptorDb.kind option,
+   Ssrview.AdaptorDb.kind option,
+   Ssrview.AdaptorDb.kind option)
+    Genarg.genarg_type

plugins/ssrmatching/g_ssrmatching.mli

@@ -24,3 +24,5 @@ val wit_lcpattern     : cpattern uniform_genarg_type
 (** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *)
 val rpattern         : rpattern Pcoq.Entry.t
 val wit_rpattern     : rpattern uniform_genarg_type
+
+val wit_ssrpatternarg : rpattern uniform_genarg_type