aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/goal.mli
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-07-10 11:12:55 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-07-10 11:12:55 +0200
commitf796ad268922e167e2156de0b5beef4eeb001700 (patch)
treeff5e1f830413739200707cae5daff5bf82f10004 /proofs/goal.mli
parenta4909dd5f8d5df773a361a7cbacefc392b7cfebd (diff)
parent0801250ff9aec71a2ccc2e0227d8706e1fbac6be (diff)
Merge PR #8025: Fix rst syntax for `quote ident {ident}`
Diffstat (limited to 'proofs/goal.mli')
0 files changed, 0 insertions, 0 deletions