From 69822345c198aa6bf51354f6b84c7fd5d401bc9c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 23 Aug 2017 20:32:15 +0200
Subject: Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.

Renaming it register_grammars_by_name.
---
 plugins/ltac/tacentries.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index ee84be5414..8112cc4008 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -545,11 +545,10 @@ let print_located_tactic qid =
 (** Grammar *)
 
 let () =
-  let open Metasyntax in
   let entries = [
     AnyEntry Pltac.tactic_expr;
     AnyEntry Pltac.binder_tactic;
     AnyEntry Pltac.simple_tactic;
     AnyEntry Pltac.tactic_arg;
   ] in
-  register_grammar "tactic" entries
+  register_grammars_by_name "tactic" entries
-- 
cgit v1.2.3