Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Main_proof.v 235 Bytes
Newer Older
charguer's avatar
charguer committed
1
Require Export CFLib Main_ml.
charguer's avatar
charguer committed
2
Require Import Auxi_ml Auxi_proof Extra.
charguer's avatar
open  
charguer committed
3

charguer's avatar
charguer committed
4
Lemma g_spec : 
charguer's avatar
charguer committed
5
  Spec g (x:int) |R>> R \[] (fun y => \[same x y]).
charguer's avatar
charguer committed
6 7 8 9 10
Proof.
  xcf. intros. xapp. hsimpl~. 
Qed.

Hint Extern 1 (RegisterSpec g) => Provide g_spec.