-let eval_ast ?do_heavy_checks lexicon_status
- grafite_status (text,prefix_len,ast)
-=
- let lexicon_status_ref = ref lexicon_status in
- let baseuri = GrafiteTypes.get_baseuri grafite_status in
- let new_grafite_status,new_objs =
+let eval_ast ?do_heavy_checks status (text,prefix_len,ast) =
+ let dump = not (Helm_registry.get_bool "matita.moo") in
+ let lexicon_status_ref = ref (status :> LexiconEngine.status) in
+ let baseuri = status#baseuri in
+ let new_status,new_objs =
+ match ast with
+ | G.Executable (_, G.Command (_, G.Coercion _)) when dump ->
+(* FG: some commands can not be executed when mmas are parsed *************)
+(* To be removed when mmas will be executed *)
+ status, `Old []
+ | ast ->