From 5fb2050e424062540ffbf22de0838fafe4de0a41 Mon Sep 17 00:00:00 2001
From: Julien Forest
Date: Mon, 14 Apr 2014 23:22:14 +0200
Subject: Closing bug #3260 adding a new grammar entry for clauses

---
 printing/pptactic.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'printing/pptactic.ml')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 520eac8abb..e74dd9fc15 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1034,6 +1034,12 @@ let () =
     Miscprint.pr_intro_pattern
     Miscprint.pr_intro_pattern
     Miscprint.pr_intro_pattern;
+  Genprint.register_print0
+    Constrarg.wit_clause_dft_concl
+    (pr_clauses (Some true) (pr_or_metaid pr_lident))
+    (pr_clauses (Some true) pr_lident)
+    (pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id)))
+  ;
   Genprint.register_print0 Constrarg.wit_sort
     pr_glob_sort pr_glob_sort pr_sort;
   Genprint.register_print0 Stdarg.wit_int int int int;
-- 
cgit v1.2.3