From 2c8275ee3e0e5cd4eb8afd24047fda7f864e0e4e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Sat, 2 Jan 2016 16:50:02 +0100
Subject: Remove useless rec flags.

---
 printing/pptactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing/pptactic.ml')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 50a543968a..7800f1edb3 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1268,7 +1268,7 @@ module Make
 
   let pr_pat_and_constr_expr pr ((c,_),_) = pr c
 
-  let rec pr_glob_tactic_level env n t =
+  let pr_glob_tactic_level env n t =
     let glob_printers =
       (strip_prod_binders_glob_constr)
     in
-- 
cgit v1.2.3