From 8c6092e8c43a74a8a175a532580284124c06e34f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 22 Oct 2017 23:50:11 +0200
Subject: Adding support for syntax "let _ := e in e'" in Ltac.

Adding a file fixing #5996 and which uses this feature.
---
 plugins/ltac/tacexpr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac/tacexpr.mli')

diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 163973688..9bd3efc6b 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -254,7 +254,7 @@ and 'a gen_tactic_expr =
   | TacFail of global_flag * int or_var * 'n message_token list
   | TacInfo of 'a gen_tactic_expr
   | TacLetIn of rec_flag *
-      (Id.t located * 'a gen_tactic_arg) list *
+      (Name.t located * 'a gen_tactic_arg) list *
       'a gen_tactic_expr
   | TacMatch of lazy_flag *
       'a gen_tactic_expr *
-- 
cgit v1.2.3