From bc044646afa3551066afbc584671a76b86b38855 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 29 Nov 2010 12:50:18 +0000 Subject: [PATCH] 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. --- helm/software/components/ng_tactics/nTactics.ml | 1 + 1 file changed, 1 insertion(+) 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 -- 2.39.2