From aaebc8d9d24b2e989b26333e43f6e41c6d77d01d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 13 May 2014 20:26:58 +0200
Subject: Fix the behaviour of ML tactic notations w.r.t. Imports by making
 them substitutive.

---
 toplevel/metasyntax.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a64f32d099..a398b77774 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -160,6 +160,8 @@ let inMLTacticGrammar : ml_tactic_grammar_obj -> obj =
   declare_object { (default_object "MLTacticGrammar") with
     open_function = open_ml_tactic_notation;
     cache_function = cache_ml_tactic_notation;
+    classify_function = (fun o -> Substitute o);
+    subst_function = (fun (_, o) -> o);
   }
 
 let add_ml_tactic_notation name prods atomic =
-- 
cgit v1.2.3