snapshot (first version in which some extensions work, e.g. infix +)

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

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index d91bec9743aea312a14afda79f891e1744f7a655..fc5328e9ffa3c252267d44b77e2d1b21614a02ac 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -194,7 +194,7 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
     let pow = 2 ** (Constr.StringSet.cardinal other_constants) in
     if ((List.length uris < pow) or (pow <= 0))
     then begin
-      prerr_endline "MetadataQuery: large sig, falling back to old method";
+(*       prerr_endline "MetadataQuery: large sig, falling back to old method"; *)
       filter_uris_forward ~dbd (main, other_constants) uris
     end else
       filter_uris_backward ~dbd ~facts (main, other_constants) uris
@@ -250,17 +250,6 @@ let experimental_hint
   ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
   let (_, metasenv, _, _) = proof in
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
-  let uris = 
-    if facts then
-      ["cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"]
-    else
-      ["cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
-       (* "cic:/Coq/Init/Logic/trans_eq.con"; *)
-       "cic:/Coq/Init/Logic/f_equal.con";
-       "cic:/Coq/Init/Logic/f_equal2.con";
-       "cic:/Coq/Init/Logic/f_equal3.con"] 
-  in
-  (* 
   let (uris, (main, sig_constants)) =
     match signature with
     | Some signature -> 
@@ -312,7 +301,7 @@ let experimental_hint
       filter_uris_forward ~dbd (main, other_constants) uris
     end else
       filter_uris_backward ~dbd ~facts (main, other_constants) uris
-  in *)
+  in 
   let rec aux = function
     | [] -> []
     | uri :: tl ->
@@ -366,11 +355,11 @@ let fill_with_dummy_constants t =
 let instance ~dbd t =
   let t',types = fill_with_dummy_constants t in 
   let metadata = MetadataExtractor.compute ~body:None ~ty:t' in
-  List.iter 
+(*   List.iter 
     (fun x -> 
        prerr_endline 
-        (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x))) 
-    metadata;
+         (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x))) 
+    metadata; *)
   let no_concl = MetadataDb.count_distinct `Conclusion metadata in
   let no_hyp = MetadataDb.count_distinct `Hypothesis metadata in
   let no_full = MetadataDb.count_distinct `Statement metadata in
@@ -390,7 +379,7 @@ let instance ~dbd t =
   in
   match (look_for_dummy_main metadata) with
     | None->
-        prerr_endline "Caso None";
+(*         prerr_endline "Caso None"; *)
         (* no dummy in main position *)
         let metadata = List.filter is_dummy metadata in
         let constraints = List.map MetadataTypes.constr_of_metadata metadata in
@@ -399,8 +388,8 @@ let instance ~dbd t =
         let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in
           Constr.at_least ~dbd ?concl_card ?full_card ?diff constraints
     | Some (depth, dummy_type) ->
-        prerr_endline 
-          (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type));
+(*         prerr_endline 
+          (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type)); *)
         (* a dummy in main position *)
         let metadata_for_dummy_type = 
           MetadataExtractor.compute ~body:None ~ty:dummy_type in