diff options
author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-07-10 11:12:55 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-07-10 11:12:55 +0200 |
commit | f796ad268922e167e2156de0b5beef4eeb001700 (patch) | |
tree | ff5e1f830413739200707cae5daff5bf82f10004 /proofs/goal.mli | |
parent | a4909dd5f8d5df773a361a7cbacefc392b7cfebd (diff) | |
parent | 0801250ff9aec71a2ccc2e0227d8706e1fbac6be (diff) |
Merge PR #8025: Fix rst syntax for `quote ident {ident}`
Diffstat (limited to 'proofs/goal.mli')
0 files changed, 0 insertions, 0 deletions