Skip to content

tmMkInductive should not be used in a tactic#1130

Open
yforster wants to merge 1 commit intoMetaCoq:coq-8.20from yforster:tmMkInductive-in-tactic
+7-4

Commits