More debug_print made lazy.

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

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 9355dfc10d20f1c1e4dca37c4754c1bbbacf68ca..e86f79af5f38d4dccedad03d601a9ac253a46534 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -123,14 +123,16 @@ let intersect uris siguris =
   let inter = Constr.UriManagerSet.inter set1 set2 in
   List.filter (fun s -> Constr.UriManagerSet.mem s inter) uris
 
+(* Profiling code
 let at_most =
  let profiler = CicUtil.profile "at_most" in
- fun ~dbd ~where uri -> profiler (Constr.at_most ~dbd ~where) uri
+ fun ~dbd ~where uri -> profiler.profile (Constr.at_most ~dbd ~where) uri
 
 let sigmatch =
  let profiler = CicUtil.profile "sigmatch" in
  fun ~dbd ~facts ~where signature ->
-  profiler (MetadataConstraints.sigmatch ~dbd ~facts ~where) signature
+  profiler.profile (MetadataConstraints.sigmatch ~dbd ~facts ~where) signature
+*) let at_most = Constr.at_most  let sigmatch = MetadataConstraints.sigmatch
 
 let filter_uris_forward ~dbd (main, constants) uris =
   let main_uris =
@@ -219,17 +221,19 @@ let close_with_constructors s metasenv context =
        | _ -> bag)
     s s
 
+(* Profiling code
 let apply_tac_verbose =
  let profiler = CicUtil.profile "apply_tac_verbose" in
-  fun ~term status -> profiler (PrimitiveTactics.apply_tac_verbose ~term) status
+  fun ~term status -> profiler.profile (PrimitiveTactics.apply_tac_verbose ~term) status
 
 let sigmatch =
  let profiler = CicUtil.profile "sigmatch" in
- fun ~dbd ~facts ?(where=`Conclusion) signature -> profiler (Constr.sigmatch ~dbd ~facts ~where) signature
+ fun ~dbd ~facts ?(where=`Conclusion) signature -> profiler.profile (Constr.sigmatch ~dbd ~facts ~where) signature
 
 let cmatch' =
  let profiler = CicUtil.profile "cmatch'" in
- fun ~dbd ~facts signature -> profiler (Constr.cmatch' ~dbd ~facts) signature
+ fun ~dbd ~facts signature -> profiler.profile (Constr.cmatch' ~dbd ~facts) signature
+*) let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose let cmatch' = Constr.cmatch'
 
 let signature_of_goal ~(dbd:Mysql.dbd) ((proof, goal) as status) =
  let (_, metasenv, _, _) = proof in
@@ -415,7 +419,7 @@ let fill_with_dummy_constants t =
     function
        Cic.Lambda (n,s,t) -> 
          let dummy_uri = 
-           UriManager.uri_of_string ("cic:/dummy_"^(string_of_int i)) in
+           UriManager.uri_of_string ("cic:/dummy_"^(string_of_int i)^".con") in
            (aux (i+1) (s::types)
               (CicSubstitution.subst (Cic.Const(dummy_uri,[])) t))
       | t -> t,types
@@ -444,7 +448,7 @@ let instance ~dbd t =
       when (String.sub (UriManager.string_of_uri s) 0 10 = "cic:/dummy") -> 
       let s = UriManager.string_of_uri s in
       let len = String.length s in
-            let dummy_index = int_of_string (String.sub s 11 (len-11)) in
+            let dummy_index = int_of_string (String.sub s 11 (len-15)) in
       let dummy_type = List.nth types dummy_index in
       Some (d,dummy_type)
     | _::l -> look_for_dummy_main l