diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-12 18:34:01 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-12 18:34:01 -0400 |
| commit | 478b56dd5d8f4dd45e0d8a5474482176da35dcc8 (patch) | |
| tree | e7ca63423d4aa6a6031a3cf3361ca0ebe177ccbd /src/Compilers/Z/ArithmeticSimplifierWf.v | |
| parent | 951939fd55d7ad8178ac095189bc8399f2124640 (diff) | |
Add reflective compose, notation for Z.Syntax.{Expr,Interp}
Diffstat (limited to 'src/Compilers/Z/ArithmeticSimplifierWf.v')
| -rw-r--r-- | src/Compilers/Z/ArithmeticSimplifierWf.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/Compilers/Z/ArithmeticSimplifierWf.v b/src/Compilers/Z/ArithmeticSimplifierWf.v index 33f3c3335..ff690688a 100644 --- a/src/Compilers/Z/ArithmeticSimplifierWf.v +++ b/src/Compilers/Z/ArithmeticSimplifierWf.v @@ -21,7 +21,6 @@ Require Import Crypto.Util.HProp. Local Notation exprf := (@exprf base_type op). Local Notation expr := (@expr base_type op). -Local Notation Expr := (@Expr base_type op). Local Notation wff := (@wff base_type op). Local Notation Wf := (@Wf base_type op). |