From b79fd581d7d57622e6163aa59d1faf0e83760530 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 11 Feb 2004 11:57:37 +0000 Subject: [PATCH] use debug_print in a debugging message --- helm/ocaml/cic_unification/cicMetaSubst.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index 96b38e424..83daf60a6 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -593,7 +593,7 @@ let delift n subst context metasenv l t = (* order (in the sense of alpha-conversion). See comment above *) (* related to the delift function. *) debug_print "\n!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ; -print_endline "\nCicMetaSubst: UNCERTAIN" ; +debug_print "\nCicMetaSubst: UNCERTAIN" ; raise (Uncertain (sprintf "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" (ppterm subst t) -- 2.39.2