aboutsummaryrefslogtreecommitdiffstats
path: root/backend/AisAnnot.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2018-03-12 10:10:50 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2018-03-12 10:10:50 +0100
commite6308c5ec63a3a01ee33c9304e5249c6159dd1ef (patch)
treea502121771580a3840f58240e8cb6178b3269d82 /backend/AisAnnot.ml
parentb125afc697c1214cb329967b506a4a740a942e81 (diff)
downloadcompcert-kvx-e6308c5ec63a3a01ee33c9304e5249c6159dd1ef.tar.gz
compcert-kvx-e6308c5ec63a3a01ee33c9304e5249c6159dd1ef.zip
Removed deprecated lemma.
The lemma Zquot_1_r is replaced by Z.quot_1_r in coq version > 8.3. Fix 23199
Diffstat (limited to 'backend/AisAnnot.ml')
0 files changed, 0 insertions, 0 deletions