From f88cce2698da000ab9054da31330db70997a41a4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 16 Dec 2014 14:33:43 +0100
Subject: Fixing CAMLP4 compilation.

---
 grammar/tacextend.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'grammar')

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 25ce4cdafe..1d5bf25833 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -204,7 +204,7 @@ let declare_tactic loc s c cl = match cl with
   let name = <:expr< Names.Id.of_string $name$ >> in
   declare_str_items loc
     [ <:str_item< do {
-      let obj () = Tacenv.register_ltac ~{for_ml=True} False $name$ $body$ in
+      let obj () = Tacenv.register_ltac True False $name$ $body$ in
       try do {
         Tacenv.register_ml_tactic $se$ $tac$;
         Mltop.declare_cache_obj obj $plugin_name$; }
-- 
cgit v1.2.3