From d3d800c2489ea484c5e9891f494ca8b07a681c15 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 24 Mar 2010 17:33:09 +0000 Subject: [PATCH] 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 --- helm/software/components/ng_tactics/nTactics.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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@ -- 2.39.2