Parameterize the lifetime logic over the user mask.
By default this parameter is filed by the namespace lft_userN. The old method, hard-wiring this parameter to lft_userN, had the defect of requiring to place libraries' namespacec in it *in advance*. The weak branch has always used such a parameter.
Showing
- theories/lifetime/at_borrow.v 3 additions, 3 deletionstheories/lifetime/at_borrow.v
- theories/lifetime/frac_borrow.v 5 additions, 4 deletionstheories/lifetime/frac_borrow.v
- theories/lifetime/lifetime.v 4 additions, 4 deletionstheories/lifetime/lifetime.v
- theories/lifetime/lifetime_sig.v 17 additions, 17 deletionstheories/lifetime/lifetime_sig.v
- theories/lifetime/meta.v 3 additions, 3 deletionstheories/lifetime/meta.v
- theories/lifetime/model/accessors.v 4 additions, 4 deletionstheories/lifetime/model/accessors.v
- theories/lifetime/model/borrow.v 1 addition, 1 deletiontheories/lifetime/model/borrow.v
- theories/lifetime/model/borrow_sep.v 1 addition, 1 deletiontheories/lifetime/model/borrow_sep.v
- theories/lifetime/model/creation.v 10 additions, 11 deletionstheories/lifetime/model/creation.v
- theories/lifetime/model/definitions.v 6 additions, 5 deletionstheories/lifetime/model/definitions.v
- theories/lifetime/model/faking.v 1 addition, 1 deletiontheories/lifetime/model/faking.v
- theories/lifetime/model/primitive.v 15 additions, 15 deletionstheories/lifetime/model/primitive.v
- theories/lifetime/model/reborrow.v 1 addition, 1 deletiontheories/lifetime/model/reborrow.v
- theories/lifetime/na_borrow.v 2 additions, 2 deletionstheories/lifetime/na_borrow.v
- theories/typing/base.v 14 additions, 0 deletionstheories/typing/base.v
- theories/typing/lft_contexts.v 3 additions, 3 deletionstheories/typing/lft_contexts.v
- theories/typing/lib/arc.v 3 additions, 3 deletionstheories/typing/lib/arc.v
- theories/typing/lib/ghostcell.v 1 addition, 1 deletiontheories/typing/lib/ghostcell.v
- theories/typing/lib/rc/rc.v 7 additions, 7 deletionstheories/typing/lib/rc/rc.v
- theories/typing/lib/refcell/ref_code.v 3 additions, 3 deletionstheories/typing/lib/refcell/ref_code.v
Loading
Please register or sign in to comment