X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=520289aa1f39d1f17886314c901991dc8ad4d843;hb=f54d5fd0caa8c15b6f12d7c91b0ee1bfa5a1b16e;hp=783d7e6fc5e624b7dd9d21ebaf9af1c621f95ccd;hpb=37b52567b8aa1bf5807767d94b96594c0e640588;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 783d7e6fc..520289aa1 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -886,8 +886,18 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
         let obj = uri,height,[],[],obj_kind in
         let old_status = status in
         let status = NCicLibrary.add_obj status obj in
-        let status = index_obj_for_auto status obj in
-        let status = index_eq_for_auto status uri in
+        let index_obj =
+         match obj_kind with
+            NCic.Constant (_,_,_,_,(_,`Example,_))
+          | NCic.Fixpoint (_,_,(_,`Example,_)) -> false
+          | _ -> true
+        in
+        let status =
+         if index_obj then
+          let status = index_obj_for_auto status obj in
+           index_eq_for_auto status uri
+         else
+          status in
 (*
 	  try 
 	    index_eq uri status