aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorMatthieu Sozeau2014-09-09 22:39:15 +0200
committerMatthieu Sozeau2014-09-09 22:53:59 +0200
commit0dd3f0d34873dcd126be8ec48724a310214f38ac (patch)
treeccb5c83cba1db777681e8ecb7251dc486b3f2044 /dev
parente365fb8ffbbc62352a725de13cbf864b3fbb3840 (diff)
- Fix printing and parsing of primitive projections, including the Set
Printing All cases (bug #3597). - Fix Ltac matching with primitive projections (bug #3598). - Spotted a problem with printing of constants with maximally implicit arguments due to strange "compatibility" interpretation of Arguments [X] as Arguments {X} but didn't fix it entirely yet (might cause incompatibilities).
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions