From c1a5679d5b5c5ef0c07d618b4bb48451a8cb7a7a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 6 Mar 2019 02:21:41 -0500 Subject: Fix reification of interpreted idents --- src/Language.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') 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. -- cgit v1.2.3