From 5ef9ec31b2e7acb2f58da1aa13c822992f65e45b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 5 Mar 2004 16:43:46 +0000 Subject: [PATCH] Debugging message removed. --- helm/ocaml/cic_unification/cicMetaSubst.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index d7b52acfa..9695d714b 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -602,7 +602,6 @@ 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_string "\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