Merge branch 'alt_ctx_refines' into 'master'
Alternative definition of contextual refinement See merge request !5
No related branches found
No related tags found
Showing
- _CoqProject 2 additions, 0 deletions_CoqProject
- theories/logic/compatibility.v 65 additions, 0 deletionstheories/logic/compatibility.v
- theories/prelude/lang_facts.v 197 additions, 0 deletionstheories/prelude/lang_facts.v
- theories/typing/contextual_refinement.v 29 additions, 28 deletionstheories/typing/contextual_refinement.v
- theories/typing/contextual_refinement_alt.v 148 additions, 0 deletionstheories/typing/contextual_refinement_alt.v
- theories/typing/fundamental.v 33 additions, 21 deletionstheories/typing/fundamental.v
- theories/typing/interp.v 29 additions, 0 deletionstheories/typing/interp.v
- theories/typing/soundness.v 12 additions, 7 deletionstheories/typing/soundness.v
- theories/typing/types.v 16 additions, 10 deletionstheories/typing/types.v
Loading
Please register or sign in to comment