From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 18 Mar 2010 10:21:46 +0000 (+0000)
Subject: Do not index examples (concrete syntax: nremark).
X-Git-Tag: make_still_working~2996
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f54d5fd0caa8c15b6f12d7c91b0ee1bfa5a1b16e;p=helm.git

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 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