Merge branch 'jh/infinite_function_cmra' into 'master'
Remove the domain finiteness hypothesis for the function CMRA, and put cmra_extend in Type. See merge request FP/iris-coq!118
No related branches found
No related tags found
Showing
- theories/algebra/cmra.v 29 additions, 28 deletionstheories/algebra/cmra.v
- theories/algebra/csum.v 4 additions, 4 deletionstheories/algebra/csum.v
- theories/algebra/excl.v 1 addition, 1 deletiontheories/algebra/excl.v
- theories/algebra/functions.v 2 additions, 2 deletionstheories/algebra/functions.v
- theories/algebra/gmap.v 10 additions, 24 deletionstheories/algebra/gmap.v
- theories/algebra/list.v 7 additions, 5 deletionstheories/algebra/list.v
- theories/base_logic/primitive.v 3 additions, 2 deletionstheories/base_logic/primitive.v
Loading
Please register or sign in to comment