Coq Call 2021 07 07 - coq/coq GitHub Wiki

Topics

  • #14598 and #14606:
    1. replacing encoding of projections as applications in constr_expr and glob_term? (#6651 reloaded)
    2. continuing allowing using r.(f) when f is not a projection (as in O.(S) for S O)?
    3. primitive projections: allowing both App(Const f, args) (concrete syntax f args, not necessarily fully applied) and Proj(f, c) (concrete syntax c.(f)) to coexist in the kernel, with App(Const f, params@c::extraargs) unfolding to App(Proj(f, c), extraargs)?
    4. non-primitive projections: continuing treating CApp(CRef(Const f), params@c::extraargs) (i.e. the former CApp((None,CRef f), params@c::extraargs) and CApp(CProj(f, params, c), extraargs) (i.e. the former CApp((Some n,CRef f), params@c::extraargs) as synonymous, and propagating this synonymy to GProj/GApp and NProj/NApp? (Or seize the opportunity to make them different?)
    5. primitive projections: allowing the concrete syntax r.(@f params) (like for non-primitive projections) even if the params are eventually thrown away in the kernel?
    6. what implicit arguments for projections (note that the main argument can be implicit in the f args syntax but not in the r.(f) syntax)? I suggest to let both cases have different signatures of implicit arguments.
  • Instantiation of arguments by name or position
    1. #11099: ready
    2. #13443: extending (x:=t)and (n:=t) notation to instantiate also non-implicit argument by name or position?
    3. #14597: deprecation syntax (arg_3:=t)?
  • #11390: what to do with implicit arguments not surviving the end of the command Context (in contrast with Hypotheses, see also #13416 for a summary of the design of commands declaring hypotheses)? (HH)

Notes

  • 8.14: blockers still there, Emilio says they're easy to fix, basically. Some bugfixes will go in 8.14.1

  • Hugo's point 6: issues/4167 is related 1.2: adding a method declaration for constant to allow them to be printed back as projections (on a unique, specified principal/subject arguments) 1.3: that's the current situation (AFAIU) 1.4: seems like a bad idea to add this confusion (@PMP?)

To be continued on the 13th of July!