From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 21 Oct 2009 09:11:23 +0000 (+0000)
Subject: add XXX where I found a catch all statement
X-Git-Tag: make_still_working~3273
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f01e9ac75628cf750ce212ff32f2b2a1d507eb6f;hp=acc309665418f646857b8c246ef037d71fdea705;p=helm.git

add XXX where I found a catch all statement
---

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index aea900cdf..fa4b95253 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -894,6 +894,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                        fst (match menv with
                              [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
                            | _ -> status,`New []))
+                       (* XXX *)
                       with _ -> HLog.warn "error in generating inversion principle"; 
                                 let status = status#set_ng_mode `CommandMode in status)
                   status