Commit 503a2ee6 authored by Martin Clochard's avatar Martin Clochard

examples: suppress warnings.

parent d9fe3880
......@@ -55,7 +55,7 @@ module PrimeNumbers
(** Bertrand's postulate, admitted as an axiom
(the label is there to suppress the warning issued by Why3) *)
axiom Bertrand_postulate "W:conservative_extension:N" :
axiom Bertrand_postulate "W:non_conservative_extension:N" :
forall p: int. prime p -> not (no_prime_in p (2*p))
(** [prime_numbers m] returns an array containing the first [m]
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment