From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 6 May 2010 22:35:02 +0000 (+0000)
Subject: Bug fixed: nstatus => status (to undo the changes).
X-Git-Tag: make_still_working~2908
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=102cb2ba885b9fa93c824c7c07ba2467cfec0e16;p=helm.git

Bug fixed: nstatus => status (to undo the changes).

Worring warnings commented out.
---

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::