Do not index examples (concrete syntax: nremark).

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 783d7e6fc5e624b7dd9d21ebaf9af1c621f95ccd..520289aa1f39d1f17886314c901991dc8ad4d843 100644 (file)
--- 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