Commits · 7607c53e9132d2fe3adb7520909573bcfae56098 · Pierre Roux / Iris

Jul 25, 2021
- Similar tests for `curry`. · 7607c53e
  Robbert Krebbers authored 3 years ago
  
  7607c53e
- Tests for non-expansive of uncurry. · fdf4deed
  Robbert Krebbers authored 3 years ago
  
  fdf4deed
Jun 19, 2021

Include workaround for Coq bug #14441, and drop now-failing test for that Coq
bug.

5f5c02af

Jun 18, 2021
- don't test 'Hint Mode Equiv !'; wait for Coq fix instead · bd9d16c9
  Ralf Jung authored 3 years ago
  
  bd9d16c9
- Revise comments on tests · a02c29ac
  Paolo G. Giarrusso authored 3 years ago
  
  a02c29ac
- Add suggested test · ac3ddfda
  Paolo G. Giarrusso authored 3 years ago
  
  ac3ddfda
Jun 02, 2021
- rename global singletons to 'GS' suffix · 1118f70f
  Ralf Jung authored 3 years ago
  
  1118f70f
Jan 19, 2021
- Rename `ofeT`→`ofe`, `cmraT`→`cmra`, and `ucmraT`→`ucmra`. · cc9470e0
  Robbert Krebbers authored 4 years ago
  
  cc9470e0
Jan 07, 2021
- Qualify all instances with Local or Global · 143d0af3
  Ralf Jung authored 4 years ago
  
  Done with a script by Tej; see iris/iris!609 for details.
  143d0af3
Oct 21, 2020
- move gmap_view_check to tests/algebra.v · 1978542d
  Ralf Jung authored 4 years ago
  
  1978542d
Mar 18, 2020
- add regression test · 042cbada
  Ralf Jung authored 5 years ago
  
  042cbada
Mar 12, 2020
- Close issue #299: `leibnizO` finds convoluted proof for definitions · f2eabe78
  Robbert Krebbers authored 5 years ago
  
  f2eabe78
Sep 19, 2019
- Also rename `iPreProp` into `iPrePropO`. · a3766213
  Robbert Krebbers authored 5 years ago
  
  a3766213
- Let `iProp` refer to `uPred ...`, so not the canonical structure bundle. · 601625fb
  Robbert Krebbers authored 5 years ago
  
  601625fb
May 20, 2019
- Fix compilation with Coq master. · eb3117bd
  Robbert Krebbers authored 5 years ago
  
  eb3117bd
May 16, 2019
- Add (redundant?) test · c75c0489
  Paolo G. Giarrusso authored 5 years ago
  
  Never used `Declare Instance`.
  c75c0489
Mar 05, 2019
- use ! when possible to avoid overzealous generalization · da93f357
  Ralf Jung authored 6 years ago
  
  da93f357
Oct 22, 2018
- Use unicide ∧ and ∃. · 49b5dd50
  Robbert Krebbers authored 6 years ago
  
  49b5dd50
Jun 25, 2018
- bump std++; test that we don't break setoid_rewrite · 42f0842f
  Ralf Jung authored 6 years ago
  
  42f0842f
May 17, 2018

move test suite out of theories/ so it does not get installed; also check... · 859871ab

Ralf Jung authored 6 years ago

move test suite out of theories/ so it does not get installed; also check output of test suite so that we can test printing

859871ab

Oct 09, 2017
- update std++; add test for solve_proper · 93eb2615
  Ralf Jung authored 7 years ago
  
  93eb2615