From 992c6ea9d35cbdf8e9d2ce870a1b3d8f7e099e7d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 16 Nov 2008 10:03:48 +0000 Subject: [PATCH] removed some printings --- helm/software/components/tactics/auto.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 09156224e..6b25982d3 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -1,4 +1,5 @@ (* Copyright (C) 2002, HELM Team. + * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -182,13 +183,17 @@ let only signature context metasenv t = in let consts = MetadataConstraints.constants_of ty in let b = MetadataConstraints.UriManagerSet.subset consts signature in - if b then (prerr_endline ("keeping " ^ (CicPp.ppterm t)); b) +(* if b then (prerr_endline ("keeping " ^ (CicPp.ppterm t)); b) *) + if b then b else let ty' = unfold context ty in let consts' = MetadataConstraints.constants_of ty' in let b = MetadataConstraints.UriManagerSet.subset consts' signature in +(* if not b then prerr_endline ("filtering " ^ (CicPp.ppterm t)) - else prerr_endline ("keeping " ^ (CicPp.ppterm t)); b + else prerr_endline ("keeping " ^ (CicPp.ppterm t)); +*) + b with | CicTypeChecker.TypeCheckerFailure _ -> assert false | ProofEngineTypes.Fail _ -> false (* unfold may fail *) -- 2.39.2