X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=e55df286b87b5a0d6f069bb4f7de9228cc3f00e4;hb=62ab884c6ce7dd41c6e6fa2efc5102b23f57de32;hp=89673e7d75dae131b867114380e98b37fec483f6;hpb=d0e97750e19af9286400a3e7b161a1c658684848;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 89673e7d7..e55df286b 100644
--- 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
@@ -770,10 +777,11 @@ let eval_ng_tac tac =
            ) hyps,
           (text,prefix_len,concl))
        ) seqs)
-  | GrafiteAst.NAuto (_loc, (None,a)) -> NAuto.auto_tac ~params:(None,a)
+  | GrafiteAst.NAuto (_loc, (None,a)) -> 
+      NAuto.auto_tac ~params:(None,a) ?trace_ref:None
   | GrafiteAst.NAuto (_loc, (Some l,a)) ->
       NAuto.auto_tac
-	~params:(Some List.map (fun x -> "",0,x) l,a)
+	~params:(Some List.map (fun x -> "",0,x) l,a) ?trace_ref:None
   | GrafiteAst.NBranch _ -> NTactics.branch_tac ~force:false
   | GrafiteAst.NCases (_loc, what, where) ->
       NTactics.cases_tac 
@@ -800,6 +808,7 @@ let eval_ng_tac tac =
       NTactics.generalize_tac ~where:(text,prefix_len,where)
   | GrafiteAst.NId _ -> (fun x -> x)
   | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
+  | GrafiteAst.NIntros (_loc,ns) -> NTactics.intros_tac ns
   | GrafiteAst.NInversion (_loc, what, where) ->
       NTactics.inversion_tac 
         ~what:(text,prefix_len,what)
@@ -926,16 +935,15 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                 in
                 if nstatus#ng_mode <> `CommandMode then
                   begin
-                    HLog.error "error in generating projection/eliminator";
-                    prerr_endline (NCicPp.ppobj nstatus#obj);
-                    nstatus, uris
+                    (*HLog.warn "error in generating projection/eliminator";*)
+                    status, uris
                   end
                 else
                   nstatus, concat_nuris uris nuris
                with
-               | MultiPassDisambiguator.DisambiguationError _ 
+               | MultiPassDisambiguator.DisambiguationError _
                | NCicTypeChecker.TypeCheckerFailure _ ->
-                  HLog.warn "error in generating projection/eliminator";
+                  (*HLog.warn "error in generating projection/eliminator";*)
                   status,uris
              ) (status,`New [] (* uris *)) boxml in             
            let _,_,_,_,nobj = obj in 
@@ -956,7 +964,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                              [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
                            | _ -> status,`New []))
                        (* XXX *)
-                      with _ -> HLog.warn "error in generating inversion principle"; 
+                      with _ -> (*HLog.warn "error in generating inversion principle"; *)
                                 let status = status#set_ng_mode `CommandMode in status)
                   status
                   (NCic.Prop::