aboutsummaryrefslogtreecommitdiffhomepage
path: root/config
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-03-30 22:15:02 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-04-01 22:46:17 +0200
commit8581e1a977518c354eb06820d3513238412af7de (patch)
tree8cfab4b9bab3600f6a1b9043e65d57073f79fb40 /config
parent226bf474155092f41cbb0d3e47143ac221947342 (diff)
Accomodating #4166 (providing "Require Import OmegaTactic" as a
replacement for 8.4's "Require Omega").
Diffstat (limited to 'config')
0 files changed, 0 insertions, 0 deletions