Fixed a problem of lifting.

[helm.git] / helm / software / components / ng_refiner / nCicUnification.ml

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index c6f4f6d9139cf1146f465791457cc800090c5712..838fad9dedfb4288d2d4dac99326da6f693bd1d5 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -249,12 +249,17 @@ and unify hdb test_eq_only metasenv subst context t1 t2 =
  (*D*) inside 'U'; try let rc =
    let fo_unif test_eq_only metasenv subst t1 t2 =
     (*D*) inside 'F'; try let rc =  
-     pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ 
-         NCicPp.ppterm ~metasenv ~subst ~context t2));
+     pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^ 
+         NCicPp.ppterm ~metasenv ~subst ~context t2 ^ "\n" ^ NCicPp.ppmetasenv
+         ~subst metasenv));
      if t1 === t2 then
        metasenv, subst
      else
        match (t1,t2) with
+       | C.Appl [_], _ | _, C.Appl [_] | C.Appl [], _ | _, C.Appl [] 
+       | C.Appl (C.Appl _::_), _ | _, C.Appl (C.Appl _::_) -> 
+           prerr_endline "Appl [Appl _;_] or Appl [] or Appl [_] invariant";
+           assert false 
        | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only -> 
            if NCicEnvironment.universe_leq a b then metasenv, subst
            else raise (fail_exc metasenv subst context t1 t2)