diff options
Diffstat (limited to 'src/Reflection/InputSyntax.v')
| -rw-r--r-- | src/Reflection/InputSyntax.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Reflection/InputSyntax.v b/src/Reflection/InputSyntax.v index 7a89a22d3..dd9cab21d 100644 --- a/src/Reflection/InputSyntax.v +++ b/src/Reflection/InputSyntax.v @@ -70,7 +70,7 @@ Section language. Fixpoint compilef {t} (e : @exprf (interp_flat_type_gen var) t) : @Syntax.exprf base_type_code interp_base_type op var t := match e in exprf t return @Syntax.exprf _ _ _ _ t with | Const _ x => Syntax.Const x - | Var _ x => Syntax.SmartVar x + | Var _ x => Syntax.SmartVarf x | Op _ _ op args => Syntax.Op op (@compilef _ args) | LetIn _ ex _ eC => Syntax.LetIn (@compilef _ ex) (fun x => @compilef _ (eC x)) | Pair _ ex _ ey => Syntax.Pair (@compilef _ ex) (@compilef _ ey) @@ -98,7 +98,7 @@ Section language. | _ => reflexivity | _ => progress unfold LetIn.Let_In | _ => progress simpl in * - | _ => rewrite interpf_SmartVar + | _ => rewrite interpf_SmartVarf | _ => rewrite <- surjective_pairing | _ => progress rewrite_hyp * | [ |- context[let (x, y) := ?v in _] ] |