Expression do no longer have a dependent type holding the set of
allowed free variables. Instead, closedness of expressions is enforced wherever it is needed with the [Closed] typeclass.
Showing
- _CoqProject 0 additions, 1 deletion_CoqProject
- derived.v 3 additions, 3 deletionsderived.v
- lang.v 120 additions, 243 deletionslang.v
- lifting.v 5 additions, 4 deletionslifting.v
- notation.v 0 additions, 1 deletionnotation.v
- races.v 4 additions, 4 deletionsraces.v
- tactics.v 2 additions, 3 deletionstactics.v
- wp_tactics.v 4 additions, 5 deletionswp_tactics.v
Loading
Please register or sign in to comment