Coq Call 2021 07 07

• July 7th 2021, 4pm-5pm Paris Time
• https://rdv2.rendez-vous.renater.fr/coq-call

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!