diff options
| author |  Jason Gross <jagro@google.com> | 2018-07-26 14:40:46 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-07-26 14:40:46 -0400 |
| commit | ca2294ffe37c8ec8f4bf027c9afd3337b10c29d5 (patch) | |
| tree | cb5f2ce9a522d9d2512b07a3c848a20206b85af7 /src/Experiments | |
| parent | 201268439584b01c1338ccf3407d929960d74a6d (diff) | |
Put == in type_scope, so that we don't need to go around opening etype_scope
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/NewPipeline/Language.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v index 1e8e9da4e..872224318 100644 --- a/src/Experiments/NewPipeline/Language.v +++ b/src/Experiments/NewPipeline/Language.v @@ -243,7 +243,7 @@ Module Compilers. Delimit Scope etype_scope with etype. Bind Scope etype_scope with type.type. Infix "->" := type.arrow : etype_scope. - Infix "==" := type.eqv : etype_scope. + Infix "==" := type.eqv : type_scope. Module base. Local Notation einterp := type.interp. Module type. |