Refining with no expected type + unification seems to be faster.

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 07d08345c3a7f0f10dc0469466bf0ff2e198baf4..e00bb2ade0d99768c11fe7330500d2487323a86a 100644 (file)
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -116,19 +116,27 @@ let fast_eq_check_all status eq_cache goal =
   let gname, ctx, gty = List.assoc goal metasenv in
   let gty = NCicUntrusted.apply_subst subst ctx gty in
   let build_status (pt, _, metasenv, subst) =
-    (* let stamp = Unix.gettimeofday () in *)
-    let metasenv, subst, pt, pty = 
+    let stamp = Unix.gettimeofday () in 
+    let metasenv, subst, pt, pty =
       NCicRefiner.typeof 
                (status#set_coerc_db NCicCoercion.empty_db) 
-       metasenv subst ctx pt (Some gty)
-    in
-(* print (lazy (Printf.sprintf "Refined in %fs"
-                    (Unix.gettimeofday() -. stamp))); *)
+       metasenv subst ctx pt None in
+    let metasenv, subst =
+       NCicUnification.unify status metasenv subst ctx gty pty 
+(* the previous code is much less expensive than directly refining
+   pt with expected type pty 
+    in 
+      NCicRefiner.typeof 
+               (status#set_coerc_db NCicCoercion.empty_db) 
+       metasenv subst ctx pt (Some gty) *)
+    in 
+      print (lazy (Printf.sprintf "Refined in %fs"
+                    (Unix.gettimeofday() -. stamp))); 
       let status = status#set_obj (n,h,metasenv,subst,o) in
       let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in
       let subst = (goal,(gname,ctx,pt,pty)) :: subst in
        status#set_obj (n,h,metasenv,subst,o)
-  in
+    in
     List.map build_status
       (NCicParamod.fast_eq_check status metasenv subst ctx 
         eq_cache (NCic.Rel ~-1,gty))