From f54d5fd0caa8c15b6f12d7c91b0ee1bfa5a1b16e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 18 Mar 2010 10:21:46 +0000 Subject: [PATCH] Do not index examples (concrete syntax: nremark). --- .../components/grafite_engine/grafiteEngine.ml | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) 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 -- 2.39.2