From 842e504b575199aab7bca96c01b3c5d8ef28f712 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 14 Dec 2006 18:48:00 +0000 Subject: [PATCH] Debugging code commented out. --- helm/software/components/tactics/universe.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/tactics/universe.ml b/helm/software/components/tactics/universe.ml index eeff1fa96..1de149270 100644 --- a/helm/software/components/tactics/universe.ml +++ b/helm/software/components/tactics/universe.ml @@ -93,7 +93,7 @@ let index univ key term = (* flexible terms are not indexed *) if key = Cic.Meta(-1,[]) then univ else - (prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term); + ((*prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);*) TI.index univ key term) ;; -- 2.39.2