...

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 89673e7d75dae131b867114380e98b37fec483f6..fe2da884d4c1f02c2c808e97b2c40fe9fa522a88 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -530,9 +530,16 @@ let record_index_obj =
    end
 ;;
 
-let compute_keys uri height kind = 
- let mk_item orig_ty spec =
-  let keys = NnAuto.keys_of_cic_term [] [] [] orig_ty in
+let compute_keys status uri height kind = 
+ let mk_item ty spec =
+   let orig_ty = NTacStatus.mk_cic_term [] ty in
+   let status,keys = NnAuto.keys_of_type status orig_ty in
+   let keys =  
+     List.map 
+       (fun t -> 
+         snd (NTacStatus.term_of_cic_term status t (NTacStatus.ctx_of t)))
+       keys
+   in
    keys,NCic.Const(NReference.reference_of_spec uri spec)
  in
  let data = 
@@ -578,12 +585,12 @@ let compute_keys uri height kind =
           NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t);
         None
       end)
-   data
+    data
 ;;
 
 let index_obj_for_auto status (uri, height, _, _, kind) = 
  (*prerr_endline (string_of_int height);*)
-  let data = compute_keys uri height kind in
+  let data = compute_keys status uri height kind in
   let status = basic_index_obj data status in
   let dump = record_index_obj data :: status#dump in   
   status#set_dump dump