new instantiate, only known bug is w.r.t. in/out scope and file matita/contribs/ng_as...

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index fa4b952535761e0341da4a552d014c627c6475da..fd8d776c180749023a85e4c87a4d266113482aa0 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -868,11 +868,18 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
             List.fold_left
              (fun (status,uris) boxml ->
                try
-                let status,nuris =
+                let nstatus,nuris =
                  eval_ncommand opts status
                   ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml))
                 in
-                status, concat_nuris uris nuris
+                if nstatus#ng_mode <> `CommandMode then
+                  begin
+                    HLog.error "error in generating projection/eliminator";
+                    prerr_endline (NCicPp.ppobj nstatus#obj);
+                    nstatus, uris
+                  end
+                else
+                  nstatus, concat_nuris uris nuris
                with
                | MultiPassDisambiguator.DisambiguationError _ 
                | NCicTypeChecker.TypeCheckerFailure _ ->