diff options
| author |  Jason Gross <jagro@google.com> | 2018-07-27 11:30:45 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-07-27 11:30:45 -0400 |
| commit | d6e363dc419f021c96606e44642784208eafe0b4 (patch) | |
| tree | c42cc88bd31b7e2417f70b595cc1e4d9fc62c436 /src | |
| parent | f3eaeb4e1f9f52b5683d2ed5d6e5cf8e5827576a (diff) | |
Set arguments of ident.{gen_,}interp
Diffstat (limited to 'src')
| -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. |