From 941928eb8d30345e4072ace2f79c127442fed6ee Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 31 Jan 2019 21:37:06 -0500 Subject: Remove an unused argument --- src/Rewriter.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Rewriter.v') diff --git a/src/Rewriter.v b/src/Rewriter.v index b9b57ff43..5f10869b2 100644 --- a/src/Rewriter.v +++ b/src/Rewriter.v @@ -948,7 +948,7 @@ Module Compilers. Local Notation maybe_do_again := (maybe_do_again do_again). - Definition rewrite_with_rule {t} (defaulte : expr t) e' (pf : rewrite_ruleT) + Definition rewrite_with_rule {t} e' (pf : rewrite_ruleT) : option (UnderLets (expr t)) := let 'existT p f := pf in let should_do_again := rew_should_do_again f in @@ -980,7 +980,7 @@ Module Compilers. (fun k ctx => match ctx return option (UnderLets (expr (type_of_rawexpr e))) with | e'::nil - => (pf <- nth_error rews k; rewrite_with_rule defaulte e' pf)%option + => (pf <- nth_error rews k; rewrite_with_rule e' pf)%option | _ => None end);;; (UnderLets.Base defaulte))%option. -- cgit v1.2.3