From: Claudio Sacerdoti Coen 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