diff options
author | 2018-07-10 11:12:55 +0200 | |
---|---|---|
committer | 2018-07-10 11:12:55 +0200 | |
commit | f796ad268922e167e2156de0b5beef4eeb001700 (patch) | |
tree | ff5e1f830413739200707cae5daff5bf82f10004 /pretyping/unification.mli | |
parent | a4909dd5f8d5df773a361a7cbacefc392b7cfebd (diff) | |
parent | 0801250ff9aec71a2ccc2e0227d8706e1fbac6be (diff) |
Merge PR #8025: Fix rst syntax for `quote ident {ident}`
Diffstat (limited to 'pretyping/unification.mli')
0 files changed, 0 insertions, 0 deletions