diff options
Diffstat (limited to 'contrib/correctness/Programs.v')
| -rw-r--r-- | contrib/correctness/Programs.v | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/contrib/correctness/Programs.v b/contrib/correctness/Programs.v new file mode 100644 index 0000000000..34d843908b --- /dev/null +++ b/contrib/correctness/Programs.v @@ -0,0 +1,36 @@ +(***********************************************************************) +(* 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 + "misc_utils" "effects" "renamings" "progTypes" "progAst" + "prog_errors" "prog_env" "prog_utils" + "prog_db" "prog_cci" "monad" "tradEnv" + "prog_red" "prog_typing" "prog_wp" "mlise" "prog_tactic" + "pprog". + +Token "'". + + + + |