diff --git a/Interpreters_template.v b/Interpreters_template.v index 5ed4380..d289bf9 100644 --- a/Interpreters_template.v +++ b/Interpreters_template.v @@ -249,6 +249,7 @@ Example factorial_ugly := * them from our examples. *) Coercion Const : nat >-> arith. Coercion Var : var >-> arith. +Declare Scope arith_scope. Infix "+" := Plus : arith_scope. Infix "-" := Minus : arith_scope. Infix "*" := Times : arith_scope.