From f3515efc26a693f4c525ad91c37c982f4c96e6ec Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 20 Apr 2016 23:24:02 +0200
Subject: Factorizing the declaration of ML notation printing in Tacentries.

---
 ltac/tacentries.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'ltac')

diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 46e48c6953..a3e15866ee 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -360,7 +360,13 @@ let extend_atomic_tactic name entries =
   List.iteri add_atomic entries
 
 let cache_ml_tactic_notation (_, obj) =
-  extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod
+  extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod;
+  let pp_rule prods = {
+    Pptactic.pptac_level = 0 (* only level 0 supported here *);
+    pptac_prods = prods;
+  } in
+  let pp_rules = Array.map_of_list pp_rule obj.mltacobj_prod in
+  Pptactic.declare_ml_tactic_pprule obj.mltacobj_name pp_rules
 
 let open_ml_tactic_notation i obj =
   if Int.equal i 1 then cache_ml_tactic_notation obj
-- 
cgit v1.2.3