aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.ml
diff options
context:
space:
mode:
authorPierre Letouzey2015-12-04 18:39:47 +0100
committerPierre Letouzey2015-12-12 18:51:37 +0100
commitec5455d7351c05a58ae99d5a300dc8576f8c9360 (patch)
treee6a743dd1ba73d7da849d4d08374d7df81500120 /kernel/type_errors.ml
parenta4d48ce98d7ae0cf07c653ed75700ed6f182936a (diff)
Extraction: nicer implementation of Implicits
Instead of the original hacks (embedding implicits in string msg in MLexn !) we now use a proper construction MLdummy (Kimplicit (r,i)) to replace the use of the i-th argument of constant or constructor r when this argument has been declared as implicit. A new option Set/Unset Extraction SafeImplicits controls what happens when some implicits still occur after an extraction : fail in safe mode, or otherwise produce some code nonetheless. This code is probably buggish if the implicits are actually used to do anything relevant (match, function call, etc), but it might also be fine if the implicits are just passed along. And anyway, this unsafe mode could help figure what's going on. Note: the MLdummy now expected a kill_reason, just as Tdummy. These kill_reason are now Ktype, Kprop (formerly Kother) and Kimplicit. Some minor refactoring on the fly.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions