]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_refiner/nCicUnification.ml
new instantiate, only known bug is w.r.t. in/out scope and file matita/contribs/ng_as...
[helm.git] / helm / software / components / ng_refiner / nCicUnification.ml
index 8e84c015dbed4c19508b876409678e03e523f22e..edf116d17f08c94464887b7fb609301329e0f217 100644 (file)
@@ -115,26 +115,8 @@ let ppmetasenv ~subst m = "\nmenv:\n" ^ NCicPp.ppmetasenv ~subst m;;
 
 let ppcontext ~metasenv:_metasenv ~subst:_subst _context = "";;
 let ppmetasenv ~subst:_subst _metasenv = "";;
-
-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 " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] orig) ;
-            raise exc
-         | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)
-        else
-         NCic.Sort (NCic.Type (
-           match NCicEnvironment.sup NCicEnvironment.type0 with 
-           | Some x -> x
-           | _ -> assert false))
-    | NCic.Meta _ as orig -> orig
-    | t -> NCicUtils.map (fun _ _ -> ()) () aux t
-  in
-    aux () t
-;;
+let ppterm ~metasenv ~subst ~context = NCicPp.ppterm ~metasenv ~subst ~context;;
+(* let ppterm ~metasenv:_ ~subst:_ ~context:_ _ = "";; *)
 
 let is_locked n subst =
    try
@@ -162,11 +144,11 @@ let rec could_reduce =
 ;;
 
 let rec lambda_intros rdb metasenv subst context argsno ty =
- pp (lazy ("LAMBDA INTROS: " ^ NCicPp.ppterm ~metasenv ~subst ~context ty));
+ pp (lazy ("LAMBDA INTROS: " ^ ppterm ~metasenv ~subst ~context ty));
  match argsno with
     0 -> 
        let metasenv, _, bo, _ = 
-         NCicMetaSubst.mk_meta metasenv context (`WithType ty)
+         NCicMetaSubst.mk_meta metasenv context ~with_type:ty `IsTerm
        in
        metasenv, bo
   | _ ->
@@ -179,181 +161,221 @@ let rec lambda_intros rdb metasenv subst context argsno ty =
            metasenv,C.Lambda (n,so,bo)
        | _ -> assert false)
 ;;
+  
+let unopt exc = function None -> raise exc | Some x -> x ;;
+
+let fix metasenv subst is_sup test_eq_only exc t =
+  let rec aux test_eq_only metasenv = function
+    | NCic.Prod (n,so,ta) ->
+       let metasenv,so = aux true metasenv so in
+       let metasenv,ta = aux test_eq_only metasenv ta in
+        metasenv,NCic.Prod (n,so,ta)
+    | NCic.Sort (NCic.Type [(`CProp|`Type),_]) as orig when test_eq_only ->
+       metasenv,orig
+    | NCic.Sort (NCic.Type _) when test_eq_only -> raise exc
+    | NCic.Sort (NCic.Type u) when is_sup ->
+       metasenv, NCic.Sort (NCic.Type (unopt exc (NCicEnvironment.sup u)))
+    | NCic.Sort (NCic.Type u) ->
+       metasenv, NCic.Sort (NCic.Type 
+         (unopt exc (NCicEnvironment.inf ~strict:false u)))
+    | NCic.Meta (n,_) as orig ->
+        (try 
+          let _,_,_,_ = NCicUtils.lookup_subst n subst in metasenv,orig
+         with NCicUtils.Subst_not_found _ -> 
+          let metasenv, _ = NCicMetaSubst.extend_meta metasenv n in
+           metasenv, orig)
+    | t ->
+      NCicUntrusted.map_term_fold_a (fun _ x -> x) test_eq_only aux metasenv t
+  in
+   aux test_eq_only metasenv t
+;;
+
+let rec sortfy exc metasenv subst = function
+  | NCic.Sort _ as orig -> metasenv, orig
+  | NCic.Meta (n,lc) -> 
+      let attrs, context, ty = NCicUtils.lookup_meta n metasenv in
+      let kind = NCicUntrusted.kind_of_meta attrs in
+      kindfy exc metasenv subst context n lc ty kind `IsSort
+  | NCic.Implicit _ -> assert false
+  | _ -> raise exc
+
+and kindfy exc metasenv subst context n lc ty kind kind2 = 
+  match kind, ty, kind2 with
+  | `IsSort, _, _ -> assert(snd lc = NCic.Irl 0); metasenv, NCic.Meta(n,lc)
+  | k1, NCic.Implicit (`Typeof _), (`IsType|`IsTerm as k2) -> 
+     let k = NCicUntrusted.max_kind k1 k2 in
+     let metasenv = 
+       NCicUntrusted.replace_in_metasenv n
+         (fun attrs,cc,ty -> NCicUntrusted.set_kind k attrs, cc, ty) metasenv 
+     in
+     metasenv, NCic.Meta(n,lc)
+  | _, NCic.Implicit (`Typeof _), `IsSort ->
+     let metasenv = 
+       NCicUntrusted.replace_in_metasenv n
+        (fun attrs,_,ty-> NCicUntrusted.set_kind `IsSort attrs,[],ty) metasenv 
+     in
+     metasenv, NCic.Meta (n,(0,NCic.Irl 0))
+  | _, ty, `IsSort ->
+     let metasenv, ty = 
+       sortfy exc metasenv subst (NCicReduction.whd ~subst context ty) 
+     in
+     let metasenv = 
+       NCicUntrusted.replace_in_metasenv n
+        (fun attrs,_,_-> NCicUntrusted.set_kind `IsSort attrs,[],ty) metasenv 
+     in
+     metasenv, NCic.Meta (n,(0,NCic.Irl 0))
+  | k1, _, k2 when NCicUntrusted.max_kind k1 k2 = k1-> metasenv, NCic.Meta(n,lc)
+  | `IsTerm, ty, `IsType ->
+     let metasenv, ty = 
+       sortfy exc metasenv subst (NCicReduction.whd ~subst context ty) 
+     in
+     let metasenv = 
+       NCicUntrusted.replace_in_metasenv n
+        (fun attrs,cc,_-> NCicUntrusted.set_kind `IsType attrs,cc,ty) metasenv 
+     in
+     metasenv, NCic.Meta (n,lc)
+  | _ -> assert false (* XXX *)
 
-let rec instantiate rdb test_eq_only metasenv subst context n lc t swap =
+and instantiate rdb test_eq_only metasenv subst context n lc t swap =
  (*D*)  inside 'I'; try let rc =  
-         pp (lazy(string_of_int n ^ " :=?= "^
-           NCicPp.ppterm ~metasenv ~subst ~context t));
-  let unify test_eq_only m s c t1 t2 = 
-    if swap then unify rdb test_eq_only m s c t2 t1 
-    else unify rdb test_eq_only m s c t1 t2
-  in
-  let has_tag = List.exists in
-  let tags, _, ty = NCicUtils.lookup_meta n metasenv in
-  (* on the types *)
-  let metasenv, subst, t = 
-    match ty with 
-    | NCic.Implicit (`Typeof _) -> 
-         pp(lazy("meta with no type"));
-         assert(has_tag ((=)`IsSort) tags); 
-         metasenv, subst, t
-    | _ ->
-       let exc_to_be =
-        UnificationFailure (mk_msg 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 as exn -> 
-              pp(lazy("we try to fix the sort\n"^
-                Lazy.force msg^"\n"^NCicPp.ppmetasenv ~subst metasenv));
-              let ft = fix_sorts swap exc_to_be t in
-              pp(lazy("unable to fix the sort"));
-              if ft == t then raise exn;
-              (try ft, NCicTypeChecker.typeof ~subst ~metasenv context ft 
-               with NCicTypeChecker.AssertFailure _ -> raise exn)
-         | NCicTypeChecker.TypeCheckerFailure msg ->
-              prerr_endline (Lazy.force msg);
-              prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
-              prerr_endline (ppcontext ~metasenv ~subst context); 
-              prerr_endline (ppmetasenv ~subst metasenv);
-              assert false
-       in
-       match ty_t with
-       | NCic.Implicit (`Typeof _) -> 
-           raise (UnificationFailure(lazy "trying to unify a term with a type"))
-       | _ -> 
-          let lty = NCicSubstitution.subst_meta lc ty in
-          pp (lazy ("On the types: " ^
-              NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === " ^ 
-              NCicPp.ppterm ~metasenv ~subst ~context ty_t)); 
-          let metasenv,subst = 
-           try unify test_eq_only metasenv subst context lty ty_t
-           with NCicEnvironment.BadConstraint _ as exc ->
-            let ty_t = fix_sorts swap exc_to_be ty_t in 
-             try unify test_eq_only metasenv subst context lty ty_t
-             with 
-             | NCicEnvironment.BadConstraint _ 
-             | UnificationFailure _ -> raise exc 
-          in
-           metasenv, subst, t
-  in 
-  (* viral sortification *)
-  let is_sort metasenv subst context t = 
-    match NCicReduction.whd ~subst context t with
-    | NCic.Meta (i,_) ->
-         let tags, _, _ = NCicUtils.lookup_meta i metasenv in
-         has_tag ((=) `IsSort) tags
-    | NCic.Sort _ -> true
-    | _ -> false
+  pp (lazy(string_of_int n^" :=?= "^ppterm ~metasenv ~subst ~context t));
+  let exc = 
+    UnificationFailure (mk_msg metasenv subst context (NCic.Meta (n,lc)) t) in
+  let move_to_subst i attrs cc t ty metasenv subst =
+    let metasenv = List.remove_assoc i metasenv in
+    pp (lazy(string_of_int n ^ " :==> "^ 
+      ppterm ~metasenv ~subst ~context:cc t));
+    metasenv, (i,(attrs, cc, t, ty)) :: subst
   in
-  let rec sortify metasenv subst = function
-    | NCic.Implicit (`Typeof _) -> assert false 
-    | NCic.Sort _ as t -> metasenv, subst, t, 0
-    | NCic.Meta (i,_) as t -> 
-         let tags, context, ty = NCicUtils.lookup_meta i metasenv in
-         if has_tag ((=) `IsSort) tags then metasenv, subst, t, i
-         else
-           let ty = NCicReduction.whd ~subst context ty in
-           let metasenv, subst, ty, _ = sortify metasenv subst ty in
-           let metasenv, j, m, _ = 
-             NCicMetaSubst.mk_meta metasenv ~attrs:[`IsSort] [] (`WithType ty)
+  let delift_to_subst test_eq_only n lc attrs cc t ty context metasenv subst =
+    pp (lazy(string_of_int n ^ " := 111 = "^ 
+      ppterm ~metasenv ~subst ~context t));
+    let (metasenv, subst), t = 
+      try 
+        NCicMetaSubst.delift 
+         ~unify:(fun m s c t1 t2 -> 
+           let ind = !indent in
+           let res = 
+                   try Some (unify rdb test_eq_only m s c t1 t2 )
+             with UnificationFailure _ | Uncertain _ -> None
            in
-           pp(lazy("rimpiazzo " ^ string_of_int i^" con "^string_of_int j));
-           let subst_entry = i, (tags, context, m, ty) in
-           let subst = subst_entry :: subst in
-           let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
-           metasenv, subst, m, j 
-    | NCic.Appl (NCic.Meta _ as hd :: args) as t -> 
-           let metasenv, lambda_Mj =
-             lambda_intros rdb metasenv subst context (List.length args)
-              (NCicTypeChecker.typeof ~metasenv ~subst context hd)
-           in
-           let metasenv,subst= unify true metasenv subst context hd lambda_Mj in
-           let t = NCicReduction.whd ~subst context t in
-           let _result = sortify metasenv subst t in       
-           (* untested, maybe dead, code *) assert false;
-    | t -> 
-         if could_reduce t then raise (Uncertain(lazy "not a sort"))
-         else raise (UnificationFailure(lazy "not a sort"))
-  in
-  let metasenv, subst, _, n = 
-    if has_tag ((=) `IsSort) tags then
-      let m,s,x,_ = sortify metasenv subst (NCicReduction.whd ~subst context t)
-      in m,s,x,n
-    else if is_sort metasenv subst context t then
-      sortify metasenv subst (NCic.Meta (n,lc))
-    else
-      metasenv, subst, NCic.Rel ~-1,n
-  in
-  let tags, ctx, ty = NCicUtils.lookup_meta n metasenv in
-  (* instantiation *)
-  pp (lazy(string_of_int n ^ " := 111 = "^ 
-    NCicPp.ppterm ~metasenv ~subst ~context t));
-  let (metasenv, subst), t = 
-    try 
-      NCicMetaSubst.delift 
-       ~unify:(fun m s c t1 t2 -> 
-         let ind = !indent in
-         let res = 
-           try Some (unify test_eq_only m s c t1 t2 )
-           with UnificationFailure _ | Uncertain _ -> None
-         in
-         indent := ind; res) 
-       metasenv subst context n lc t
-    with NCicMetaSubst.Uncertain msg -> 
-         pp (lazy ("delift fails: " ^ Lazy.force msg));
-         raise (Uncertain msg)
-    | NCicMetaSubst.MetaSubstFailure msg -> 
-         pp (lazy ("delift fails: " ^ Lazy.force msg));
-         raise (UnificationFailure msg)
-  in
-         pp (lazy(string_of_int n ^ " := 222 = "^
-           NCicPp.ppterm ~metasenv ~subst ~context:ctx t
-         ^ ppmetasenv ~subst metasenv));
-  (* Unifying the types may have already instantiated n. *)
-  try
-    let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
-    let oldt = NCicSubstitution.subst_meta lc oldt in
-    let t = NCicSubstitution.subst_meta lc t in
-    (* conjecture: always fail --> occur check *)
-    unify test_eq_only metasenv subst context oldt t
-  with NCicUtils.Subst_not_found _ -> 
-    let metasenv, tags = 
-      let rec aux = function
-        | NCic.Meta (j,lc) -> 
-            (try 
-              let _, _, t, _ = NCicUtils.lookup_subst j subst in
-              aux (NCicSubstitution.subst_meta lc t)
-            with NCicUtils.Subst_not_found _ -> 
-              let tags', ctx, ty = NCicUtils.lookup_meta j metasenv in
-              let metasenv = List.remove_assoc j metasenv in
-              let tags = tags @ tags' in
-              (j, (tags, ctx, ty)) :: metasenv, tags)
-        | _ -> metasenv, tags
-      in 
-        aux t
+           indent := ind; res) 
+         metasenv subst context n lc t
+      with NCicMetaSubst.Uncertain msg -> 
+           pp (lazy ("delift is uncertain: " ^ Lazy.force msg));
+           raise (Uncertain msg)
+      | NCicMetaSubst.MetaSubstFailure msg -> 
+           pp (lazy ("delift fails: " ^ Lazy.force msg));
+           raise (UnificationFailure msg)
     in
-    (* by cumulativity when unify(?,Type_i) 
-     * we could ? := Type_j with j <= i... *)
-    let subst = (n, (tags, ctx, t, ty)) :: subst in
-    pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm
-      ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t)));
-    let metasenv = 
-      List.filter (fun (m,_) -> not (n = m)) metasenv 
-    in
-    metasenv, subst
+    pp (lazy(string_of_int n ^ " := 222 = "^
+      ppterm ~metasenv ~subst ~context:cc t^ppmetasenv ~subst metasenv));
+    (* Unifying the types may have already instantiated n. *)
+    try
+      let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
+      let oldt = NCicSubstitution.subst_meta lc oldt in
+      let t = NCicSubstitution.subst_meta lc t in
+      (* conjecture: always fail --> occur check *)
+      unify rdb test_eq_only metasenv subst context t oldt
+    with NCicUtils.Subst_not_found _ -> 
+      move_to_subst n attrs cc t ty metasenv subst
+  in
+  let attrs, cc, ty = NCicUtils.lookup_meta n metasenv in
+  match NCicUntrusted.kind_of_meta attrs, ty, t, swap with
+  | `IsSort, (NCic.Implicit (`Typeof _) as bot), NCic.Sort (NCic.Type u),false->
+      pp(lazy("1"));
+      let u = NCicEnvironment.inf ~strict:false u in
+      let t = NCic.Sort (NCic.Type (unopt exc u)) in
+      move_to_subst n attrs cc t bot metasenv subst  
+  | `IsSort, (NCic.Implicit (`Typeof _) as bot), NCic.Sort (NCic.Type u),true ->
+      pp(lazy("2"));
+      let u = NCicEnvironment.sup u in
+      let t = NCic.Sort (NCic.Type (unopt exc u)) in
+      move_to_subst n attrs cc t bot metasenv subst  
+  | `IsSort, (NCic.Sort(NCic.Type u1) as ty), NCic.Sort (NCic.Type u2), false ->
+      pp(lazy("3"));
+      let u = 
+        NCicEnvironment.inf ~strict:false (u1 @
+          unopt exc (NCicEnvironment.inf ~strict:true u2)) 
+      in
+      let t = NCic.Sort (NCic.Type (unopt exc u)) in
+      move_to_subst n attrs cc t ty metasenv subst  
+  | `IsSort, (NCic.Sort(NCic.Type u1) as ty), NCic.Sort (NCic.Type u2), true ->
+      pp(lazy("4"));
+      let u = unopt exc (NCicEnvironment.sup u2) in
+      if NCicEnvironment.universe_lt u u1 then
+        let t = NCic.Sort (NCic.Type u) in
+        move_to_subst n attrs cc t ty metasenv subst  
+      else (raise exc)
+  | _, _, NCic.Meta(m,lcm), _ when List.mem_assoc m subst ->
+      (* deref needed for locked metas, maybe should be done outside *)
+      let _,_,bo,_ = NCicUtils.lookup_subst m subst in
+      let bo = NCicSubstitution.subst_meta lcm bo in
+      instantiate rdb test_eq_only metasenv subst context n lc bo swap
+  | kind, (NCic.Implicit (`Typeof _) as bot),  NCic.Meta(m,lcm), _ ->
+      pp(lazy("5"));
+      let attrsm, ccm, tym = NCicUtils.lookup_meta m metasenv in
+      let kindm = NCicUntrusted.kind_of_meta attrsm in
+      let metasenv, t = kindfy exc metasenv subst ccm m lcm tym kindm kind in
+      move_to_subst n attrs cc t bot metasenv subst  
+  | kind, ty,  (NCic.Meta(m,_) as t), _ when 
+    let _, _, tym = NCicUtils.lookup_meta m metasenv in
+    (match tym with NCic.Implicit (`Typeof _) -> true | _ -> false) ->
+      pp(lazy("6"));
+      let attrsm, _, _ = NCicUtils.lookup_meta m metasenv in
+      let kindm = NCicUntrusted.kind_of_meta attrsm in
+      let metasenv, _ = kindfy exc metasenv subst cc n lc ty kind kindm in
+      let attrs, cc, ty = NCicUtils.lookup_meta n metasenv in
+      let metasenv = NCicUntrusted.replace_in_metasenv m
+        (fun _,_,_ -> attrs,cc,ty) metasenv
+      in
+      (* XXX *)move_to_subst n attrs cc t ty metasenv subst  
+  | kind, ty,  NCic.Meta(m,lcm), _ ->
+      pp(lazy("7"));
+      let ty_t, ccm, kindm = 
+        let at, ccm, tym = NCicUtils.lookup_meta m metasenv in
+        NCicSubstitution.subst_meta lcm tym, ccm, NCicUntrusted.kind_of_meta at
+      in
+      let lty = NCicSubstitution.subst_meta lc ty in
+      pp (lazy ("On the types: " ^
+        ppterm ~metasenv ~subst ~context lty ^
+        (if test_eq_only then " === " else "=<=") ^
+        ppterm ~metasenv ~subst ~context ty_t)); 
+      let metasenv, subst = 
+        unify rdb test_eq_only metasenv subst context ty_t lty
+      in
+      let metasenv, t = kindfy exc metasenv subst ccm m lcm ty_t kindm kind in
+      delift_to_subst test_eq_only n lc attrs cc t ty context metasenv subst 
+  | _, (NCic.Implicit (`Typeof _) as bot), t, swap ->
+      pp(lazy("8"));
+      let metasenv, t = fix metasenv subst swap test_eq_only exc t in
+(*       let ty_t = NCicTypeChecker.typeof ~metasenv ~subst context t in *)
+      (* ty andrebbe deliftato *)
+      delift_to_subst test_eq_only n lc attrs cc t bot context metasenv subst 
+  | _, ty, t, swap ->
+      pp(lazy("9"));
+      let lty = NCicSubstitution.subst_meta lc ty in
+      let metasenv, t = fix metasenv subst swap test_eq_only exc t in
+      let ty_t = NCicTypeChecker.typeof ~metasenv ~subst context t in
+      pp (lazy ("On the types: " ^
+        ppterm ~metasenv ~subst ~context lty ^
+        (if test_eq_only then " === " else "=<=") ^
+        ppterm ~metasenv ~subst ~context ty_t)); 
+      let metasenv, subst = 
+        unify rdb test_eq_only metasenv subst context ty_t lty
+      in
+      delift_to_subst test_eq_only n lc attrs cc t ty context metasenv subst 
  (*D*)  in outside None; rc with exn -> outside (Some exn); raise exn 
 
 and unify rdb test_eq_only metasenv subst context t1 t2 =
  (*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("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^ 
-         NCicPp.ppterm ~metasenv ~subst ~context t2 ^ ppmetasenv
+     pp (lazy("  " ^ ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^ 
+         ppterm ~metasenv ~subst ~context t2 ^ ppmetasenv
          ~subst metasenv));
-     pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst:[] ~context t1 ^ " ==??== " ^ 
-         NCicPp.ppterm ~metasenv ~subst:[] ~context t2 ^ ppmetasenv
+     pp (lazy("  " ^ ppterm ~metasenv ~subst:[] ~context t1 ^ " ==??== " ^ 
+         ppterm ~metasenv ~subst:[] ~context t2 ^ ppmetasenv
          ~subst metasenv));
      if t1 === t2 then
        metasenv, subst
@@ -614,8 +636,8 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
     let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
     (*D*) inside 'H'; try let rc =  
      pp(lazy ("\nProblema:\n" ^
-        NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^
-        NCicPp.ppterm ~metasenv ~subst ~context t2));
+        ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^
+        ppterm ~metasenv ~subst ~context t2));
       let candidates = 
         NCicUnifHint.look_for_hint rdb metasenv subst context t1 t2
       in
@@ -626,11 +648,11 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
               String.concat "\n"
                 (List.map 
                   (fun (a,b) ->
-                   NCicPp.ppterm ~metasenv ~subst ~context a ^  " =?= " ^
-                   NCicPp.ppterm ~metasenv ~subst ~context b) premises) ^
+                   ppterm ~metasenv ~subst ~context a ^  " =?= " ^
+                   ppterm ~metasenv ~subst ~context b) premises) ^
               "\n-------------------------------------------\n"^
-              NCicPp.ppterm ~metasenv ~subst ~context c1 ^  " = " ^
-              NCicPp.ppterm ~metasenv ~subst ~context c2));
+              ppterm ~metasenv ~subst ~context c1 ^  " = " ^
+              ppterm ~metasenv ~subst ~context c2));
             try 
     (*D*) inside 'K'; try let rc =  
               let metasenv,subst = 
@@ -657,7 +679,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
       NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
       NCicReduction.reduce_machine ~delta:max_int ~subst context m2
     in
-    let fo_unif_w_hints test_eq_only metasenv subst (xx1,t1 as m1) (xx2,t2 as m2) =
+    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
@@ -703,10 +725,10 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
       | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
      (*D*) inside 'M'; try let rc = 
          pp (lazy("UM: " ^
-           NCicPp.ppterm ~metasenv ~subst ~context 
+           ppterm ~metasenv ~subst ~context 
              (NCicReduction.unwind (k1,e1,t1,s1)) ^
            " === " ^ 
-           NCicPp.ppterm ~metasenv ~subst ~context 
+           ppterm ~metasenv ~subst ~context 
              (NCicReduction.unwind (k2,e2,t2,s2))));
          pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
           let relevance = [] (* TO BE UNDERSTOOD 
@@ -789,4 +811,6 @@ let unify rdb ?(test_eq_only=false) =
   indent := "";      
   unify rdb test_eq_only;;
 
-let fix_sorts = fix_sorts true (UnificationFailure (lazy "no sup"));;
+let fix_sorts m s =
+  fix m s true false (UnificationFailure (lazy "no sup"))
+;;