Merge pull request #1079 from silene/remove-vm

Remove useless calls to Eval vm_compute.
MetaCoq · Jun 12, 2024 · 7f820b6 · 7f820b6
2 parents 35dbb48 + 1dd3fd1
commit 7f820b6
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/test-suite/vs.v b/test-suite/vs.v
@@ -2317,13 +2317,11 @@ Definition example_myent := Entailment
   (Assertion nil nil)
   (Assertion [Equ a a] nil).
 Definition ce_example_myent := check_entailment example_myent.
-Eval vm_compute in ce_example_myent.
 
 Definition example1_myent := Entailment
   (Assertion [Equ a b] nil)
   (Assertion [Equ b a] nil).
 Definition ce_example1_myent := check_entailment example1_myent.
-Eval vm_compute in ce_example1_myent.
 
 Definition example2_myent := Entailment
   (Assertion [Equ a b; Equ b c] nil)