diff options
Diffstat (limited to 'contrib/correctness/examples/fact.v')
| -rw-r--r-- | contrib/correctness/examples/fact.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/contrib/correctness/examples/fact.v b/contrib/correctness/examples/fact.v index 8c694d132..a6c443807 100644 --- a/contrib/correctness/examples/fact.v +++ b/contrib/correctness/examples/fact.v @@ -18,7 +18,7 @@ (* Proof of an imperative program computing the factorial (over type nat) *) -Require Programs. +Require Correctness. Require Omega. Require Arith. @@ -60,7 +60,6 @@ Correctness factorielle end { y = (fact x@0) }. Proof. -Split. (* decreasing of the variant *) Omega. (* preservation of the invariant *) |