From 9dce41a62c86d55f2e9bb373bf9de0ec655b4f48 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Wed, 22 Apr 2009 10:54:26 +0000 Subject: [PATCH] Disabled debug prints in the inversion principle. --- helm/software/components/tactics/inversion.ml | 2 +- helm/software/components/tactics/inversion_principle.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/components/tactics/inversion.ml b/helm/software/components/tactics/inversion.ml index 13b350daf..fa4b71178 100644 --- a/helm/software/components/tactics/inversion.ml +++ b/helm/software/components/tactics/inversion.ml @@ -28,7 +28,7 @@ exception TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple exception NotAnInductiveTypeToEliminate -let debug = true;; +let debug = false;; let debug_print = fun msg -> if debug then prerr_endline (Lazy.force msg) else () diff --git a/helm/software/components/tactics/inversion_principle.ml b/helm/software/components/tactics/inversion_principle.ml index e15e8cb63..3229a261b 100644 --- a/helm/software/components/tactics/inversion_principle.ml +++ b/helm/software/components/tactics/inversion_principle.ml @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -let debug = true;; +let debug = false;; let debug_print = fun msg -> if debug then prerr_endline (Lazy.force msg) else () -- 2.39.2