Finished

[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 466c0ef855bf93b0bbd4a84ac06eee43558d8fde..c7b487461963a179bd6333232cefb7ce13385bbf 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -241,9 +241,11 @@ let tipify exc metasenv subst context t ty =
         if is_type attrs then
          metasenv,subst,true
         else
+         let _,cc,ty = NCicUtils.lookup_meta n metasenv in
+         let metasenv,subst,ty = sortfy exc metasenv subst cc ty in
          let metasenv = 
            NCicUntrusted.replace_in_metasenv n
-            (fun attrs,cc,ty -> NCicUntrusted.set_kind `IsType attrs, cc, ty)
+            (fun attrs,cc,_ -> NCicUntrusted.set_kind `IsType attrs, cc, ty)
             metasenv 
          in
           metasenv,subst,false
@@ -253,9 +255,11 @@ let tipify exc metasenv subst context t ty =
          if is_type attrs then
           metasenv,subst,true
          else
+          let _,cc,_,ty = NCicUtils.lookup_subst n subst in
+          let metasenv,subst,ty = sortfy exc metasenv subst cc ty in
           let subst = 
             NCicUntrusted.replace_in_subst n
-             (fun attrs,cc,bo,ty->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty)
+              (fun attrs,cc,bo,_->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty)
              subst 
           in
            optimize_meta metasenv subst (NCicSubstitution.subst_meta lc bo))
@@ -354,8 +358,8 @@ let rec instantiate rdb test_eq_only metasenv subst context n lc t swap =
        | _ -> assert false)
   | `IsType
   | `IsTerm ->
-     (match ty,t with
-         NCic.Implicit (`Typeof _), _ ->
+     (match ty with
+         NCic.Implicit (`Typeof _) ->
           let (metasenv, subst), ty_t = 
             try 
               NCicMetaSubst.delift 
@@ -375,7 +379,7 @@ let rec instantiate rdb test_eq_only metasenv subst context n lc t swap =
           in
            delift_to_subst test_eq_only n lc (attrs,cc,ty_t) t context metasenv
             subst 
-       | _, _ ->
+       | _ ->
         let lty = NCicSubstitution.subst_meta lc ty in
         pp (lazy ("On the types: " ^
           ppterm ~metasenv ~subst ~context lty ^ "=<=" ^