From eadb00648127c9a535b533d51189dce41ef16db7 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sun, 17 Feb 2019 10:10:22 +0100
Subject: Multiple payload types in tokens

Instead of just string (and empty strings for tokens without payload)
---
 plugins/ltac/tacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index b770b97384..814be64f81 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -48,7 +48,7 @@ let atactic n =
   else Aentryl (Pltac.tactic_expr, string_of_int n)
 
 type entry_name = EntryName :
-  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name
+  'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Extend.symbol -> entry_name
 
 (** Quite ad-hoc *)
 let get_tacentry n m =
-- 
cgit v1.2.3