Skip to content
Snippets Groups Projects

Workaround to avoid `injection` from unfolding equalities on `dom`

Merged Robbert Krebbers requested to merge robbert/injection_gset_dom into master
All threads resolved!
3 files
+ 30
2
Compare changes
  • Side-by-side
  • Inline
Files
3
+ 6
0
@@ -70,3 +70,9 @@ Failed to progress.
============================
bool_decide (∅ ⊆ {[1; 2; 3]}) = true
The command has indeed failed with message:
Nothing to inject.
The command has indeed failed with message:
Nothing to inject.
The command has indeed failed with message:
Failed to progress.
Loading