diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-07 14:56:43 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-07 14:56:53 -0700 |
| commit | 054752ccf0b80bc413e70202a823fd034db6ea6b (patch) | |
| tree | afb7424ab413cb087aa35d3bf65f0a65564b6906 | |
| parent | c8a157cb0786acbd163eb3a56e201110782ef527 (diff) | |
Fixes for Coq 8.4
| -rw-r--r-- | src/Reflection/CommonSubexpressionElimination.v | 2 | ||||
| -rw-r--r-- | src/Reflection/TestCase.v | 1 |
2 files changed, 2 insertions, 1 deletions
diff --git a/src/Reflection/CommonSubexpressionElimination.v b/src/Reflection/CommonSubexpressionElimination.v index 3c5e1cbd7..1f44f333d 100644 --- a/src/Reflection/CommonSubexpressionElimination.v +++ b/src/Reflection/CommonSubexpressionElimination.v @@ -52,7 +52,7 @@ Section symbolic. Local Notation flat_type := (flat_type base_type_code). Local Notation type := (type base_type_code). Let Tbase := @Tbase base_type_code. - Local Coercion Tbase : base_type_code >-> flat_type. + Local Coercion Tbase : base_type_code >-> Syntax.flat_type. Local Notation interp_type := (interp_type interp_base_type). Local Notation interp_flat_type := (interp_flat_type_gen interp_base_type). Local Notation exprf := (@exprf base_type_code interp_base_type op). diff --git a/src/Reflection/TestCase.v b/src/Reflection/TestCase.v index fd60e7906..05b3dab4b 100644 --- a/src/Reflection/TestCase.v +++ b/src/Reflection/TestCase.v @@ -9,6 +9,7 @@ Import ReifyDebugNotations. Local Set Boolean Equality Schemes. Local Set Decidable Equality Schemes. +Scheme Equality for nat. Inductive base_type := Tnat. Definition interp_base_type (v : base_type) : Type := match v with |