split into two major parts:

[helm.git] / helm / ocaml / cic_unification / cicUnification.ml

diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index 70c7aa9cb17c1511394233117c8f7787c04fad38..3c8b077297fd5ad8da82700f4dd081fade124c19 100644 (file)
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -106,7 +106,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
             type_of_aux' metasenv' subst'' context t
           in
            fo_unif_subst subst'' context metasenv' (S.lift_meta l meta_type) tyt
-        with _ ->
+        with AssertFailure _ ->
           (* TODO huge hack!!!!
            * we keep on unifying/refining in the hope that the problem will be
            * eventually solved. In the meantime we're breaking a big invariant:
@@ -144,7 +144,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
        raise (UnificationFailure (sprintf
         "Can't unify %s with %s due to different inductive constructors"
         (CicPp.ppterm t1) (CicPp.ppterm t1)))
-   | (C.Implicit, _) | (_, C.Implicit) ->  assert false
+   | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
    | (C.Cast (te,ty), t2) -> fo_unif_subst subst context metasenv te t2
    | (t1, C.Cast (te,ty)) -> fo_unif_subst subst context metasenv t1 te
    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->