Skip to content
Snippets Groups Projects
Commit 21713f80 authored by Allan Blanchard's avatar Allan Blanchard Committed by Andre Maroneze
Browse files

[WP+Coq] Updates some tests

parent 79f84f5e
No related branches found
No related tags found
No related merge requests found
Require Import ZArith.
Definition my_abs := Zabs.
Definition my_abs := Z.abs.
......@@ -4,9 +4,9 @@ Goal typed_abs_abs_ensures.
Hint abs,default,property.
Proof.
intro n. intros. subst.
unfold my_abs.
induction H1;
[ intros ; rewrite Zabs_non_eq | intros ; rewrite Zabs_eq ] ;
unfold my_abs.
induction H1;
[ intros ; rewrite Zabs_non_eq | intros ; rewrite Z.abs_eq ] ;
auto with zarith.
Qed.
......
......@@ -5,16 +5,15 @@
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 2 goals scheduled
[wp] [Coq] Goal typed_lemma_offset : Saved script
[wp] [Coq] Goal typed_lemma_offset : Default tactic
[wp] [Coq (Native)] Goal typed_lemma_offset : Unsuccess
[wp] [Coq (Native)] Goal typed_lemma_offset : Valid
[wp] [Coq] Goal typed_lemma_test : Saved script
[wp] [Coq] Goal typed_lemma_test : Default tactic
[wp] [Coq (Native)] Goal typed_lemma_test : Unsuccess
[wp] Proved goals: 0 / 2
Coq: 0 (unsuccess: 2)
[wp] [Coq (Native)] Goal typed_lemma_test : Valid
[wp] Proved goals: 2 / 2
Qed: 0
Coq: 2
[wp] Report in: 'tests/wp_plugin/oracle_qualif/inductive.0.report.json'
[wp] Report out: 'tests/wp_plugin/result_qualif/inductive.0.report.json'
-------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Lemma - - 2 0.0%
Lemma - - 2 100%
-------------------------------------------------------------
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment