]> matita.cs.unibo.it Git - helm.git/commitdiff
add XXX where I found a catch all statement
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 21 Oct 2009 09:11:23 +0000 (09:11 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 21 Oct 2009 09:11:23 +0000 (09:11 +0000)
helm/software/components/grafite_engine/grafiteEngine.ml

index aea900cdf6fac1027f76fa6554f2ee0bd218844b..fa4b952535761e0341da4a552d014c627c6475da 100644 (file)
@@ -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