let sigma f l = Context.sigma s.current f l