aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-06-26 12:50:46 +0200
committerPierre-Marie Pédrot2020-06-29 15:20:35 +0200
commitd28af587b9848c6155c7eae482591836f0fbc68f (patch)
treef485f9cd2c05bd05d2b02c832fe732f1419004e0 /kernel/nativecode.ml
parentf34dcb97406611704c93970ea623d6a8587e5ba8 (diff)
Move the FailError exception from Refiner to Tacticals.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions