X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FmetadataQuery.ml;h=2941a806e3193025436a4d23393cd3ce8e9ff8ef;hb=ac31c84bb9bcf327554976d4296d787853fc8db5;hp=2cfd95e9a96ed0cc71392f2bb36e64e42d68ee3e;hpb=61a2faa2694907757dd617175e0144705e79d65a;p=helm.git

diff --git a/helm/software/components/tactics/metadataQuery.ml b/helm/software/components/tactics/metadataQuery.ml
index 2cfd95e9a..2941a806e 100644
--- a/helm/software/components/tactics/metadataQuery.ml
+++ b/helm/software/components/tactics/metadataQuery.ml
@@ -109,7 +109,7 @@ let filter_uris_backward ~dbd ~facts signature uris =
     intersect uris siguris 
 
 let compare_goal_list proof goal1 goal2 =
-  let _,metasenv,_,_, _ = proof in
+  let _,metasenv, _subst, _,_, _ = proof in
   let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
   let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
   let ty_sort1,_ = 
@@ -194,8 +194,8 @@ let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose
 let cmatch' = Constr.cmatch'
 
 (* used only by te old auto *)
-let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
- let (_, metasenv, _, _, _) = proof in
+let signature_of_goal ~(dbd:HSql.dbd) ((proof, goal) as _status) =
+ let (_, metasenv, _subst, _, _, _) = proof in
  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
  let main, sig_constants = Constr.signature_of ty in
  let set = signature_of_hypothesis context metasenv in
@@ -275,7 +275,7 @@ let signature_of metasenv goal =
     close_with_types set metasenv context
 
 
-let universe_of_goal ~(dbd:HMysql.dbd) apply_only metasenv goal =
+let universe_of_goal ~(dbd:HSql.dbd) apply_only metasenv goal =
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
   let ty_set = Constr.constants_of ty in
   let hyp_set = signature_of_hypothesis context metasenv in
@@ -288,20 +288,20 @@ let universe_of_goal ~(dbd:HMysql.dbd) apply_only metasenv goal =
   let uris =
     Constr.UriManagerSet.fold
       (fun u acc -> 
-         prerr_endline ("processing "^(UriManager.string_of_uri u));
+         debug_print (lazy ("processing "^(UriManager.string_of_uri u)));
          let set_for_sigmatch = 
 	   Constr.UriManagerSet.remove u all_constants_closed in
 	 if LibraryObjects.is_eq_URI (UriManager.strip_xpointer u) then
 	   (* equality has a special treatment *)
-           (prerr_endline "special treatment";
+           (debug_print (lazy "special treatment");
 	   let tfe =
 	     Constr.SetSet.elements (types_for_equality metasenv goal) 
 	   in
 	     List.fold_left 
 	       (fun acc l ->
 		  let tyl = Constr.UriManagerSet.elements l in
-                  prerr_endline ("tyl: "^(String.concat "\n" 
-			(List.map UriManager.string_of_uri tyl)));
+                  debug_print (lazy ("tyl: "^(String.concat "\n" 
+			(List.map UriManager.string_of_uri tyl))));
 		  let set_for_sigmatch =
 		    Constr.UriManagerSet.diff set_for_sigmatch l in
 		  let uris =
@@ -310,7 +310,7 @@ let universe_of_goal ~(dbd:HMysql.dbd) apply_only metasenv goal =
 		    acc @ uris) 
 	       acc tfe)
 	 else
-           (prerr_endline "normal treatment";
+           (debug_print (lazy "normal treatment");
            let uris =
              sigmatch ~dbd ~facts:false ~where:`Statement 
                (Some (u,[]),set_for_sigmatch)
@@ -334,7 +334,7 @@ let filter_out_predicate set ctx menv =
   Constr.UriManagerSet.filter (fun u -> not (is_predicate u)) set  
 ;;
 
-let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
+let equations_for_goal ~(dbd:HSql.dbd) ?signature ((proof, goal) as _status) =
 (*
   let to_string set =
     "{\n" ^
@@ -344,7 +344,7 @@ let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
     ^ "\n}"
   in
 *)
- let (_, metasenv, _, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
  let main, sig_constants = 
    match signature with 
@@ -393,8 +393,8 @@ let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
    (*        else raise Goal_is_not_an_equation *)
 
 let experimental_hint 
-  ~(dbd:HMysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
-  let (_, metasenv, _, _, _) = proof in
+  ~(dbd:HSql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
+  let (_, metasenv, _subst, _, _, _) = proof in
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
   let (uris, (main, sig_constants)) =
     match signature with
@@ -475,10 +475,10 @@ let experimental_hint
     (aux uris)
 
 let new_experimental_hint 
-  ~(dbd:HMysql.dbd) ?(facts=false) ?signature ~universe
+  ~(dbd:HSql.dbd) ?(facts=false) ?signature ~universe
   ((proof, goal) as status)
 =
-  let (_, metasenv, _, _, _) = proof in
+  let (_, metasenv,  _subst, _, _, _) = proof in
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
   let (uris, (main, sig_constants)) =
     match signature with