From d0305718b4141aa08675743d4f85238301f37ad7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 21 Nov 2017 14:15:37 +0100
Subject: [coq] Adapt to Coq's new functional EXTEND API.

See https://github.com/coq/coq/pull/6197
---
 src/g_ltac2.ml4 | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 080fba7103..c738cb65bd 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -831,10 +831,11 @@ let classify_ltac2 = function
 | StrSyn _ -> Vernacexpr.VtUnknown, Vernacexpr.VtNow
 | StrMut _ | StrVal _ | StrPrm _  | StrTyp _ | StrRun _ -> Vernac_classifier.classify_as_sideeff
 
-VERNAC COMMAND EXTEND VernacDeclareTactic2Definition
+VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTactic2Definition
 | [ "Ltac2" ltac2_entry(e) ] => [ classify_ltac2 e ] -> [
-    let local = Locality.LocalityFixme.consume () in
-    Tac2entries.register_struct ?local e
+    fun ~atts ~st -> let open Vernacinterp in
+    Tac2entries.register_struct ?local:atts.locality e;
+    st
   ]
 END
 
-- 
cgit v1.2.3