From 5aa1f1918c39c0d4130574927fa0f870e613cdea 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. --- components/tactics/universe.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/components/tactics/universe.ml b/components/tactics/universe.ml index eeff1fa96..1de149270 100644 --- a/components/tactics/universe.ml +++ b/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