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.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'printing/pptactic.mli')

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