Skip to content

Silence some warnings

Kimaya Bedarkar requested to merge kbedarka/rt-proofs:silencewarnings into master
  • Currently we get two types of warnings during the compilation of Prosa
  • One is to do with the use of deprecated tactics in elf/rta/bounded_pi.v. If we want to silence these warnings then we lose compatibility with Mathcomp 1.16
  • The other is due to obligation tactics declared in behavior/schedule.v and behavior/ready.v
  • Declaring this tactic does not actually solve any goals. However, it has the effect that the default Coq obligation tactic is not used and hence introsing of some variables is prevented.
  • Currently I added the tactic back in local scope to the files where it is needed since otherwise it is not possible to generate proofs that are compatible with mangle names.
  • However, maybe there is a better way of doing it.

Merge request reports