aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Relations
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-04-10 17:04:44 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-06-16 17:30:17 +0200
commita4ff40931201f91cde79c212a9d2cc19a62b8128 (patch)
treee741a660a342c935d2cc81ef7db7f39dafa920e7 /theories/Relations
parent53e8a445177501846c75147680da03a95d5e9b5c (diff)
Protect the beautifier from change in the lexer state (typically by
calling Pcoq.parse_string, what some plugins such as coretactics, are doing, thus breaking the beautification of "Declare ML Module").
Diffstat (limited to 'theories/Relations')
0 files changed, 0 insertions, 0 deletions