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

[helm.git] / matita / components / ng_tactics / nTactics.ml

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