Skip to content

rm problematic variables under beta-redexes and evars for evar instantiation#19822

Closed
Tragicus wants to merge 3 commits into
rocq-prover:masterfrom
Tragicus:evd-inst
Closed

rm problematic variables under beta-redexes and evars for evar instantiation#19822
Tragicus wants to merge 3 commits into
rocq-prover:masterfrom
Tragicus:evd-inst

shelve new variable when instantiating old shelved variable with the …

bbabba0
Select commit
Loading
Failed to load commit list.

Workflow runs completed with no jobs