From e6127d1f65a761a27c80b81c0f1bc5fca2b74af8 Mon Sep 17 00:00:00 2001
From: Tej Chajed
Date: Thu, 16 Feb 2017 10:24:15 -0500
Subject: [cleanup] Change Id.t option to Name.t in TacFun

---
 plugins/ssrmatching/ssrmatching.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ssrmatching')

diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index fc988a2c5f..ea14bc00a9 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -1411,7 +1411,7 @@ let () =
   let name = { mltac_plugin = "ssrmatching_plugin"; mltac_tactic = "ssrpattern"; } in
   let () = Tacenv.register_ml_tactic name [|mltac|] in
   let tac =
-    TacFun ([Some (Id.of_string "pattern")],
+    TacFun ([Name (Id.of_string "pattern")],
       TacML (Loc.ghost, { mltac_name = name; mltac_index = 0 }, [])) in
   let obj () =
     Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in
-- 
cgit v1.2.3


From ebc0870ca932acf0ceea5fe513e2ca40e74c2a02 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 6 Oct 2016 17:34:12 +0200
Subject: Moving the Ltac plugin to a pack-based one.

This is cumbersome, because now code may fail at link time if it's not
referring to the correct module name. Therefore, one has to add corresponding
open statements a the top of every file depending on a Ltac module. This
includes seemingly unrelated files that use EXTEND statements.
---
 plugins/ssrmatching/ssrmatching.ml4 | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/ssrmatching')

diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index fc988a2c5f..f4f6efa4a6 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -15,6 +15,7 @@ let frozen_lexer = CLexer.freeze () ;;
 (*i camlp4use: "pa_extend.cmo" i*)
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open Names
 open Pp
 open Pcoq
-- 
cgit v1.2.3