Use lia instead of omega in examples

plclub · Jun 25, 2024 · c0e79f0 · c0e79f0
1 parent c0d5a10
commit c0e79f0
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/examples/tests/NonStructuralRec/edits b/examples/tests/NonStructuralRec/edits
@@ -6,4 +6,4 @@ rename value NonStructuralRec.S = S
 rename value NonStructuralRec.add = Nat.add
 
 termination NonStructuralRec.mapTree2 { measure (NonStructuralRec.size arg_1__) }
-obligations NonStructuralRec.mapTree2 prog_omega
+obligations NonStructuralRec.mapTree2 prog_lia
diff --git a/examples/tests/NonStructuralRec/preamble.v b/examples/tests/NonStructuralRec/preamble.v
@@ -1,3 +1,3 @@
 Require Coq.Program.Tactics.
-Require Omega.
-Ltac prog_omega := Coq.Program.Tactics.program_simpl;simpl;Omega.omega.
+Require Lia.
+Ltac prog_lia := Coq.Program.Tactics.program_simpl;simpl;Lia.lia.