Skip to content

Fix duplicate clear warning from occurrence switch

Tej Chajed requested to merge tchajed/iris-coq:fix-duplicate-clear into master

Looks like this is the way to signal clearing a term: https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#abbreviations.

Merge request reports