aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/nanoPG.ml
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2018-06-04 14:47:36 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2018-06-04 14:47:36 +0200
commit0a829c6ac232b0ea786716709b0d01c707548089 (patch)
treec5279bc173449f1e83a884c5e74da773c2c64bc6 /ide/nanoPG.ml
parentd5de86d0606e1c3dc88c48bf3ec2e820b5485d8f (diff)
parent15e43996b342f2eddf0c6c0bd4166e757589337e (diff)
Merge PR #7199: Fixes #7195: missing freshness condition in Ltac pattern-matching names
Diffstat (limited to 'ide/nanoPG.ml')
0 files changed, 0 insertions, 0 deletions