search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
488 stars 87 forks source link

Ssreflect's under tactic #584

Open proux01 opened 3 years ago

proux01 commented 3 years ago

The new ssreflect's under tactic https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html?highlight=under#rewriting-under-binders lacks some syntax highlighting and indentation support.

cpitclaudel commented 3 years ago

For these many highlighting issues, I would suggest opening a single meta-issue with a checklist in there. It will reduce noise and make it easier to track progress.