summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorBrian Campbell2018-08-03 15:04:18 +0100
committerBrian Campbell2018-08-03 15:04:18 +0100
commitbaabef2bc2d39fc47ba47cd2ac5305856dd212a2 (patch)
treee4d90f0eb109b0cf4e1eff6d21073720ea9f29b4 /src
parent2cb15665392d0b87da9e0c1f43e19267f28c3a82 (diff)
Coq: use a dummy constraint when the real one is unknown
Not really what we want, but a useful placeholder because of the widespread use of ex_int.
Diffstat (limited to 'src')
0 files changed, 0 insertions, 0 deletions