diff options
| author | Hugo Herbelin | 2015-03-30 22:15:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-04-01 22:46:17 +0200 |
| commit | 8581e1a977518c354eb06820d3513238412af7de (patch) | |
| tree | 8cfab4b9bab3600f6a1b9043e65d57073f79fb40 /kernel/type_errors.mli | |
| parent | 226bf474155092f41cbb0d3e47143ac221947342 (diff) | |
Accomodating #4166 (providing "Require Import OmegaTactic" as a
replacement for 8.4's "Require Omega").
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions