From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 24 Mar 2010 17:33:09 +0000 (+0000)
Subject: Equality has one right parameter and thus it's elimination principle has two
X-Git-Tag: make_still_working~2969
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d3d800c2489ea484c5e9891f494ca8b07a681c15;p=helm.git

Equality has one right parameter and thus it's elimination principle has two
arguments to be protected by the scope, not 1. Why did I put one long ago in
place of 2? Maybe we were working on the old library where rewriting was non
dependent?

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>
---

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 675681540..019aac2f1 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -541,7 +541,7 @@ let rewrite_tac ~dir ~what:(_,_,what) ~where status =
    | `RightToLeft -> "eq" ^ suffix
  in
   block_tac
-   [ select_tac ~where ~job:(`Substexpand 1) true;
+   [ select_tac ~where ~job:(`Substexpand 2) true;
      exact_tac
       ("",0,
        Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list (Ast.Implicit `JustOne) 5@