From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 29 Nov 2010 12:50:18 +0000 (+0000)
Subject: Back-porting from new Matita:
X-Git-Tag: make_still_working~2680
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bc044646afa3551066afbc584671a76b86b38855;p=helm.git

Back-porting from new Matita:

- 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/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 895eec2d2..86b42f661 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/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