1. Paweł Wieczorek
  2. MgrCoq

Commits

Show all
Author Commit Message Date Builds
Paweł Wieczorek
Removed tag release_2011_11_10
Paweł Wieczorek
Added tag release_2011_11_10 for changeset 3191740282de
Paweł Wieczorek
Paweł Wieczorek
Paweł Wieczorek
Code: new extracted evaluator
Paweł Wieczorek
Model.Valid: a lot of fixes ;]
Paweł Wieczorek
Model.Valid: added helper FUN_SB
Paweł Wieczorek
Model.Valid: added Helper_FUN3
Paweł Wieczorek
Model.Valid: added tactic build_valenv
Paweł Wieczorek
Syntax.System: fixes...
Paweł Wieczorek
Added tag coq_internal_error for changeset 87091870edf1
Paweł Wieczorek
Model.Valid: removed extensionality from Soundness theorem
Paweł Wieczorek
Model.Valid: Partial script for EQ_SBAPP
Paweł Wieczorek
Model.Valid: removed Beta rule from Soundness thoerem
Paweł Wieczorek
Model.Valid: removed SB_EXT rule from Model soundness theorem
Paweł Wieczorek
Model.Valid: removed SB rule from Soundness_theorem
Paweł Wieczorek
Paweł Wieczorek
Model.Valid: Beta-reduction, Extensionality
Paweł Wieczorek
Model.Valid: Helper for SB_EXT
Paweł Wieczorek
Model.Valid: Helper for SB
Paweł Wieczorek
Fixes in system.
Paweł Wieczorek
Model.Valid: a lot of rules with admits
Paweł Wieczorek
Syntax.System: a lot of fixes
Paweł Wieczorek
Model.Valid: EQ_CONG_SB
Paweł Wieczorek
Model.Valid: removed SB_F from theorem
Paweł Wieczorek
Model.Valid: SB_F as Helper
Paweł Wieczorek
Model.Valid: another helper EQ_TP_VALID
Paweł Wieczorek
Model.Valid: EQ_SB_SYM and EQ_SB_TRANS as helpers
Paweł Wieczorek
Syntax.System: fixes...
Paweł Wieczorek
Model.Valid: EQ_CONG_FUN_E
  1. Prev
  2. Next