diff options
| author | ppedrot | 2012-10-04 11:53:19 +0000 |
|---|---|---|
| committer | ppedrot | 2012-10-04 11:53:19 +0000 |
| commit | 41abdd815f9384e197cba73ee67f2b78f89a6319 (patch) | |
| tree | 9b0d2b502e98e705529d1b244d0eaf8026f72f86 /plugins | |
| parent | 5b6582f8d47975f6f4f394cf44a1c65c799d43ff (diff) | |
Adding a nominal typing layer to Metasyntax in order to clarify
things up. Records are used instead of their equivalents as tuples.
This is maybe syntactically heavier, but this is semantically
equivalent and easier to understand.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15848 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions