Merge branch 'robbert/iInduction_name_IH' into 'master'
Use IH names from Coq intro pattern in `iInduction`. Closes #574 See merge request iris/iris!1063
No related branches found
No related tags found
Showing
- CHANGELOG.md 4 additions, 0 deletionsCHANGELOG.md
- docs/proof_mode.md 15 additions, 7 deletionsdocs/proof_mode.md
- iris/base_logic/lib/later_credits.v 1 addition, 1 deletioniris/base_logic/lib/later_credits.v
- iris/bi/lib/relations.v 4 additions, 4 deletionsiris/bi/lib/relations.v
- iris/program_logic/lifting.v 1 addition, 1 deletioniris/program_logic/lifting.v
- iris/program_logic/total_adequacy.v 1 addition, 1 deletioniris/program_logic/total_adequacy.v
- iris/program_logic/total_lifting.v 1 addition, 1 deletioniris/program_logic/total_lifting.v
- iris/program_logic/weakestpre.v 1 addition, 1 deletioniris/program_logic/weakestpre.v
- iris/proofmode/ltac_tactics.v 55 additions, 16 deletionsiris/proofmode/ltac_tactics.v
- iris/proofmode/string_ident.v 43 additions, 9 deletionsiris/proofmode/string_ident.v
- iris_heap_lang/derived_laws.v 1 addition, 1 deletioniris_heap_lang/derived_laws.v
- iris_heap_lang/lib/array.v 5 additions, 5 deletionsiris_heap_lang/lib/array.v
- iris_heap_lang/primitive_laws.v 2 additions, 2 deletionsiris_heap_lang/primitive_laws.v
- tests/heap_lang.v 3 additions, 3 deletionstests/heap_lang.v
- tests/list_reverse.v 1 addition, 1 deletiontests/list_reverse.v
- tests/proofmode.ref 28 additions, 4 deletionstests/proofmode.ref
- tests/proofmode.v 69 additions, 11 deletionstests/proofmode.v
- tests/tree_sum.v 3 additions, 3 deletionstests/tree_sum.v
Loading
Please register or sign in to comment