From c684d7621bbd0cb059aee0c47cd2de78ec518f30 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sat, 17 May 2014 09:28:28 +0200
Subject: Fixing Camlp4 compilation

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

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index dc8a47864..5a65fe93a 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -170,7 +170,7 @@ let declare_tactic loc s c cl = match cl with
   let name = <:expr< Libnames.Ident($dloc$, Names.Id.of_string $name$) >> in
   declare_str_items loc
     [ <:str_item< do {
-      let obj () = Tacenv.register_ltac false false [($name$, false, $body$)] in
+      let obj () = Tacenv.register_ltac False False [($name$, False, $body$)] in
       try do {
         Tacenv.register_ml_tactic $se$ $tac$;
         Mltop.declare_cache_obj obj __coq_plugin_name; }
-- 
cgit v1.2.3