From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Thu, 23 Feb 2012 09:48:07 +0000 (+0000)
Subject: refiner porting from matita 1.
X-Git-Tag: make_still_working~1942
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=1410ea677188e9e11d748c69e208d1e90b0a324e

refiner porting from matita 1.
---

diff --git a/matitaB/components/ng_refiner/nCicRefiner.ml b/matitaB/components/ng_refiner/nCicRefiner.ml
index 8deb72797..7cdeb875e 100644
--- a/matitaB/components/ng_refiner/nCicRefiner.ml
+++ b/matitaB/components/ng_refiner/nCicRefiner.ml
@@ -70,7 +70,7 @@ let exp_implicit status ~localise metasenv subst context with_type t =
               ~unify:(fun m s c t1 t2 ->
                 try Some (NCicUnification.unify status m s c t1 t2)
                 with NCicUnification.UnificationFailure _ | NCicUnification.Uncertain _ -> None)
-              metasenv subst context 0 (0,NCic.Irl 0) typ
+              metasenv subst context ~-1 (0,NCic.Irl 0) typ
             with
               NCicMetaSubst.MetaSubstFailure _
             | NCicMetaSubst.Uncertain _ ->
@@ -139,6 +139,32 @@ let check_allowed_sort_elimination status localise r orig =
     aux
 ;;
 
+(* CSC: temporary thing, waiting for better times *)
+let mk_fresh_name context name =
+try
+ let rex = Str.regexp "[0-9']*$" in
+ let rex2 = Str.regexp "'*$" in
+ let basename = Str.global_replace rex "" in
+ let suffix name =
+  ignore (Str.search_forward rex name 0);
+  let n = Str.matched_string name in
+  let n = Str.global_replace rex2 "" n in
+   if n = "" then 0 else int_of_string n
+in
+ let name' = basename name in
+ let name' = if name' = "_" then "H" else name' in
+ let last =
+  List.fold_left
+   (fun last (name,_) ->
+     if basename name = name' then
+      max last (suffix name)
+     else
+      last
+   ) (-1) context
+ in
+  name' ^ (if last = -1 then "" else string_of_int (last + 1))
+with exn -> prerr_endline ("XXX" ^ Printexc.to_string exn); assert false
+
 let rec typeof (status:#NCicCoercion.status)
   ?(localise=fun _ -> Stdpp.dummy_loc) 
   metasenv subst context term expty 
@@ -166,7 +192,7 @@ let rec typeof (status:#NCicCoercion.status)
            | NCicUnification.Uncertain _ 
            | NCicUnification.UnificationFailure _ as exc -> 
              try_coercions status ~localise 
-               metasenv subst context t orig infty expty true exc)
+               metasenv subst context t orig infty (`Type expty) exc)
     | None -> metasenv, subst, t, infty
     (*D*)in outside true; rc with exc -> outside false; raise exc
   in
@@ -464,14 +490,17 @@ and check_type status ~localise metasenv subst context (ty as orig_ty) =
 
 and try_coercions status 
   ~localise 
-  metasenv subst context t orig_t infty expty perform_unification exc 
+  metasenv subst context t orig_t infty expty exc 
 =
   let cs_subst = NCicSubstitution.subst status ~avoid_beta_redexes:true in
   try 
-    pp (lazy "WWW: trying coercions -- preliminary unification");
-    let metasenv, subst = 
-      NCicUnification.unify status metasenv subst context infty expty
-    in metasenv, subst, t, expty
+   (match expty with
+       `Type expty ->
+         pp (lazy "WWW: trying coercions -- preliminary unification");
+         let metasenv, subst = 
+           NCicUnification.unify status metasenv subst context infty expty
+         in metasenv, subst, t, expty
+     | _ -> raise (Failure "Special case Prod or Sort"))
   with
   | exn ->
   (* we try with a coercion *)
@@ -482,7 +511,7 @@ and try_coercions status
         "The term\n%s\nhas type\n%s\nbut is here used with type\n%s"
         (status#ppterm ~metasenv ~subst ~context t)
         (status#ppterm ~metasenv ~subst ~context infty)
-        (status#ppterm ~metasenv ~subst ~context expty))) exc)
+        expty)) exc)
   | (_,metasenv, newterm, newtype, meta)::tl ->
       try 
           pp (lazy("K=" ^ status#ppterm ~metasenv ~subst ~context newterm));
@@ -494,21 +523,28 @@ and try_coercions status
             status#ppterm ~metasenv ~subst ~context t ^  " === " ^
             status#ppterm ~metasenv ~subst ~context meta ^ "\n"));
         let metasenv, subst = 
-          NCicUnification.unify status metasenv subst context t meta
-        in
-          pp (lazy ( "UNIFICATION in CTX:\n"^ 
-            status#ppcontext ~metasenv ~subst context
-            ^ "\nMENV: " ^
-            status#ppmetasenv metasenv ~subst
-            ^ "\nOF: " ^
-            status#ppterm ~metasenv ~subst ~context newtype ^  " === " ^
-            status#ppterm ~metasenv ~subst ~context expty ^ "\n"));
-        let metasenv, subst = 
-          if perform_unification then
-            NCicUnification.unify status metasenv subst context newtype expty
-          else metasenv, subst
-        in
-        metasenv, subst, newterm, newtype
+          NCicUnification.unify status metasenv subst context t meta in
+        match expty with
+           `Type expty ->
+             pp (lazy ( "UNIFICATION in CTX:\n"^ 
+               status#ppcontext ~metasenv ~subst context
+               ^ "\nMENV: " ^
+               status#ppmetasenv metasenv ~subst
+               ^ "\nOF: " ^
+               status#ppterm ~metasenv ~subst ~context newtype ^  " === " ^
+               status#ppterm ~metasenv ~subst ~context expty ^ "\n"));
+             let metasenv,subst =
+               NCicUnification.unify status metasenv subst context newtype expty
+             in
+              metasenv, subst, newterm, newtype
+         | `Sort ->
+             (match NCicReduction.whd status ~subst context newtype with
+                 NCic.Sort _ -> metasenv,subst,newterm,newtype
+               | _ -> first exc tl)
+         | `Prod ->
+             (match NCicReduction.whd status ~subst context newtype with
+                 NCic.Prod _ -> metasenv,subst,newterm,newtype
+               | _ -> first exc tl)
       with 
       | NCicUnification.UnificationFailure _ -> first exc tl
       | NCicUnification.Uncertain _ as exc -> first exc tl
@@ -517,7 +553,8 @@ and try_coercions status
   try 
     pp (lazy "WWW: trying coercions -- inner check");
     match infty, expty, t with
-    | _,_, NCic.Match (Ref.Ref (_,Ref.Ind (_,tyno,leftno)) as r,outty,m,pl) ->
+    (* `Sort|`Prod + Match not implemented *) 
+    | _,`Type expty, NCic.Match (Ref.Ref (_,Ref.Ind (_,tyno,leftno)) as r,outty,m,pl) ->
         (*{{{*) pp (lazy "CASE");
         (* {{{ helper functions *)
         let get_cl_and_left_p refit outty =
@@ -572,6 +609,7 @@ and try_coercions status
               cl, left_p, leftno, rno
           | _ -> raise exn
         in
+        (*{{{*) pp (lazy "CASE");
         let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
           match t,n with
           | _,0 ->
@@ -598,8 +636,8 @@ and try_coercions status
         in
         (*let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.ind(1,0,2)")) in
         let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.con(0,1,2)")) in*)
-        let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/jmeq/jmeq.ind(1,0,2)")) in
-        let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/jmeq/jmeq.con(0,1,2)")) in
+        let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.ind(1,0,2)")) in
+        let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/basics/jmeq/jmeq.con(0,1,2)")) in
         let add_params 
           metasenv subst context cty outty mty m i 
         =
@@ -777,7 +815,7 @@ and try_coercions status
                  ~context ~metasenv ~subst pbo));
                let metasenv, subst, pbo, _ =
                  try_coercions status ~localise menv s context pbo 
-          	 orig_t (*??*) infty_pbo expty_pbo perform_unification exc
+          	 orig_t (*??*) infty_pbo (`Type expty_pbo) exc
                in
                pp 
                  (lazy ("CASE: pbo2: " ^ status#ppterm 
@@ -802,24 +840,29 @@ and try_coercions status
         let t = NCic.Appl (NCic.Match(r,new_outty,m,pl) :: eqs) 
         in
         metasenv, subst, t, expty (*}}}*)
-    | NCic.Prod (nameprod, src, ty),NCic.Prod (_, src2, ty2), _ -> 
-        let rec mk_fresh_name ctx firstch n =
-          let candidate = (String.make 1 firstch) ^ (string_of_int n) in
-          if (List.for_all (fun (s,_) -> s <> candidate) ctx) then candidate
-          else mk_fresh_name ctx firstch (n+1)
+    | _,`Type expty,NCic.LetIn(name,ty,t,bo) -> 
+        pp (lazy "LETIN");
+        let name' = mk_fresh_name context name in
+        let context_bo = (name', NCic.Def (t,ty)) :: context in
+        let metasenv, subst, bo2, _ = 
+          try_coercions status ~localise metasenv subst context_bo
+           bo orig_t (NCicSubstitution.lift status 1 infty)
+           (`Type (NCicSubstitution.lift status 1 expty)) exc
         in
+        let coerced = NCic.LetIn (name',ty,t,bo2) in
+        pp (lazy ("LETIN: coerced = " ^ status#ppterm ~metasenv ~subst ~context coerced));
+        metasenv, subst, coerced, expty
+    | NCic.Prod (nameprod, src, ty),`Type (NCic.Prod (_, src2, ty2) as expty), _ -> 
         (*{{{*) pp (lazy "LAM");
         pp (lazy ("LAM: t = " ^ status#ppterm ~metasenv ~subst ~context t));
-        let name_con = mk_fresh_name context 'c' 0
-          (*FreshNamesGenerator.mk_fresh_name 
-            ~subst metasenv context ~typ:src2 Cic.Anonymous*)
-        in
+        let namename = match t with NCic.Lambda (n,_,_) -> n | _ -> nameprod in
+        let name_con = mk_fresh_name context namename in
         let context_src2 = ((name_con, NCic.Decl src2) :: context) in
         (* contravariant part: the argument of f:src->ty *)
         let metasenv, subst, rel1, _ = 
           try_coercions status ~localise metasenv subst context_src2
            (NCic.Rel 1) orig_t (NCicSubstitution.lift status 1 src2) 
-           (NCicSubstitution.lift status 1 src) perform_unification exc
+           (`Type (NCicSubstitution.lift status 1 src)) exc
         in
         (* covariant part: the result of f(c x); x:src2; (c x):src *)
         let name_t, bo = 
@@ -831,13 +874,23 @@ and try_coercions status
         let ty = cs_subst rel1 (NCicSubstitution.lift_from status 2 1 ty) in
         let metasenv, subst, bo, _ = 
           try_coercions status ~localise metasenv subst context_src2
-            bo orig_t ty ty2 perform_unification exc
+            bo orig_t ty (`Type ty2) exc
         in
         let coerced = NCic.Lambda (name_t,src2, bo) in
         pp (lazy ("LAM: coerced = " ^ status#ppterm ~metasenv ~subst ~context coerced));
         metasenv, subst, coerced, expty (*}}}*)
     | _ -> raise exc
   with exc2 ->    
+  let expty =
+   match expty with
+      `Type expty -> expty
+    | `Sort ->
+        NCic.Sort (NCic.Type 
+         (match NCicEnvironment.get_universes () with
+           | x::_ -> x 
+           | _ -> assert false))
+    | `Prod -> NCic.Prod ("_",NCic.Implicit `Type,NCic.Implicit `Type)
+  in
   pp(lazy("try_coercion " ^ 
     status#ppterm ~metasenv ~subst ~context infty ^ " |---> " ^
     status#ppterm ~metasenv ~subst ~context expty));
@@ -852,15 +905,19 @@ and force_to_sort status metasenv subst context t orig_t localise ty =
       metasenv, subst, t, ty
   with
       Failure _ -> 
+        let msg =
+         (lazy (localise orig_t, 
+           "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^
+           " is not a sort: " ^ status#ppterm ~metasenv ~subst ~context ty)) in
         let ty = NCicReduction.whd status ~subst context ty in
+        let exn =
+         if NCicUnification.could_reduce status ~subst context ty then
+          Uncertain msg
+         else
+          RefineFailure msg
+        in
           try_coercions status ~localise metasenv subst context
-            t orig_t ty (NCic.Sort (NCic.Type 
-              (match NCicEnvironment.get_universes status with
-               | x::_ -> x 
-               | _ -> assert false))) false 
-             (Uncertain (lazy (localise orig_t, 
-             "The type of " ^ status#ppterm ~metasenv ~subst ~context t ^
-             " is not a sort: " ^ status#ppterm ~metasenv ~subst ~context ty)))
+            t orig_t ty `Sort exn
 
 and sort_of_prod status localise metasenv subst context orig_s orig_t (name,s)
  t (t1, t2) 
@@ -987,8 +1044,7 @@ and eat_prods status ~localise force_ty metasenv subst context expty orig_t orig
           let metasenv, subst, newhead, newheadty = 
             try_coercions status ~localise metasenv subst context
               (NCicUntrusted.mk_appl he (List.rev args_so_far)) orig_he ty
-              (NCic.Prod ("_",NCic.Implicit `Term,NCic.Implicit `Term))
-              false
+              `Prod
               (RefineFailure (lazy (localise orig_he, Printf.sprintf
                ("The term %s is here applied to %d arguments but expects " ^^
                "only %d arguments") (status#ppterm ~metasenv ~subst ~context he)
@@ -1204,7 +1260,7 @@ let typeof_obj
                 NCicReduction.whd status ~subst [] ty_sort
                with
                   (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) ->
-                   if not (NCicEnvironment.universe_leq status u1 u2) then
+                   if not (NCicEnvironment.universe_leq u1 u2) then
                     raise
                      (RefineFailure
                        (lazy(localise te, "The type " ^
diff --git a/matitaB/components/ng_refiner/nCicUnification.ml b/matitaB/components/ng_refiner/nCicUnification.ml
index cd5c89dd3..d45b14fc9 100644
--- a/matitaB/components/ng_refiner/nCicUnification.ml
+++ b/matitaB/components/ng_refiner/nCicUnification.ml
@@ -99,6 +99,8 @@ let outside exc_opt =
     match !times with time1::tl -> times := tl; time1 | [] -> assert false in
    prerr_endline ("}}} " ^ !indent ^ " " ^ string_of_float (time2 -. time1));
    (match exc_opt with
+   | Some (UnificationFailure msg) ->  prerr_endline ("exception raised: NCicUnification.UnificationFailure:" ^ Lazy.force msg)
+   | Some (Uncertain msg) ->  prerr_endline ("exception raised: NCicUnification.Uncertain:" ^ Lazy.force msg)
    | Some e ->  prerr_endline ("exception raised: " ^ Printexc.to_string e)
    | None -> ());
    try
@@ -132,13 +134,15 @@ let rec mk_irl stop base =
 ;;
 
 (* the argument must be a term in whd *)
-let rec could_reduce =
+let rec could_reduce status ~subst context =
  function
   | C.Meta _ -> true
   | C.Appl (C.Const (Ref.Ref (_,Ref.Fix (_,recno,_)))::args)
-     when List.length args > recno -> could_reduce (List.nth args recno)
-  | C.Match (_,_,arg,_) -> could_reduce arg
-  | C.Appl (he::_) -> could_reduce he
+     when List.length args > recno ->
+      let t = NCicReduction.whd status ~subst context (List.nth args recno) in
+        could_reduce status subst context t
+  | C.Match (_,_,arg,_) -> could_reduce status ~subst context arg
+  | C.Appl (he::_) -> could_reduce status ~subst context he
   | C.Sort _ | C.Rel _ | C.Prod _ | C.Lambda _ | C.Const _ -> false
   | C.Appl [] | C.LetIn _ | C.Implicit _ -> assert false
 ;;
@@ -273,6 +277,11 @@ let tipify status exc metasenv subst context t ty =
      metasenv,subst,t
 ;;
 
+let put_in_whd status subst context m1 m2 =
+  NCicReduction.reduce_machine status ~delta:max_int ~subst context m1,
+  NCicReduction.reduce_machine status ~delta:max_int ~subst context m2
+;;
+
 let rec instantiate status test_eq_only metasenv subst context n lc t swap =
  (*D*)  inside 'I'; try let rc =  
   pp (lazy(string_of_int n^" :=?= "^ppterm status ~metasenv ~subst ~context t));
@@ -288,14 +297,7 @@ let rec instantiate status test_eq_only metasenv subst context n lc t swap =
       ppterm status ~metasenv ~subst ~context t));
     let (metasenv, subst), t = 
       try 
-        NCicMetaSubst.delift status
-         ~unify:(fun m s c t1 t2 -> 
-           let ind = !indent in
-           let res = 
-             try Some (unify status test_eq_only m s c t1 t2 false)
-             with UnificationFailure _ | Uncertain _ -> None
-           in
-           indent := ind; res) 
+        NCicMetaSubst.delift status ~unify:(unify_for_delift status)
          metasenv subst context n lc t
       with NCicMetaSubst.Uncertain msg -> 
            pp (lazy ("delift is uncertain: " ^ Lazy.force msg));
@@ -362,13 +364,7 @@ let rec instantiate status test_eq_only metasenv subst context n lc t swap =
          NCic.Implicit (`Typeof _) ->
           let (metasenv, subst), ty_t = 
             try 
-              NCicMetaSubst.delift status
-               ~unify:(fun m s c t1 t2 -> 
-                 let ind = !indent in
-                 let res = try Some (unify status test_eq_only m s c t1 t2 false )
-                   with UnificationFailure _ | Uncertain _ -> None
-                 in
-                 indent := ind; res)
+              NCicMetaSubst.delift status ~unify:(unify_for_delift status)
                metasenv subst context n lc ty_t
             with NCicMetaSubst.Uncertain msg -> 
                  pp (lazy ("delift is uncertain: " ^ Lazy.force msg));
@@ -391,22 +387,49 @@ let rec instantiate status test_eq_only metasenv subst context n lc t swap =
          subst)
  (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
 
-and unify status test_eq_only metasenv subst context t1 t2 swap =
- (*D*) inside 'U'; try let rc =
-   let fo_unif test_eq_only metasenv subst (norm1,t1) (norm2,t2) =
-    (*D*) inside 'F'; try let rc =  
-     pp (lazy("  " ^ ppterm status ~metasenv ~subst ~context t1 ^ 
-          (if swap then " ==>?== " 
-           else " ==<?==" ) ^ 
-         ppterm status ~metasenv ~subst ~context t2 ^ ppmetasenv status
-         ~subst metasenv));
-     pp (lazy("  " ^ ppterm status ~metasenv ~subst:[] ~context t1 ^
-          (if swap then " ==>??== " 
-           else " ==<??==" ) ^ 
-         ppterm status ~metasenv ~subst:[] ~context t2 ^ ppmetasenv status
-         ~subst metasenv));
-     if t1 === t2 then
-       metasenv, subst
+and fo_unif_w_hints during_delift status swap test_eq_only metasenv subst context (_,t1 as m1) (_,t2 as m2) =
+ try fo_unif during_delift status swap test_eq_only metasenv subst context m1 m2
+ with 
+ | UnificationFailure _ as exn -> raise exn
+ | KeepReducing _ | Uncertain _ as exn ->
+   let (t1,norm1 as tm1),(t2,norm2 as tm2) =
+    put_in_whd status subst context (0,[],t1,[]) (0,[],t2,[])
+   in
+    match 
+      try_hints status swap test_eq_only metasenv subst context
+       (norm1,NCicReduction.unwind status t1) (norm2,NCicReduction.unwind status t2)
+    with
+     | Some x -> x
+     | None -> 
+         match exn with 
+         | KeepReducing msg -> raise (KeepReducingThis (msg,tm1,tm2))
+         | Uncertain _ as exn -> raise exn
+         | _ -> assert false
+
+and unify_for_delift status metasenv subst context t1 t2 =
+ let ind = !indent in
+ let res = 
+   try Some
+    (fo_unif_w_hints true status false true(*test_eq_only*) metasenv subst
+      context (false,t1) (false,t2))
+   with UnificationFailure _ | Uncertain _ | KeepReducingThis _ -> None
+ in
+ indent := ind; res
+
+and fo_unif0 during_delift status swap test_eq_only metasenv subst context (norm1,t1 as m1) (norm2,t2 as m2) =
+ (*D*) inside 'F'; try let rc =  
+  pp (lazy("  " ^ ppterm status ~metasenv ~subst ~context t1 ^ 
+       (if swap then " ==>?== " 
+        else " ==<?==" ) ^ 
+      ppterm status ~metasenv ~subst ~context t2 ^ ppmetasenv status
+      ~subst metasenv));
+  pp (lazy("  " ^ ppterm status ~metasenv ~subst:[] ~context t1 ^
+       (if swap then " ==>??== " 
+        else " ==<??==" ) ^ 
+      ppterm status ~metasenv ~subst:[] ~context t2 ^ ppmetasenv status
+      ~subst metasenv));
+  if t1 === t2 then
+    metasenv, subst
 (* CSC: To speed up Oliboni's stuff. Why is it necessary, anyway?
      else if
       NCicUntrusted.metas_of_term subst context t1 = [] &&
@@ -417,368 +440,352 @@ and unify status test_eq_only metasenv subst context t1 t2 swap =
       else
        raise (UnificationFailure (lazy "Closed terms not convertible"))
 *)
-     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 ->
-           let a, b = if swap then b,a else a,b in
-           if NCicEnvironment.universe_leq status a b then metasenv, subst
-           else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
-       | (C.Sort (C.Type a), C.Sort (C.Type b)) -> 
-           if NCicEnvironment.universe_eq a b then metasenv, subst
-           else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
-       | (C.Sort C.Prop,C.Sort (C.Type _)) when not swap -> 
-           if (not test_eq_only) then metasenv, subst
-           else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
-       | (C.Sort (C.Type _), C.Sort C.Prop) when swap -> 
-           if (not test_eq_only) then metasenv, subst
-           else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
-
-       | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) 
-       | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
-           let metasenv, subst = unify status true metasenv subst context s1 s2 swap in
-           unify status test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 swap
-       | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
-           let metasenv,subst=unify status test_eq_only metasenv subst context ty1 ty2 swap in
-           let metasenv,subst=unify status test_eq_only metasenv subst context s1 s2 swap in
-           let context = (name1, C.Def (s1,ty1))::context in
-           unify status test_eq_only metasenv subst context t1 t2 swap
-
-       | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
-          (try 
-           let l1 = NCicUtils.expand_local_context l1 in
-           let l2 = NCicUtils.expand_local_context l2 in
-           let metasenv, subst, to_restrict, _ =
-            List.fold_right2 
-             (fun t1 t2 (metasenv, subst, to_restrict, i) -> 
-                try 
-                  let metasenv, subst = 
-                   unify status (*test_eq_only*) true metasenv subst context
-                    (NCicSubstitution.lift status s1 t1) (NCicSubstitution.lift status s2 t2)
-                     swap
-                  in
-                  metasenv, subst, to_restrict, i-1  
-                with UnificationFailure _ | Uncertain _ ->
-                  metasenv, subst, i::to_restrict, i-1)
-             l1 l2 (metasenv, subst, [], List.length l1)
-           in
-           if to_restrict <> [] then
-             let metasenv, subst, _, _ = 
-               NCicMetaSubst.restrict status metasenv subst n1 to_restrict
-             in
-               metasenv, subst
-           else metasenv, subst
-          with 
-           | Invalid_argument _ -> assert false
-           | NCicMetaSubst.MetaSubstFailure msg ->
-              try 
-                let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
-                let term1 = NCicSubstitution.subst_meta status lc1 term in
-                let term2 = NCicSubstitution.subst_meta status lc2 term in
-                  unify status test_eq_only metasenv subst context term1 term2 swap
-              with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
-
-       |  NCic.Appl (NCic.Meta (i,_)::_ as l1),
-          NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
-            (try
-              List.fold_left2 
-                (fun (metasenv, subst) t1 t2 ->
-                  unify status (*test_eq_only*) true metasenv subst context t1 
-                    t2 swap)
-                (metasenv,subst) l1 l2
-            with Invalid_argument _ -> 
-              raise (UnificationFailure (mk_msg status metasenv subst context t1 t2)))
-       
-       | _, NCic.Meta (n, _) when is_locked n subst && not swap->
-           (let (metasenv, subst), i = 
-              match NCicReduction.whd status ~subst context t1 with
-              | NCic.Appl (NCic.Meta (i,l) as meta :: args) ->
-                 let metasenv, lambda_Mj =
-                   lambda_intros status metasenv subst context (List.length args)
-                    (NCicTypeChecker.typeof status ~metasenv ~subst context meta)
-                 in
-                   unify status test_eq_only metasenv subst context 
-                    (C.Meta (i,l)) lambda_Mj false,
-                   i
-              | NCic.Meta (i,_) -> (metasenv, subst), i
-              | _ ->
-                 raise (UnificationFailure (lazy "Locked term vs non
-                  flexible term; probably not saturated enough yet!"))
-             in
-              let t1 = NCicReduction.whd status ~subst context t1 in
-              let j, lj = 
-                match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false
-              in
+ 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 ->
+       let a, b = if swap then b,a else a,b in
+       if NCicEnvironment.universe_leq status a b then metasenv, subst
+       else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
+   | (C.Sort (C.Type a), C.Sort (C.Type b)) -> 
+       if NCicEnvironment.universe_eq a b then metasenv, subst
+       else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
+   | (C.Sort C.Prop,C.Sort (C.Type _)) when not swap -> 
+       if (not test_eq_only) then metasenv, subst
+       else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
+   | (C.Sort (C.Type _), C.Sort C.Prop) when swap -> 
+       if (not test_eq_only) then metasenv, subst
+       else raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
+
+   | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) 
+   | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
+       let metasenv, subst = unify status true metasenv subst context s1 s2 swap in
+       unify status test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2 swap
+   | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
+       let metasenv,subst=unify status test_eq_only metasenv subst context ty1 ty2 swap in
+       let metasenv,subst=unify status test_eq_only metasenv subst context s1 s2 swap in
+       let context = (name1, C.Def (s1,ty1))::context in
+       unify status test_eq_only metasenv subst context t1 t2 swap
+
+   | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
+      (try 
+       let l1 = NCicUtils.expand_local_context l1 in
+       let l2 = NCicUtils.expand_local_context l2 in
+       let metasenv, subst, to_restrict, _ =
+        List.fold_right2 
+         (fun t1 t2 (metasenv, subst, to_restrict, i) -> 
+            try 
               let metasenv, subst = 
-                instantiate status test_eq_only metasenv subst context j lj t2 true
+               unify status (*test_eq_only*) true metasenv subst context
+                (NCicSubstitution.lift status s1 t1) (NCicSubstitution.lift status s2 t2)
+                 swap
               in
-              (* We need to remove the out_scope_tags to avoid propagation of
-                 them that triggers again the ad-hoc case *)
-              let subst =
-               List.map (fun (i,(tag,ctx,bo,ty)) ->
-                let tag =
-                 List.filter
-                  (function `InScope | `OutScope _ -> false | _ -> true) tag
-                in
-                  i,(tag,ctx,bo,ty)
-                ) subst
-              in
-              (try
-                let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
-                let term = eta_reduce status subst term in
-                let subst = List.filter (fun (j,_) -> j <> i) subst in
-                metasenv, ((i, (name, ctx, term, ty)) :: subst)
-              with Not_found -> assert false))
-       | NCic.Meta (n, _), _ when is_locked n subst && swap ->
-           unify status test_eq_only metasenv subst context t2 t1 false
-
-       | t, C.Meta (n,lc) when List.mem_assoc n subst -> 
-          let _,_,term,_ = NCicUtils.lookup_subst n subst in
-          let term = NCicSubstitution.subst_meta status lc term in
-            unify status test_eq_only metasenv subst context t term swap
-       | C.Meta (n,_), _ when List.mem_assoc n subst -> 
-            unify status test_eq_only metasenv subst context t2 t1 (not swap)
-
-       | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
-            let _,_,term,_ = NCicUtils.lookup_subst i subst in
-            let term = NCicSubstitution.subst_meta status l term in
-              unify status test_eq_only metasenv subst context t1 
-                (mk_appl status ~upto:(List.length args) term args) swap
-       | NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst ->
-            unify status test_eq_only metasenv subst context t2 t1 (not swap)
-
-       | C.Meta (n,_), C.Meta (m,lc') when 
-           let _,cc1,_ = NCicUtils.lookup_meta n metasenv in
-           let _,cc2,_ = NCicUtils.lookup_meta m metasenv in
-            (n < m && cc1 = cc2) ||
-             let len1 = List.length cc1 in
-             let len2 = List.length cc2 in
-              len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) ->
-          instantiate status test_eq_only metasenv subst context m lc'
-            (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
-       | C.Meta (n,lc), C.Meta (m,lc') when
-          let _,_,tyn = NCicUtils.lookup_meta n metasenv in
-          let _,_,tym = NCicUtils.lookup_meta m metasenv in
-          let tyn = NCicSubstitution.subst_meta status lc tyn in
-          let tym = NCicSubstitution.subst_meta status lc tym in
-           match tyn,tym with
-              NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
-               NCicEnvironment.universe_lt status u1 u2
-            | _,_ -> false ->
-          instantiate status test_eq_only metasenv subst context m lc'
-            (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
-       | C.Meta (n,lc), t -> 
-          instantiate status test_eq_only metasenv subst context n lc 
-            (NCicReduction.head_beta_reduce status ~subst t) swap
-       | t, C.Meta (n,lc) -> 
-          instantiate status test_eq_only metasenv subst context n lc 
-           (NCicReduction.head_beta_reduce status ~subst t) (not swap)
-
-       (* higher order unification case *)
-       | NCic.Appl (NCic.Meta (i,l) as meta :: args), _ ->
-           (* this easy_case handles "(? ?) =?= (f a)", same number of 
-            * args, preferring the instantiation "f" over "\_.f a" for the
-            * metavariable in head position. Since the arguments of the meta
-            * are flexible, delift would ignore them generating a constant
-            * function even in the easy case above *)
-           let easy_case = 
-             match t2 with
-             | NCic.Appl (f :: f_args)
-               when 
-               List.exists (NCicMetaSubst.is_flexible status context ~subst) args ->
-                let mlen = List.length args in
-                let flen = List.length f_args in
-                let min_len = min mlen flen in
-                let mhe,margs = HExtlib.split_nth (mlen - min_len) args in
-                let fhe,fargs = HExtlib.split_nth (flen - min_len) f_args in
-                 (try 
-                    Some (List.fold_left2 
-                      (fun (m, s) t1 t2 -> 
-                        unify status test_eq_only m s context t1 t2 swap
-                      ) (metasenv,subst)
-                        ((NCicUntrusted.mk_appl meta mhe)::margs)
-                        ((NCicUntrusted.mk_appl f fhe)::fargs))
-                  with UnificationFailure _ | Uncertain _ | KeepReducing _ ->
-                    None) 
-             | _ -> None
+              metasenv, subst, to_restrict, i-1  
+            with UnificationFailure _ | Uncertain _ ->
+              metasenv, subst, i::to_restrict, i-1)
+         l1 l2 (metasenv, subst, [], List.length l1)
+       in
+       if to_restrict <> [] then
+         let metasenv, subst, _, _ = 
+           NCicMetaSubst.restrict status metasenv subst n1 to_restrict
+         in
+           metasenv, subst
+       else metasenv, subst
+      with 
+       | Invalid_argument _ -> assert false
+       | NCicMetaSubst.MetaSubstFailure msg ->
+          try 
+            let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
+            let term1 = NCicSubstitution.subst_meta status lc1 term in
+            let term2 = NCicSubstitution.subst_meta status lc2 term in
+              unify status test_eq_only metasenv subst context term1 term2 swap
+          with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
+
+   |  NCic.Appl (NCic.Meta (i,_)::_ as l1),
+      NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
+        (try
+          List.fold_left2 
+            (fun (metasenv, subst) t1 t2 ->
+              unify status (*test_eq_only*) true metasenv subst context t1 
+                t2 swap)
+            (metasenv,subst) l1 l2
+        with Invalid_argument _ -> 
+          raise (UnificationFailure (mk_msg status metasenv subst context t1 t2)))
+   
+   | _, NCic.Meta (n, _) when is_locked n subst && not swap && not during_delift ->
+       (let (metasenv, subst), i = 
+          match NCicReduction.whd status ~subst context t1 with
+          | NCic.Appl (NCic.Meta (i,l) as meta :: args) ->
+             let metasenv, lambda_Mj =
+               lambda_intros status metasenv subst context (List.length args)
+                (NCicTypeChecker.typeof status ~metasenv ~subst context meta)
+             in
+               unify status test_eq_only metasenv subst context 
+                (C.Meta (i,l)) lambda_Mj false,
+               i
+          | NCic.Meta (i,_) -> (metasenv, subst), i
+          | _ ->
+             raise (UnificationFailure (lazy "Locked term vs non
+              flexible term; probably not saturated enough yet!"))
+         in
+          let t1 = NCicReduction.whd status ~subst context t1 in
+          let j, lj = 
+            match t1 with NCic.Meta (j,l) -> j, l | _ -> assert false
+          in
+          let metasenv, subst = 
+            instantiate status test_eq_only metasenv subst context j lj t2 true
+          in
+          (* We need to remove the out_scope_tags to avoid propagation of
+             them that triggers again the ad-hoc case *)
+          let subst =
+           List.map (fun (i,(tag,ctx,bo,ty)) ->
+            let tag =
+             List.filter
+              (function `InScope | `OutScope _ -> false | _ -> true) tag
+            in
+              i,(tag,ctx,bo,ty)
+            ) subst
+          in
+          (try
+            let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
+            let term = eta_reduce status subst term in
+            let subst = List.filter (fun (j,_) -> j <> i) subst in
+            metasenv, ((i, (name, ctx, term, ty)) :: subst)
+          with Not_found -> assert false))
+   | NCic.Meta (n, _), _ when is_locked n subst && swap ->
+      fo_unif0 during_delift status false test_eq_only metasenv subst context m2 m1
+
+   | _, C.Meta (n,lc) when List.mem_assoc n subst -> 
+      let _,_,term,_ = NCicUtils.lookup_subst n subst in
+      let term = NCicSubstitution.subst_meta status lc term in
+        fo_unif0 during_delift status swap test_eq_only metasenv subst context
+         m1 (false,term)
+   | C.Meta (n,_), _ when List.mem_assoc n subst -> 
+      fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1
+
+   | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
+      let _,_,term,_ = NCicUtils.lookup_subst i subst in
+      let term = NCicSubstitution.subst_meta status l term in
+        fo_unif0 during_delift status swap test_eq_only metasenv subst context
+         m1 (false,mk_appl status ~upto:(List.length args) term args)
+   | NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst ->
+      fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1
+
+   | C.Meta (n,_), C.Meta (m,lc') when 
+       let _,cc1,_ = NCicUtils.lookup_meta n metasenv in
+       let _,cc2,_ = NCicUtils.lookup_meta m metasenv in
+        (n < m && cc1 = cc2) ||
+         let len1 = List.length cc1 in
+         let len2 = List.length cc2 in
+          len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) ->
+      instantiate status test_eq_only metasenv subst context m lc'
+        (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
+   | C.Meta (n,lc), C.Meta (m,lc') when
+      let _,_,tyn = NCicUtils.lookup_meta n metasenv in
+      let _,_,tym = NCicUtils.lookup_meta m metasenv in
+      let tyn = NCicSubstitution.subst_meta status lc tyn in
+      let tym = NCicSubstitution.subst_meta status lc tym in
+       match tyn,tym with
+          NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
+           NCicEnvironment.universe_lt u1 u2
+        | _,_ -> false ->
+      instantiate status test_eq_only metasenv subst context m lc'
+        (NCicReduction.head_beta_reduce status ~subst t1) (not swap)
+   | C.Meta (n,lc), t -> 
+      instantiate status test_eq_only metasenv subst context n lc 
+        (NCicReduction.head_beta_reduce status ~subst t) swap
+   | t, C.Meta (n,lc) -> 
+      instantiate status test_eq_only metasenv subst context n lc 
+       (NCicReduction.head_beta_reduce status ~subst t) (not swap)
+
+   (* higher order unification case *)
+   | NCic.Appl (NCic.Meta (i,l) as meta :: args), _ ->
+       (* this easy_case handles "(? ?) =?= (f a)", same number of 
+        * args, preferring the instantiation "f" over "\_.f a" for the
+        * metavariable in head position. Since the arguments of the meta
+        * are flexible, delift would ignore them generating a constant
+        * function even in the easy case above *)
+       let easy_case = 
+         match t2 with
+         | NCic.Appl (f :: f_args)
+           when 
+           List.exists (NCicMetaSubst.is_flexible status context ~subst) args ->
+            let mlen = List.length args in
+            let flen = List.length f_args in
+            let min_len = min mlen flen in
+            let mhe,margs = HExtlib.split_nth (mlen - min_len) args in
+            let fhe,fargs = HExtlib.split_nth (flen - min_len) f_args in
+             (try 
+                Some (List.fold_left2 
+                  (fun (m, s) t1 t2 -> 
+                    unify status test_eq_only m s context t1 t2 swap
+                  ) (metasenv,subst)
+                    ((NCicUntrusted.mk_appl meta mhe)::margs)
+                    ((NCicUntrusted.mk_appl f fhe)::fargs))
+              with UnificationFailure _ | Uncertain _ | KeepReducing _ ->
+                None) 
+         | _ -> None
+       in
+       (match easy_case with
+       | Some ms -> ms
+       | None ->
+           (* This case handles "(?_f ..ti..) =?= t2", abstracting every
+            * non flexible ti (delift skips local context items that are
+            * flexible) from t2 in two steps:
+            *  1) ?_f := \..xi.. .?
+            *  2) ?_f ..ti..  =?= t2 --unif_machines-->
+                  ?_f[..ti..] =?= t2 --instantiate-->
+                  delift [..ti..] t2 *)
+           let metasenv, lambda_Mj =
+             lambda_intros status metasenv subst context (List.length args)
+              (NCicTypeChecker.typeof status ~metasenv ~subst context meta)
            in
-           (match easy_case with
-           | Some ms -> ms
-           | None ->
-               (* This case handles "(?_f ..ti..) =?= t2", abstracting every
-                * non flexible ti (delift skips local context items that are
-                * flexible) from t2 in two steps:
-                *  1) ?_f := \..xi.. .?
-                *  2) ?_f ..ti..  =?= t2 --unif_machines-->
-                      ?_f[..ti..] =?= t2 --instantiate-->
-                      delift [..ti..] t2 *)
-               let metasenv, lambda_Mj =
-                 lambda_intros status metasenv subst context (List.length args)
-                  (NCicTypeChecker.typeof status ~metasenv ~subst context meta)
-               in
-               let metasenv, subst = 
-                 unify status test_eq_only metasenv subst context 
-                   (C.Meta (i,l)) lambda_Mj swap
-               in
-               let metasenv, subst = 
-                 unify status test_eq_only metasenv subst context t1 t2 swap
-               in
-               (try
-                 let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
-                 let term = eta_reduce status subst term in
-                 let subst = List.filter (fun (j,_) -> j <> i) subst in
-                 metasenv, ((i, (name, ctx, term, ty)) :: subst)
-               with Not_found -> assert false))
-
-       | _, NCic.Appl (NCic.Meta (_,_) :: _) ->
-           unify status test_eq_only metasenv subst context t2 t1 (not swap)
-
-       (* processing this case here we avoid a useless small delta step *)
-       | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2)) 
-         when Ref.eq r1 r2 ->
-           let relevance = NCicEnvironment.get_relevance status r1 in
-           let metasenv, subst, _ = 
-             try
-               List.fold_left2 
-                 (fun (metasenv, subst, relevance) t1 t2 ->
-                    let b, relevance = 
-                      match relevance with b::tl -> b,tl | _ -> true, [] in
-                    let metasenv, subst = 
-                      try unify status test_eq_only metasenv subst context t1 t2
-                            swap
-                      with UnificationFailure _ | Uncertain _ when not b ->
-                        metasenv, subst
-                    in
-                      metasenv, subst, relevance)
-                 (metasenv, subst, relevance) tl1 tl2
-             with
-                Invalid_argument _ -> 
-                 raise (Uncertain (mk_msg status metasenv subst context t1 t2))
-              | KeepReducing _ | KeepReducingThis _ -> assert false
-           in 
-             metasenv, subst
-
-       | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
-          C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 ->
-           let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys status ref1 in
-           let _,_,ty,_ = List.nth itl tyno in
-           let rec remove_prods ~subst context ty = 
-             let ty = NCicReduction.whd status ~subst context ty in
-             match ty with
-             | C.Sort _ -> ty
-             | C.Prod (name,so,ta) -> 
-                   remove_prods ~subst ((name,(C.Decl so))::context) ta
-             | _ -> assert false
+           let metasenv, subst = 
+             unify status test_eq_only metasenv subst context 
+               (C.Meta (i,l)) lambda_Mj swap
            in
-           let is_prop = 
-             match remove_prods ~subst [] ty with
-             | C.Sort C.Prop -> true
-             | _ -> false 
+           let metasenv, subst = 
+             unify status test_eq_only metasenv subst context t1 t2 swap
            in
-           (* if not (Ref.eq ref1 ref2) then 
-             raise (Uncertain (mk_msg status metasenv subst context t1 t2))
-           else*)
-             let metasenv, subst = 
-              unify status test_eq_only metasenv subst context outtype1 outtype2 swap in
-             let metasenv, subst = 
-               try unify status test_eq_only metasenv subst context term1 term2 swap
-               with UnificationFailure _ | Uncertain _ when is_prop -> 
-                 metasenv, subst
-             in
-             (try
-              List.fold_left2 
-               (fun (metasenv,subst) t1 t2 -> 
-                  unify status test_eq_only metasenv subst context t1 t2 swap)
-               (metasenv, subst) pl1 pl2
-             with Invalid_argument _ -> assert false)
-       | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
-       | _ when norm1 && norm2 ->
-           if (could_reduce t1 || could_reduce t2) then
-            raise (Uncertain (mk_msg status metasenv subst context t1 t2))
-           else
-            raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
-       | _ -> raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
-     (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
-    in
-    let fo_unif test_eq_only metasenv subst (norm1,t1 as nt1) (norm2,t2 as nt2)=
-     try fo_unif test_eq_only metasenv subst nt1 nt2
-     with
-      UnificationFailure _ | Uncertain _ when not norm1 || not norm2 ->
-       raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
-    in
-    let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
-      if NCicUntrusted.metas_of_term status subst context t1 = [] &&
-         NCicUntrusted.metas_of_term status subst context t2 = [] 
-      then None 
-      else begin
-    (*D*) inside 'H'; try let rc =  
-     pp(lazy ("\nProblema:\n" ^
-        ppterm status ~metasenv ~subst ~context t1 ^ " =?= " ^
-        ppterm status ~metasenv ~subst ~context t2));
-      let candidates = 
-        NCicUnifHint.look_for_hint status metasenv subst context t1 t2
-      in
-      let rec cand_iter = function
-        | [] -> None (* raise exc *)
-        | (metasenv,(c1,c2),premises)::tl -> 
-            pp (lazy ("\nProvo il candidato:\n" ^ 
-              String.concat "\n"
-                (List.map 
-                  (fun (a,b) ->
-                   ppterm status ~metasenv ~subst ~context a ^  " =?= " ^
-                   ppterm status ~metasenv ~subst ~context b) premises) ^
-              "\n-------------------------------------------\n"^
-              ppterm status ~metasenv ~subst ~context c1 ^  " = " ^
-              ppterm status ~metasenv ~subst ~context c2));
-            try 
-    (*D*) inside 'K'; try let rc =  
-              let metasenv,subst = 
-                fo_unif test_eq_only metasenv subst mt1 (false,c1) in
-              let metasenv,subst = 
-                fo_unif test_eq_only metasenv subst (false,c2) mt2 in
-              let metasenv,subst = 
-                List.fold_left 
-                  (fun (metasenv, subst) (x,y) ->
-                     unify status test_eq_only metasenv subst context x y false)
-                  (metasenv, subst) (List.rev premises)
-              in
-              pp(lazy("FUNZIONA!"));
-              Some (metasenv, subst)
-     (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
-            with
-             KeepReducing _ | UnificationFailure _ | Uncertain _ -> cand_iter tl
-           | KeepReducingThis _ -> assert false
-      in
-        cand_iter candidates
-     (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
-      end
-    in
-    let put_in_whd m1 m2 =
-      NCicReduction.reduce_machine status ~delta:max_int ~subst context m1,
-      NCicReduction.reduce_machine status ~delta:max_int ~subst context m2
-    in
-    let fo_unif_w_hints test_eq_only metasenv subst (_,t1 as m1) (_,t2 as m2) =
-      try fo_unif test_eq_only metasenv subst m1 m2
-      with 
-      | UnificationFailure _ as exn -> raise exn
-      | KeepReducing _ | Uncertain _ as exn ->
-        let (t1,norm1 as tm1),(t2,norm2 as tm2) =
-         put_in_whd (0,[],t1,[]) (0,[],t2,[])
-        in
-         match 
-           try_hints metasenv subst 
-            (norm1,NCicReduction.unwind status t1) (norm2,NCicReduction.unwind status t2)
+           (try
+             let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
+             let term = eta_reduce status subst term in
+             let subst = List.filter (fun (j,_) -> j <> i) subst in
+             metasenv, ((i, (name, ctx, term, ty)) :: subst)
+           with Not_found -> assert false))
+
+   | _, NCic.Appl (NCic.Meta (_,_) :: _) ->
+     fo_unif0 during_delift status (not swap) test_eq_only metasenv subst context m2 m1
+
+   | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
+       let metasenv,subst =
+        fo_unif0 during_delift status swap test_eq_only metasenv subst context
+         (false,hd1) (false,hd2) in
+       let relevance =
+         match hd1 with
+         | C.Const r -> NCicEnvironment.get_relevance status r
+         | _ -> [] in
+       let metasenv, subst, _ = 
+         try
+           List.fold_left2 
+             (fun (metasenv, subst, relevance) t1 t2 ->
+                let b, relevance = 
+                  match relevance with b::tl -> b,tl | _ -> true, [] in
+                let metasenv, subst = 
+                  try unify status test_eq_only metasenv subst context t1 t2
+                        swap
+                  with UnificationFailure _ | Uncertain _ when not b ->
+                    metasenv, subst
+                in
+                  metasenv, subst, relevance)
+             (metasenv, subst, relevance) tl1 tl2
          with
-          | Some x -> x
-          | None -> 
-              match exn with 
-              | KeepReducing msg -> raise (KeepReducingThis (msg,tm1,tm2))
-              | Uncertain _ as exn -> raise exn
-              | _ -> assert false
-    in
+            Invalid_argument _ -> 
+             raise (Uncertain (mk_msg status metasenv subst context t1 t2))
+          | KeepReducing _ | KeepReducingThis _ -> assert false
+       in 
+         metasenv, subst
+
+   | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
+      C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 ->
+       let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys status ref1 in
+       let _,_,ty,_ = List.nth itl tyno in
+       let rec remove_prods ~subst context ty = 
+         let ty = NCicReduction.whd status ~subst context ty in
+         match ty with
+         | C.Sort _ -> ty
+         | C.Prod (name,so,ta) -> 
+               remove_prods ~subst ((name,(C.Decl so))::context) ta
+         | _ -> assert false
+       in
+       let is_prop = 
+         match remove_prods ~subst [] ty with
+         | C.Sort C.Prop -> true
+         | _ -> false 
+       in
+       (* if not (Ref.eq ref1 ref2) then 
+         raise (Uncertain (mk_msg status metasenv subst context t1 t2))
+       else*)
+         let metasenv, subst = 
+          unify status test_eq_only metasenv subst context outtype1 outtype2 swap in
+         let metasenv, subst = 
+           try unify status test_eq_only metasenv subst context term1 term2 swap
+           with UnificationFailure _ | Uncertain _ when is_prop -> 
+             metasenv, subst
+         in
+         (try
+          List.fold_left2 
+           (fun (metasenv,subst) t1 t2 -> 
+              unify status test_eq_only metasenv subst context t1 t2 swap)
+           (metasenv, subst) pl1 pl2
+         with Invalid_argument _ -> assert false)
+   | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
+   | _ when norm1 && norm2 ->
+       if (could_reduce status ~subst context t1 || could_reduce status ~subst context t2) then
+        raise (Uncertain (mk_msg status metasenv subst context t1 t2))
+       else
+        raise (UnificationFailure (mk_msg status metasenv subst context t1 t2))
+   | _ -> raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
+ (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
+
+and try_hints status swap test_eq_only metasenv subst context (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
+  if NCicUntrusted.metas_of_term status subst context t1 = [] &&
+     NCicUntrusted.metas_of_term status subst context t2 = [] 
+  then None 
+  else begin
+(*D*) inside 'H'; try let rc =  
+ pp(lazy ("\nProblema:\n" ^
+    ppterm status ~metasenv ~subst ~context t1 ^ " =?= " ^
+    ppterm status ~metasenv ~subst ~context t2));
+  let candidates = 
+    NCicUnifHint.look_for_hint status metasenv subst context t1 t2
+  in
+  let rec cand_iter = function
+    | [] -> None (* raise exc *)
+    | (metasenv,(c1,c2),premises)::tl -> 
+        pp (lazy ("\nProvo il candidato:\n" ^ 
+          String.concat "\n"
+            (List.map 
+              (fun (a,b) ->
+               ppterm status ~metasenv ~subst ~context a ^  " =?= " ^
+               ppterm status ~metasenv ~subst ~context b) premises) ^
+          "\n-------------------------------------------\n"^
+          ppterm status ~metasenv ~subst ~context c1 ^  " = " ^
+          ppterm status ~metasenv ~subst ~context c2));
+        try 
+(*D*) inside 'K'; try let rc =  
+          let metasenv,subst = 
+           fo_unif false status swap test_eq_only metasenv subst context mt1 (false,c1) in
+          let metasenv,subst = 
+           fo_unif false status swap test_eq_only metasenv subst context (false,c2) mt2 in
+          let metasenv,subst = 
+            List.fold_left 
+              (fun (metasenv, subst) (x,y) ->
+                 unify status test_eq_only metasenv subst context x y false)
+              (metasenv, subst) (List.rev premises)
+          in
+          pp(lazy("FUNZIONA!"));
+          Some (metasenv, subst)
+ (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
+        with
+         KeepReducing _ | UnificationFailure _ | Uncertain _ -> cand_iter tl
+       | KeepReducingThis _ -> assert false
+  in
+    cand_iter candidates
+ (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
+  end
+
+and fo_unif during_delift status swap test_eq_only metasenv subst context (norm1,t1 as nt1) (norm2,t2 as nt2)=
+ try fo_unif0 during_delift status swap test_eq_only metasenv subst context nt1 nt2
+ with
+  UnificationFailure _ | Uncertain _ when not norm1 || not norm2 ->
+   raise (KeepReducing (mk_msg status metasenv subst context t1 t2))
+
+and unify status test_eq_only metasenv subst context t1 t2 swap =
+ (*D*) inside 'U'; try let rc =
     let fo_unif_heads_and_cont_or_unwind_and_hints 
       test_eq_only metasenv subst m1 m2 cont hm1 hm2
      =
@@ -787,13 +794,13 @@ and unify status test_eq_only metasenv subst context t1 t2 swap =
            and makes unification stronger, but looks not frequent to me
            that heads unify but not the arguments and that an hints can fix 
            that *)
-        try fo_unif test_eq_only metasenv subst m1 m2, cont
+        try fo_unif false status swap test_eq_only metasenv subst context m1 m2, cont
         with 
         | UnificationFailure _ 
         | KeepReducing _ | Uncertain _ as exn ->
            let (t1,norm1),(t2,norm2) = hm1, hm2 in
            match 
-             try_hints metasenv subst 
+             try_hints status swap test_eq_only metasenv subst context
               (norm1,NCicReduction.unwind status t1) (norm2,NCicReduction.unwind status t2)
            with
             | Some x -> x, fun x -> x
@@ -846,7 +853,7 @@ and unify status test_eq_only metasenv subst context t1 t2 swap =
               try
                 let t1 = NCicReduction.from_stack ~delta:max_int t1 in
                 let t2 = NCicReduction.from_stack ~delta:max_int t2 in
-                unif_machines metasenv subst (put_in_whd t1 t2)
+                unif_machines metasenv subst (put_in_whd status subst context t1 t2)
               with UnificationFailure _ | Uncertain _ when not b ->
                 metasenv, subst
           in
@@ -881,12 +888,12 @@ and unify status test_eq_only metasenv subst context t1 t2 swap =
          | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
            -> unif_machines metasenv subst (small_delta_step ~subst m1 m2)
          | UnificationFailure msg
-           when could_reduce (NCicReduction.unwind status (fst m1))
-             || could_reduce (NCicReduction.unwind status (fst m2))
+           when could_reduce status ~subst context (NCicReduction.unwind status (fst m1))
+             || could_reduce status ~subst context (NCicReduction.unwind status (fst m2))
            -> raise (Uncertain msg)
       (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
      in
-     try fo_unif_w_hints test_eq_only metasenv subst (false,t1) (false,t2)
+     try fo_unif_w_hints false status swap test_eq_only metasenv subst context (false,t1) (false,t2)
      with
       | KeepReducingThis (msg,tm1,tm2) ->
          (try 
@@ -903,15 +910,8 @@ and delift_type_wrt_terms status metasenv subst context t args =
   let lc = List.rev args @ mk_irl (List.length context) (List.length args+1) in
   let (metasenv, subst), t =
    try
-    NCicMetaSubst.delift status
-      ~unify:(fun m s c t1 t2 -> 
-         let ind = !indent in
-         let res = 
-           try Some (unify status false m s c t1 t2 false)
-           with UnificationFailure _ | Uncertain _ -> None
-         in
-         indent := ind; res)
-      metasenv subst context 0 (0,NCic.Ctx lc) t
+    NCicMetaSubst.delift status ~unify:(unify_for_delift status)
+      metasenv subst context (-1) (0,NCic.Ctx lc) t
    with
       NCicMetaSubst.MetaSubstFailure _
     | NCicMetaSubst.Uncertain _ -> (metasenv, subst), t
diff --git a/matitaB/components/ng_refiner/nCicUnification.mli b/matitaB/components/ng_refiner/nCicUnification.mli
index d0a539c6a..1ce5a95db 100644
--- a/matitaB/components/ng_refiner/nCicUnification.mli
+++ b/matitaB/components/ng_refiner/nCicUnification.mli
@@ -28,6 +28,10 @@ val fix_sorts:
   #NCicEnvironment.status -> NCic.metasenv -> NCic.substitution -> 
     NCic.term -> NCic.metasenv * NCic.term
 
+(* this should be moved elsewhere *)
+(* The term must be in whd *)
+val could_reduce: #NCicCoercion.status -> subst:NCic.substitution -> NCic.context -> NCic.term -> bool
+
 (* delift_type_wrt_terms st m s c t args
  *   lift t (length args) 
  *      [ rel 1 ... rel (len args) / lift (length args) (arg_1 .. arg_n) ]