From 17b5c56ab72d42f3cf71390e0f9beed360c9777f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 9 Mar 2021 07:45:54 +0100
Subject: Adding an Ltac2 API to manipulate inductive types.

Fixes #10095: Get list of constructors of Inductive.
---
 user-contrib/Ltac2/tac2ffi.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'user-contrib/Ltac2/tac2ffi.mli')

diff --git a/user-contrib/Ltac2/tac2ffi.mli b/user-contrib/Ltac2/tac2ffi.mli
index c9aa50389e..e87ad7139c 100644
--- a/user-contrib/Ltac2/tac2ffi.mli
+++ b/user-contrib/Ltac2/tac2ffi.mli
@@ -184,6 +184,7 @@ val val_binder : (Name.t Context.binder_annot * types) Val.tag
 val val_univ : Univ.Level.t Val.tag
 val val_free : Id.Set.t Val.tag
 val val_ltac1 : Geninterp.Val.t Val.tag
+val val_ind_data : (Names.Ind.t * Declarations.mutual_inductive_body) Val.tag
 
 val val_exn : Exninfo.iexn Tac2dyn.Val.tag
 (** Toplevel representation of OCaml exceptions. Invariant: no [LtacError]
-- 
cgit v1.2.3