From f9580dfa7bc89d0ca4c9d8b69d5f4b42d558234e Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 15 Apr 2015 13:51:38 +0200
Subject: Remove dirty debug printing from funind.

---
 plugins/funind/invfun.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d9ae87ecc1..d10924f886 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -378,7 +378,6 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	    observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
 	    (* Conclusion *)
 	    observe_tac "exact" (fun g ->
-				 Pp.msgnl (str "TITI " ++ pf_apply Printer.pr_lconstr_env g (app_constructor g));
 				 Proofview.V82.of_tactic (exact_check (app_constructor g)) g)  
 	  ]
       )
@@ -427,7 +426,6 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       in
       (params_bindings@lemmas_bindings)
     in
-    Pp.msgnl (str "princ_type := " ++ pf_apply Printer.pr_lconstr_env g princ_type);
     tclTHENSEQ
       [ 
 	observe_tac "principle" (Proofview.V82.of_tactic (assert_by
-- 
cgit v1.2.3