From 102cb2ba885b9fa93c824c7c07ba2467cfec0e16 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 6 May 2010 22:35:02 +0000 Subject: [PATCH] Bug fixed: nstatus => status (to undo the changes). Worring warnings commented out. --- .../components/grafite_engine/grafiteEngine.ml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index fe2da884d..c44b70178 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -933,16 +933,15 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = in if nstatus#ng_mode <> `CommandMode then begin - HLog.error "error in generating projection/eliminator"; - prerr_endline (NCicPp.ppobj nstatus#obj); - nstatus, uris + (*HLog.warn "error in generating projection/eliminator";*) + status, uris end else nstatus, concat_nuris uris nuris with - | MultiPassDisambiguator.DisambiguationError _ + | MultiPassDisambiguator.DisambiguationError _ | NCicTypeChecker.TypeCheckerFailure _ -> - HLog.warn "error in generating projection/eliminator"; + (*HLog.warn "error in generating projection/eliminator";*) status,uris ) (status,`New [] (* uris *)) boxml in let _,_,_,_,nobj = obj in @@ -963,7 +962,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) | _ -> status,`New [])) (* XXX *) - with _ -> HLog.warn "error in generating inversion principle"; + with _ -> (*HLog.warn "error in generating inversion principle"; *) let status = status#set_ng_mode `CommandMode in status) status (NCic.Prop:: -- 2.39.2