diff options
Diffstat (limited to 'user-contrib/Ltac2/tac2ffi.ml')
| -rw-r--r-- | user-contrib/Ltac2/tac2ffi.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/user-contrib/Ltac2/tac2ffi.ml b/user-contrib/Ltac2/tac2ffi.ml index a09438c6bf..5f9fbc4e41 100644 --- a/user-contrib/Ltac2/tac2ffi.ml +++ b/user-contrib/Ltac2/tac2ffi.ml @@ -104,6 +104,7 @@ let val_binder = Val.create "binder" let val_univ = Val.create "universe" let val_free : Names.Id.Set.t Val.tag = Val.create "free" let val_ltac1 : Geninterp.Val.t Val.tag = Val.create "ltac1" +let val_ind_data : (Names.Ind.t * Declarations.mutual_inductive_body) Val.tag = Val.create "ind_data" let extract_val (type a) (type b) (tag : a Val.tag) (tag' : b Val.tag) (v : b) : a = match Val.eq tag tag' with |