X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=1f03755ffbd9cde673cc3be5c9cbeffe9809d23f;hb=63047f8ff8ef477ac32939985b0b41b70e918054;hp=805ea859f8beef8be33eb03d123b850f37a5c48e;hpb=a4615d355dba036f1faf4aa3306e005da5e839a0;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 805ea859f..1f03755ff 100644
--- 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 ^ "=<=" ^
@@ -546,6 +550,15 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
        | NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst ->
             unify rdb 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 rdb test_eq_only metasenv subst context m lc'
+            (NCicReduction.head_beta_reduce ~subst t1) (not swap)
        | C.Meta (n,lc), t -> 
           instantiate rdb test_eq_only metasenv subst context n lc 
             (NCicReduction.head_beta_reduce ~subst t) swap
@@ -606,7 +619,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
              metasenv, subst
 
        | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
-          C.Match (ref2,outtype2,term2,pl2)) ->
+          C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 ->
            let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
            let _,_,ty,_ = List.nth itl tyno in
            let rec remove_prods ~subst context ty = 
@@ -622,9 +635,9 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
              | C.Sort C.Prop -> true
              | _ -> false 
            in
-           if not (Ref.eq ref1 ref2) then 
+           (* if not (Ref.eq ref1 ref2) then 
              raise (Uncertain (mk_msg metasenv subst context t1 t2))
-           else
+           else*)
              let metasenv, subst = 
               unify rdb test_eq_only metasenv subst context outtype1 outtype2 swap in
              let metasenv, subst =