diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-03-22 13:52:42 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-03-23 12:45:19 -0400 |
| commit | 2044c675924d2f63633cbac3c8b5d742526ba4be (patch) | |
| tree | 7c05af104dad9f441f96194e9cad5718cd2a6e49 /src | |
| parent | 7fd351a24f75174b9090edbb2e8933500bd65abb (diff) | |
Make the ERROR definition opaque to vm_compute
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index e882b3f0e..ca7340fd5 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -5313,8 +5313,7 @@ Module Compilers. | Abs (s : type) (n : positive) {d} (f : expr d) : expr (s -> d). End Flat. - Definition ERROR {T} (v : T) : T := v. - Global Opaque ERROR. + Definition ERROR {T} (v : T) : T. exact v. Qed. Fixpoint to_flat' {t} (e : @expr (fun _ => PositiveMap.key) t) (cur_idx : PositiveMap.key) |