diff options
Diffstat (limited to 'src/Language.v')
-rw-r--r-- | src/Language.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Language.v b/src/Language.v index 4d4995e68..52c340d18 100644 --- a/src/Language.v +++ b/src/Language.v @@ -1401,7 +1401,7 @@ Module Compilers. | fancy.interp ?idc => let ridc := (eval cbv [to_fancy] in (to_fancy idc)) in then_tac ridc - | @gen_interp _ ?idc => then_tac idc + | @gen_interp _ _ ?idc => then_tac idc | _ => else_tac () end end. |