• Robbert Krebbers's avatar
    Make type class inference for inG less eager. · a0348d7c
    Robbert Krebbers authored
    This way, it won't pick arbitrary (and possibly wrong!) inG instances
    when multiple ones are available. We achieve this by declaring:
    
      Hint Mode inG - - +
    
    So that type class inference only succeeds when the type of the ghost
    variable does not include any evars.
    
    This required me to make some minor changes throughout the whole
    development making some types explicit.
    a0348d7c
Name
Last commit
Last update
algebra Loading commit data...
benchmark Loading commit data...
docs Loading commit data...
heap_lang Loading commit data...
prelude Loading commit data...
program_logic Loading commit data...
proofmode Loading commit data...
tests Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
CHANGELOG.md Loading commit data...
LICENSE Loading commit data...
Makefile Loading commit data...
ProofMode.md Loading commit data...
README.md Loading commit data...
_CoqProject Loading commit data...
naming.txt Loading commit data...