X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=838fad9dedfb4288d2d4dac99326da6f693bd1d5;hb=5338da4d7047b18aacd43447a3261b531895291d;hp=c6f4f6d9139cf1146f465791457cc800090c5712;hpb=c63c1b75e1afd0307c932e43375963aea1ec6c0b;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index c6f4f6d91..838fad9de 100644
--- 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)