Much simpler (and slightly more performant) implementation of the UriManager.

[helm.git] / helm / ocaml / tactics / autoTactic.ml

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index c2407ee73b3625997a21b76cb212296810ef9de7..13dac415f8298af2bc7b4f4ba486008eb72f68fb 100644 (file)
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -27,6 +27,11 @@
 
 (* let debug_print = fun _ -> () *)
 
+let experimental_hint =
+ let profile = CicUtil.profile "experimental_hint" in
+ fun ~dbd ~facts ?signature status ->
+  profile (MetadataQuery.experimental_hint ~dbd ~facts ?signature) status
+
 let search_theorems_in_context status =
   let (proof, goal) = status in
   let module C = Cic in
@@ -291,7 +296,7 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
              new_search_theorems 
                (fun status -> 
                   List.map snd
-                  (MetadataQuery.experimental_hint 
+                  (experimental_hint 
                      ~dbd ~facts:facts ?signature:sign status))
                dbd proof goal (depth-1) new_sign in 
            let all_choices =