From 1cd62aa20ba3f9fb206f2926c8e47dd463dee863 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 20 May 2018 21:15:44 +0200
Subject: Adapt to coq/coq#7558.

Trivial renaming of the vernacular parsing entry point.
---
 src/g_ltac2.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 6189bb18cc..ac65495fe5 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -841,8 +841,8 @@ END
 let _ =
   let mode = {
     Proof_global.name = "Ltac2";
-    set = (fun () -> set_command_entry tac2mode);
-    reset = (fun () -> set_command_entry Pcoq.Vernac_.noedit_mode);
+    set = (fun () -> Pvernac.set_command_entry tac2mode);
+    reset = (fun () -> Pvernac.(set_command_entry Vernac_.noedit_mode));
   } in
   Proof_global.register_proof_mode mode
 
-- 
cgit v1.2.3