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 ++++++
 printing/pptactic.mli | 2 ++
 2 files changed, 8 insertions(+)

(limited to 'printing')

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;
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index e20e3ae014..7dbdf80aac 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -55,6 +55,8 @@ type pp_tactic = {
 val declare_ml_tactic_pprule : string -> pp_tactic -> unit
 val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
 
+val pr_clauses :  bool option ->
+           ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
 val pr_raw_generic :
   (constr_expr -> std_ppcmds) ->
   (constr_expr -> std_ppcmds) ->
-- 
cgit v1.2.3