From 275bf791887670020301eb6160d540d00d368e76 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 9 Feb 2007 14:53:30 +0000 Subject: [PATCH] Debugging code removed. --- helm/software/components/tactics/primitiveTactics.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index d716ed2d4..3ef39d0c5 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/components/tactics/primitiveTactics.ml @@ -628,7 +628,6 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam let term_to_refine = C.MutCase (uri,typeno,outtype,term,patterns) in -prerr_endline (CicMetaSubst.ppterm_in_context ~metasenv:metasenv' [] term_to_refine context); let refined_term,_,metasenv'',_ = CicRefine.type_of_aux' metasenv' context term_to_refine CicUniv.empty_ugraph -- 2.39.2