From d6e363dc419f021c96606e44642784208eafe0b4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 27 Jul 2018 11:30:45 -0400 Subject: Set arguments of ident.{gen_,}interp --- src/Experiments/NewPipeline/Language.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src') 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. -- cgit v1.2.3