diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2018-10-31 18:44:16 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2018-10-31 18:44:16 +0100 |
| commit | caa7946a4da47b64807662468e68ecc2788a0980 (patch) | |
| tree | afdc7fcd4e4a5465c03bb330b8b8f6fdac8918b6 /README-JFLA19.md | |
| parent | 8a2f393bb52c3be681a301064539df65015bee22 (diff) | |
| download | smtcoq-caa7946a4da47b64807662468e68ecc2788a0980.tar.gz smtcoq-caa7946a4da47b64807662468e68ecc2788a0980.zip | |
One more example + typos in README
Diffstat (limited to 'README-JFLA19.md')
| -rw-r--r-- | README-JFLA19.md | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/README-JFLA19.md b/README-JFLA19.md index fc79f71..40ac5b5 100644 --- a/README-JFLA19.md +++ b/README-JFLA19.md @@ -22,13 +22,13 @@ La fin du fichier [examples/Example.v](https://github.com/smtcoq/smtcoq/blob/mas Côté Coq: -- L'extension du vérificateur (§ 3.3) est définie dans le fichier [src/Trace.v](https://github.com/smtcoq/smtcoq/blob/master/src/Trace.v). Notamment, la nouvelle règle `ForallInst` apparaît à la ligne 344. Son fonctionnement est donné dans le fichier [src/spl/Assumptions.v](https://github.com/smtcoq/smtcoq/blob/master/src/spl/Assumptions.v). +- L'extension du vérificateur (§ 3.3) est définie dans le fichier [src/Trace.v](https://github.com/smtcoq/smtcoq/blob/master/src/Trace.v). Notamment, la nouvelle règle `ForallInst` apparaît à la ligne 344. Sa propriété de correction est prouvée dans le fichier [src/spl/Assumptions.v](https://github.com/smtcoq/smtcoq/blob/master/src/spl/Assumptions.v). - Le cas d'application à la tactique `verit` (§ 3.4.3) est définie dans le fichier [src/SMTCoq.v](https://github.com/smtcoq/smtcoq/blob/master/src/SMTCoq.v), avec la définition de la tactique `vauto` permettant la preuve automatique des instanciations. Côté OCaml: -- L'extension du vérificateur (§ 3.3) est définie dans le fichier [src/trace/smtCertif.ml](https://github.com/smtcoq/smtcoq/blob/master/src/trace/smtCertif.ml). Notamment, la nouvelle règle `ForallInst` apparaît à la ligne 113. Son trairement est donné dans le fichier [src/trace/smtTrace.ml](https://github.com/smtcoq/smtcoq/blob/master/src/trace/smtTrace.ml), ligne 423. +- L'extension du vérificateur (§ 3.3) est définie dans le fichier [src/trace/smtCertif.ml](https://github.com/smtcoq/smtcoq/blob/master/src/trace/smtCertif.ml). Notamment, la nouvelle règle `ForallInst` apparaît à la ligne 113. Son traitement est donné dans le fichier [src/trace/smtTrace.ml](https://github.com/smtcoq/smtcoq/blob/master/src/trace/smtTrace.ml), ligne 423. - Le préprocesseur pour la règle forall_inst de veriT (§ 3.4.2 et 3.4.3) est défini dans le fichier [src/verit/veritSyntax.ml](https://github.com/smtcoq/smtcoq/blob/master/src/verit/veritSyntax.ml), lignes 213 et suivantes. |