diff options
Diffstat (limited to 'src/Experiments/NewPipeline/Language.v')
| -rw-r--r-- | src/Experiments/NewPipeline/Language.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v index 872224318..18546f54a 100644 --- a/src/Experiments/NewPipeline/Language.v +++ b/src/Experiments/NewPipeline/Language.v @@ -1245,6 +1245,8 @@ Module Compilers. Notation "x || y" := (#Z_lor @ x @ y)%expr : expr_scope. Notation "x 'mod' y" := (#Z_modulo @ x @ y)%expr : expr_scope. Notation "- x" := (#Z_opp @ x)%expr : expr_scope. + Global Arguments interp _ !_. + Global Arguments gen_interp _ _ !_. End Notations. End ident. Export ident.Notations. |