main constants set is closed with constants types

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 3bc3c566e778ba9a591bc3042c7f3f5a8abbcd4c..5afd37a9aafe6cb2620412f8d8f19d597f453acd 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -236,6 +236,16 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
     The cose is a cut and paste of the previous one: at the end 
     of the experimentation we shall make a choice. *)
 
+let close_with_types s metasenv context =
+  Constr.StringSet.fold 
+    (fun e bag -> 
+      let t = CicUtil.term_of_uri e in
+      let ty, _ = 
+        CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph  
+      in
+      Constr.StringSet.union bag (Constr.constants_of ty)) 
+    s s
+
 let experimental_hint 
   ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
   let (_, metasenv, _, _) = proof in
@@ -256,11 +266,32 @@ let experimental_hint
         List.fold_right Constr.StringSet.add (main :: types)
           Constr.StringSet.empty
   in
-  let hyp_constants =
-    Constr.StringSet.diff (signature_of_hypothesis context) types_constants
+  let all_constants =
+    let hyp_and_sug =
+      Constr.StringSet.union
+        (signature_of_hypothesis context) 
+        sig_constants
+    in
+    let main = 
+      match main with
+      | None -> Constr.StringSet.empty
+      | Some (main,_) -> 
+          let ty, _ = 
+            CicTypeChecker.type_of_aux' 
+              metasenv context (CicUtil.term_of_uri main) CicUniv.empty_ugraph
+          in
+          Constr.constants_of ty
+    in
+    Constr.StringSet.union main hyp_and_sug
   in
-(* Constr.StringSet.iter prerr_endline hyp_constants; *)
-  let other_constants = Constr.StringSet.union sig_constants hyp_constants in
+  let all_constants_closed = close_with_types all_constants metasenv context in
+  let other_constants = 
+    Constr.StringSet.diff all_constants_closed types_constants
+  in
+  prerr_endline "all_constants_closed";
+  Constr.StringSet.iter prerr_endline all_constants_closed;
+  prerr_endline "other_constants";
+  Constr.StringSet.iter prerr_endline other_constants;
   let uris = 
     let pow = 2 ** (Constr.StringSet.cardinal other_constants) in
     if ((List.length uris < pow) or (pow <= 0))