aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/C2C.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2022-12-22 16:20:15 +0100
committerGitHub <noreply@github.com>2022-12-22 16:20:15 +0100
commitfc79b13a30f124e9ac2d658773c395e0a74e2d1e (patch)
treef81eb0494f192d3abe40c7ce50a4bf77c9596766 /cfrontend/C2C.ml
parent8d21a7fa245637b684ddb4c12f4bfa6295569fb6 (diff)
downloadcompcert-fc79b13a30f124e9ac2d658773c395e0a74e2d1e.tar.gz
compcert-fc79b13a30f124e9ac2d658773c395e0a74e2d1e.zip
Use `exfalso` instead of `elimtype False` (#470)
Adapt w.r.t. coq/coq#16904.
Diffstat (limited to 'cfrontend/C2C.ml')
0 files changed, 0 insertions, 0 deletions