blob: bc12ec755228d775e64c9384ed62c7eccffb4f03 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* Certification of Imperative Programs / Jean-Christophe Filli�tre *)
(* $Id$ *)
(* Correctness is base on the tactic Refine (developped on purpose) *)
Require Export Refine.
Require Export Tuples.
Require Export ProgInt.
Require Export ProgBool.
Require Export ProgWf.
Require Export Arrays.
Declare ML Module
"pmisc" "peffect" "prename"
"perror" "penv" "putil" "pdb" "pcic" "pmonad" "pcicenv"
"pred" "ptyping" "pwp" "pmlize" "ptactic" "psyntax".
Token "'".
|
