diff options
Diffstat (limited to 'src/Rewriter.v')
-rw-r--r-- | src/Rewriter.v | 4 |
1 files changed, 2 insertions, 2 deletions
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. |