ocaml 3.09 transition

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

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index 2235670a06e7a2814c8a4bfbba979cca5381ded8..de356a3d1f52860237a9582bb57b0ddc991e271f 100644 (file)
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -125,11 +125,7 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st
   (* List.iter 
     (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) uris; *)
   (* delete all .var uris *)
-  let isvar (_,s) =
-    let len = String.length s in
-    let suffix = String.sub s (len-4) 4 in
-      not (suffix  = ".var") in
-  let uris = List.filter isvar uris in 
+  let uris = List.filter UriManager.is_var uris in 
   (* delete all not "cic:/Coq" uris *)
   (*
   let uris =
@@ -238,21 +234,24 @@ let  searchTheorems mqi_handle (proof,goal) =
 (*
    prerr_endline "PRIMA DELLA PRIMA TYPE OF " ;
 *)
-   let ty_sort1 = CicTypeChecker.type_of_aux' metasenv ey1 ty1 in
+   let ty_sort1,u = (*TASSI: FIXME *)
+     CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.empty_ugraph in
 (*
    prerr_endline (Printf.sprintf "PRIMA DELLA SECONDA TYPE OF %s \n### %s @@@%s " (CicMetaSubst.ppmetasenv metasenv []) (CicMetaSubst.ppcontext [] ey2) (CicMetaSubst.ppterm [] ty2));
 *)
-   let ty_sort2 = CicTypeChecker.type_of_aux' metasenv ey2 ty2 in
+   let ty_sort2,u1 = CicTypeChecker.type_of_aux' metasenv ey2 ty2 u in
 (*
    prerr_endline "DOPO LA SECONDA TYPE OF " ;
 *)
-   let prop1 = if CicReduction.are_convertible 
-                  ey1 (Cic.Sort Cic.Prop) ty_sort1 then 0
-                else 1 in
-   let prop2 = if CicReduction.are_convertible 
-                  ey2 (Cic.Sort Cic.Prop) ty_sort2 then 0
-                else 1 in
- prop1 - prop2 in
- List.map (fun (level,(proof,goallist)) -> (proof, (List.stable_sort (order_goal_list proof) goallist))) res  
+   let b,u2 = 
+     CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1 u1 in
+   let prop1 = if b then 0 else 1 in
+   let b,_ = CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2 u2 in
+   let prop2 = if b then 0 else 1 in
+     prop1 - prop2 in
+   List.map (
+     fun (level,(proof,goallist)) -> 
+       (proof, (List.stable_sort (order_goal_list proof) goallist))
+   ) res  
 ;;