Skip to content
GitLab

Fix `forall` parsing.

Merged Gregory Malecha requested to merge gmalecha/iris:fix-forall-parsing into master
  • This fixes a bug in the declaration of the forall notation which was preventing Coq from recognizing the primitive Gallina forall.
  • The solution is to re-introduce the forall notation at type scope. This overrides the primitive notation.

New tests at the bottom of the proofmode_ascii file.