CicUniv.UniverseInconsistency is no handled correcly.

[helm.git] / helm / software / components / cic_unification / cicUnification.ml

diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml
index 6004e73fa98e71497447e5d72357683907ea88c0..c9981bb1114ead6d8b5fd8262162a1066a4f94db 100644 (file)
--- a/helm/software/components/cic_unification/cicUnification.ml
+++ b/helm/software/components/cic_unification/cicUnification.ml
@@ -74,7 +74,11 @@ in profiler_toa.HExtlib.profile foo ()
 ;;
 
 let exists_a_meta l = 
-  List.exists (function Cic.Meta _ -> true | _ -> false) l
+  List.exists 
+    (function 
+       | Cic.Meta _  
+       | Cic.Appl (Cic.Meta _::_) -> true
+       | _ -> false) l
 
 let rec deref subst t =
   let snd (_,a,_) = a in
@@ -427,10 +431,14 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                C.Sort (C.Type u) when not test_equality_only ->
                  let u' = CicUniv.fresh () in
                  let s = C.Sort (C.Type u') in
-                 let ugraph2 =   
-                   CicUniv.add_ge (upper u u') (lower u u') ugraph1
-                 in
-                   s,ugraph2
+                  (try
+                    let ugraph2 =   
+                     CicUniv.add_ge (upper u u') (lower u u') ugraph1
+                    in
+                     s,ugraph2
+                   with
+                    CicUniv.UniverseInconsistency msg ->
+                     raise (UnificationFailure msg))
              | _ -> t',ugraph1
          in
          (* Unifying the types may have already instantiated n. Let's check *)
@@ -655,7 +663,9 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
                           C.Appl (C.MutInd _::_) -> 
                             fo_unif_subst test_equality_only 
                               subst context metasenv t1 t2' ugraph         
-                        | _ -> raise (UnificationFailure (lazy "99")))
+                        | _ -> raise 
+                           (UnificationFailure 
+                              (lazy ("not a mutind :"^CicMetaSubst.ppterm subst t2 ))))
                   | _ -> raise exn)))
    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
        let subst', metasenv',ugraph1 =