Added universes handling. The PRE_UNIVERSES tag may help ;)

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

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index e5656b9b3f9aaa80e9e68c2b1169cad747ff7958..180091c0a871053bcd49c1b997f6ab2bb36421b0 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -94,15 +94,27 @@ let compare_goal_list proof goal1 goal2 =
   let _,metasenv,_,_ = proof in
   let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
   let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
-  let ty_sort1 = CicTypeChecker.type_of_aux' metasenv ey1 ty1 in
-  let ty_sort2 = CicTypeChecker.type_of_aux' metasenv ey2 ty2 in
+  let ty_sort1,_ = 
+    CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.empty_ugraph 
+  in
+  let ty_sort2,_ = 
+    CicTypeChecker.type_of_aux' metasenv ey2 ty2 CicUniv.empty_ugraph 
+  in
   let prop1 =
-    if CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1 then 0
-    else 1
+    let b,_ = 
+      CicReduction.are_convertible 
+       ey1 (Cic.Sort Cic.Prop) ty_sort1 CicUniv.empty_ugraph 
+    in
+      if b then 0
+      else 1
   in
   let prop2 =
-    if CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2 then 0
-    else 1
+    let b,_ = 
+      CicReduction.are_convertible 
+       ey2 (Cic.Sort Cic.Prop) ty_sort2 CicUniv.empty_ugraph 
+    in 
+      if b then 0
+      else 1
   in
   prop1 - prop2