From 3d357d5f7b2eeec9c795087ea1b329761cd966d5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 3 Jan 2007 17:09:32 +0000 Subject: [PATCH] Debugging code removed. --- 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 c8d370f04..6dbdb950a 100644 --- a/helm/software/components/tactics/universe.ml +++ b/helm/software/components/tactics/universe.ml @@ -89,7 +89,7 @@ let rec dummies_of_coercions = let s' = dummies_of_coercions s in let t' = dummies_of_coercions t in Cic.LetIn (n,s',t') - | Cic.MutCase _ -> prerr_endline "mutcase";Cic.Meta (-1,[]) + | Cic.MutCase _ -> Cic.Meta (-1,[]) | t -> t ;; -- 2.39.2