- GREAT: when unifying ?1 : Type[i] with ?2: Type[j] the unifier

  randomly tried to instantiate ?1 with ?2 even when j > i, yielding to
  an unification error later on. In turn, this created that horrible
  behaviour of rewriting that failed if you did not pass enough types
  to the lemma.
- in rewriting the argument is now automatically saturated

These two fixes together allow most of the time to write simply >f as we
did in the old system.

diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml
index 5500abcbf189ee44073a288ac59049410b4cd083..a74172ca0e463b3e449f4fc970f877c677afc677 100644 (file)
--- a/matita/components/ng_refiner/nCicUnification.ml
+++ b/matita/components/ng_refiner/nCicUnification.ml
@@ -382,8 +382,8 @@ let rec instantiate rdb test_eq_only metasenv subst context n lc t swap =
        | _ ->
         let lty = NCicSubstitution.subst_meta lc ty in
         pp (lazy ("On the types: " ^
-          ppterm ~metasenv ~subst ~context lty ^ "=<=" ^
-          ppterm ~metasenv ~subst ~context ty_t)); 
+          ppterm ~metasenv ~subst ~context ty_t ^ "=<=" ^
+          ppterm ~metasenv ~subst ~context lty)); 
         let metasenv, subst = 
           unify rdb false metasenv subst context ty_t lty false
         in
@@ -559,6 +559,17 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
               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), 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 lc tyn in
+          let tym = NCicSubstitution.subst_meta lc tym in
+           match tyn,tym with
+              NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
+               NCicEnvironment.universe_lt u1 u2
+            | _,_ -> false ->
+          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
@@ -866,7 +877,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 swap =
          | KeepReducing _ -> assert false
          | KeepReducingThis _ ->
             assert (not (norm1 && norm2));
-           unif_machines metasenv subst (small_delta_step ~subst m1 m2)
+            unif_machines metasenv subst (small_delta_step ~subst m1 m2)
          | UnificationFailure _ | Uncertain _ when (not (norm1 && norm2))
            -> unif_machines metasenv subst (small_delta_step ~subst m1 m2)
          | UnificationFailure msg

diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml
index 15e77f0940417eb6c5368e99798434706c12ea15..9c9f0d73a18276d3bb495783a34ddd29e4a555fa 100644 (file)
--- a/matita/components/ng_tactics/nTactics.ml
+++ b/matita/components/ng_tactics/nTactics.ml
@@ -542,6 +542,7 @@ let rewrite_tac ~dir ~what:(_,_,what) ~where status =
      `LeftToRight -> "eq" ^ suffix ^ "_r"
    | `RightToLeft -> "eq" ^ suffix
  in
+ let what = Ast.Appl [what; Ast.Implicit `Vector] in
   block_tac
    [ select_tac ~where ~job:(`Substexpand 2) true;
      exact_tac