Let's refresh the universe to avoid assert failure.

However, the effect of this is still unclear to me.

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index ed650a3c326cd5dedc0ff605f877a638a024453c..325cd3e5f1e5520365a8bcb90712cd4f84e8c8a2 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -104,13 +104,12 @@ let ppmetasenv ~subst:_subst _metasenv = "...";;
 
 let pp _ = ();;
 
-let fix_sorts swap metasenv subst context meta t =
+let fix_sorts swap exc t =
   let rec aux () = function
     | NCic.Sort (NCic.Type u) as orig ->
         if swap then
          match NCicEnvironment.sup u with
-         | None -> prerr_endline "no sup for" ;
-            raise (fail_exc metasenv subst context meta t)
+         | None -> prerr_endline "no sup for" ; raise exc
          | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)
         else
          NCic.Sort (NCic.Type (
@@ -192,12 +191,13 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
          "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\nctx:\n"^
           ppcontext ~metasenv ~subst context ^ "\nmenv:\n"^
           ppmetasenv ~subst metasenv));
+       let exc_to_be = fail_exc metasenv subst context (NCic.Meta (n,lc)) t in
        let t, ty_t = 
          try t, NCicTypeChecker.typeof ~subst ~metasenv context t 
          with 
          | NCicTypeChecker.AssertFailure msg -> 
            (pp (lazy "fine typeof (fallimento)");
-           let ft=fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t in
+           let ft = fix_sorts swap exc_to_be t in
            if ft == t then 
              (prerr_endline ( ("ILLTYPED: " ^ 
                 NCicPp.ppterm ~metasenv ~subst ~context t
@@ -217,6 +217,7 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap =
               prerr_endline (Lazy.force msg);
               pp msg; assert false
        in
+       let ty_t = fix_sorts swap exc_to_be ty_t in 
        let lty = NCicSubstitution.subst_meta lc ty in
        match ty_t with
        | NCic.Implicit _ -> 
@@ -352,7 +353,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
                     (C.Meta (i,l)) lambda_Mj,
                    i
               | NCic.Meta (i,_) -> (metasenv, subst), i
-              | _ -> assert false
+              | _ -> prerr_endline ("XXX: " ^ NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.whd ~subst context t1)); assert false
              in
               let t1 = NCicReduction.whd ~subst context t1 in
               let j, lj =