From 4dd2102b7b12efb3ff7805aab3b7f318c6e3f989 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 21 Feb 2020 15:35:13 -0500
Subject: [parsing] Track need to reinit by typing

This PR is in preparation of #9067 (together with #11647) .

Before this PR, `grammar_extend` always took an optional `reinit`
argument, even if it was never set to `Some ...`. Indeed, there is a
single case where reinit is needed; we track it now by using a
different extension rule constructor.
---
 user-contrib/Ltac2/g_ltac2.mlg    | 2 +-
 user-contrib/Ltac2/tac2entries.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'user-contrib')

diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index c1bd585f3f..5317aa4d91 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -889,7 +889,7 @@ let rules = [
 ] in
 
 Hook.set Tac2entries.register_constr_quotations begin fun () ->
-  Pcoq.grammar_extend Pcoq.Constr.operconstr None (Some (Gramlib.Gramext.Level "0"), [(None, None, rules)])
+  Pcoq.grammar_extend Pcoq.Constr.operconstr (Some (Gramlib.Gramext.Level "0"), [(None, None, rules)])
 end
 
 }
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index d6db4a735c..70cba858c9 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -643,7 +643,7 @@ let perform_notation syn st =
   | Some lev -> Some (string_of_int lev)
   in
   let rule = (lev, None, [rule]) in
-  ([Pcoq.ExtendRule (Pltac.tac2expr, None, (None, [rule]))], st)
+  ([Pcoq.ExtendRule (Pltac.tac2expr, (None, [rule]))], st)
 
 let ltac2_notation =
   Pcoq.create_grammar_command "ltac2-notation" perform_notation
-- 
cgit v1.2.3