Commits · ede904dc71304b8be1b989308807766c7049919e · Paolo G. Giarrusso / iris

Sep 03, 2024
- Add changelog · ede904dc
  Janggun Lee authored 6 months ago
  
  ede904dc
Aug 29, 2024
- Add some `discrete_fun_singleton` helpers. · f6ab4763
  Janggun Lee authored 6 months ago
  
  f6ab4763
- Add changelog. · 197d868c
  Janggun Lee authored 6 months ago
  
  197d868c
Aug 28, 2024
- Apply review comments and add `discrete_fun_updateP'`. · 3f996021
  Janggun Lee authored 6 months ago
  
  3f996021
Aug 23, 2024

Add `discrete_function_update{P}`. · fe3f50a8

Janggun Lee authored 6 months ago

* `updateP` requires `Finite A`, similar to `discrete_fun_included_spec`.

* `update` has no such side conditions.

fe3f50a8

Aug 20, 2024
- Merge branch 'janno/iframe-cbv' into 'master' · 657b34ad
  Robbert Krebbers authored 6 months ago
  
  iFrame: Do not call `cbv` on user terms in contexts See merge request iris/iris!1042
  657b34ad
- More documentation. · 13aa09a8
  Robbert Krebbers authored 6 months ago
  
  13aa09a8
- Documentation. · 77fd4c86
  Robbert Krebbers authored 6 months ago
  
  77fd4c86
- Turn two more uses of `cbv` into `lazy` that involve user terms. · 3e55344c
  Robbert Krebbers authored 6 months ago
  
  3e55344c
- iFrame: Do not call `cbv` on user terms in contexts · 45b4a2d2
  Jan-Oliver Kaiser authored 11 months ago
  
  45b4a2d2
Aug 19, 2024
- Merge branch 'robbert/iInduction_name_IH' into 'master' · f11d6aab
  Ralf Jung authored 6 months ago
  
  Use IH names from Coq intro pattern in `iInduction`. Closes #574 See merge request iris/iris!1063
  f11d6aab
- CHANGELOG. · 37b578f5
  Robbert Krebbers authored 6 months ago
  
  37b578f5
- Fix error in `iInduction` docs. · 4e7365ae
  Robbert Krebbers authored 6 months ago
  
  4e7365ae
- Move Ltac2 `compute` back into `StringToIdent` module. · 9e0cc537
  Robbert Krebbers authored 6 months ago
  
  9e0cc537
- Some tests for legacy syntax and error messages. · 44508871
  Robbert Krebbers authored 7 months ago
  
  44508871
- Better version of `ident_to_string`, also by @lepigre . · f4db0245
  Robbert Krebbers authored 7 months ago
  
  f4db0245
- Update code to use new `iInduction` syntax. · 9fdd6724
  Robbert Krebbers authored 7 months ago
  
  9fdd6724
- Update documentation. · 37fdb619
  Robbert Krebbers authored 7 months ago
  
  37fdb619
- Add version of `iInduction` that allows to name IHs in the Coq intro pattern. · 8d2dfa63
  Robbert Krebbers authored 7 months ago
  
  8d2dfa63
- Add `ident_to_string`, based on code by @lepigre . · 76a6808a
  Robbert Krebbers authored 7 months ago
  
  76a6808a
- Some coding tweaks to the internals of `string_to_ident`. · c7a48ded
  Robbert Krebbers authored 7 months ago
  
  c7a48ded
- Merge branch 'robbert/iUnfold' into 'master' · e4bc73af
  Ralf Jung authored 6 months ago
  
  Add `iUnfold` tactic. Closes #573 See merge request iris/iris!1066
  e4bc73af
Aug 17, 2024

Merge branch 'tc-match-hints' into 'master' · 8a98d00a

Ralf Jung authored 6 months ago

Add instances for `match` on `Persistent`, `Affine`, `Absorbing`, `Plain`, `Timeless`

Closes #479

See merge request iris/iris!1068

8a98d00a

Aug 16, 2024
- hints -> instances · 593e7cf7
  Sanjit Bhat authored 6 months ago
  
  Verified
  
  593e7cf7
- cleanup/move tests and improve changelog · 1fb80e30
  Sanjit Bhat authored 6 months ago
  
  Verified
  
  1fb80e30
- Bump std++ (length_X). · 8890e30a
  Robbert Krebbers authored 6 months ago
  
  8890e30a
- Merge branch 'robbert/local_instance_pragma' into 'master' · f9526b3a
  Ralf Jung authored 6 months ago
  
  Use `#[local] field ::` to make `inG` instances local. Closes #561 See merge request iris/iris!1065
  f9526b3a
- Merge branch 'rm-old-file' into 'master' · 34183299
  Ralf Jung authored 6 months ago
  
  Remove old ProofMode.md file See merge request iris/iris!1069
  34183299
- Merge branch 'robbert/heaplang_pointsto_seal' into 'master' · 21f62ebd
  Robbert Krebbers authored 6 months ago
  
  Seal heap_lang `pointsto`. Closes #549 See merge request iris/iris!1067
  21f62ebd
- CHANGELOG. · 59c6fee1
  Robbert Krebbers authored 7 months ago
  
  59c6fee1
- Seal heap_lang `pointsto`. · 91072969
  Robbert Krebbers authored 7 months ago
  
  This closes #549.
  91072969
- Also update proof_guide. · 2353a354
  Robbert Krebbers authored 6 months ago
  
  2353a354
Aug 15, 2024
- rm old ProofMode.md file · d75eb7f0
  Sanjit Bhat authored 7 months ago
  
  Verified
  
  d75eb7f0
- update changelog and add tests · f112bfcd
  Sanjit Bhat authored 7 months ago
  
  Verified
  
  f112bfcd
- for derived connectives, add TC hints to destruct matches · 582db478
  Sanjit Bhat authored 7 months ago
  
  Verified
  
  582db478
- Add docs and CHANGELOG. · 00fef20c
  Robbert Krebbers authored 7 months ago
  
  00fef20c
- Add tests. · 64eab238
  Robbert Krebbers authored 7 months ago
  
  64eab238
- Add `iUnfold` tactic. · 41f7fa19
  Robbert Krebbers authored 7 months ago
  
  This closes #573.
  41f7fa19
- Use `#[local] field ::` to make `inG` instances local. · ee9b400b
  Robbert Krebbers authored 7 months ago
  
  This closes #561.
  ee9b400b
- Merge branch 'robbert/iDestruct_exist_fail' into 'master' · 2015eb34
  Robbert Krebbers authored 7 months ago
  
  Fix freshness error message in `iDestruct` for existentials. See merge request iris/iris!1064
  2015eb34