aboutsummaryrefslogtreecommitdiff
path: root/vernac/comProgramFixpoint.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-03-29 19:42:41 +0100
committerEmilio Jesus Gallego Arias2019-03-29 19:42:41 +0100
commitae9cc11c9975cc7ced1800f6684e160bc17fb092 (patch)
tree68ce39acc517369d5e25fac9aa2d87f33fd3a4ed /vernac/comProgramFixpoint.ml
parent23d6e0619fc7a1d466bebb831a988431828da88f (diff)
parent7eba2dfda86238cb0941edfd7aafb09f566c36d8 (diff)
Merge PR #9830: [parser] initialization based on Loc.t rather than Loc.source
Reviewed-by: ejgallego Ack-by: gares
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
0 files changed, 0 insertions, 0 deletions