From e89c5c3de0f00de2732f385087a3461b4e6f3a84 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 31 Aug 2017 19:36:50 +0200
Subject: Expand the primitive functions on terms.

---
 src/tac2ffi.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/tac2ffi.mli')

diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index cf1d7e81a1..e836319349 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -80,6 +80,7 @@ val val_inductive : inductive Val.tag
 val val_constant : Constant.t Val.tag
 val val_constructor : constructor Val.tag
 val val_projection : Projection.t Val.tag
+val val_case : Constr.case_info Val.tag
 val val_univ : Univ.universe_level Val.tag
 val val_kont : (Exninfo.iexn -> valexpr Proofview.tactic) Val.tag
 val val_free : Id.Set.t Val.tag
-- 
cgit v1.2.3