X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=0806057ec14ab1d67189dba4832028c6509576db;hb=d43b4cfa41256e90fceb0129b7eadb38207190c3;hp=482a138a6c8f4ce16863c36b5a92b3bfe561deb1;hpb=8b1a49bbee9eea86eb74c040defe701370ca5893;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 482a138a6..0806057ec 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -861,6 +861,27 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
           [] ->
            eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
         | _ -> status,`New [])
+  | GrafiteAst.NInverter (loc, name, indty) ->
+     if status#ng_mode <> `CommandMode then
+      raise (GrafiteTypes.Command_error "Not in command mode")
+     else
+      let status = status#set_ng_mode `ProofMode in
+      let metasenv,subst,status,indty =
+       GrafiteDisambiguate.disambiguate_nterm None status [] [] [] (text,prefix_len,indty) in
+      let _,leftno,tys,_,_ = match indty with
+          NCic.Const r -> NCicEnvironment.get_checked_indtys r
+        | _ -> assert false in
+      let it = match tys with
+          hd::tl -> hd
+        | _ -> assert false
+      in
+     let status,obj =
+      NInversion.mk_inverter name it leftno status status#baseuri in
+     let _,_,menv,_,_ = obj in
+     (match menv with
+        [] ->
+          eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+      | _ -> assert false)
   | GrafiteAst.NUnivConstraint (loc,u1,u2) ->
       eval_add_constraint status [`Type,u1] [`Type,u2]
 ;;