diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-28 12:57:58 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-28 12:57:58 +0000 |
commit | c48b9097201dc9a1e326acdbce491fe16cab01e6 (patch) | |
tree | 53335d9dcb4aead3ec1f42e4138e87649640edd0 /doc/removeproofs | |
parent | 2b89ae94ffb6dc56fa780acced8ab7ad0afbb3b5 (diff) | |
download | compcert-c48b9097201dc9a1e326acdbce491fe16cab01e6.tar.gz compcert-c48b9097201dc9a1e326acdbce491fe16cab01e6.zip |
Fusion de la branche restr-cminor. En Clight, C#minor et Cminor, les expressions sont maintenant pures et les appels de fonctions sont des statements. Ajout de semantiques coinductives pour la divergence en Clight, C#minor, Cminor. Preuve de preservation semantique pour les programmes qui divergent.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@409 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'doc/removeproofs')
-rwxr-xr-x | doc/removeproofs | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/removeproofs b/doc/removeproofs index 82809ba6..5ae9a235 100755 --- a/doc/removeproofs +++ b/doc/removeproofs @@ -2,7 +2,9 @@ for i in $*; do mv $i $i.bak - sed -e '/<code class="keyword">Proof<\/code> *\./,/<code class="keyword">\(Qed\|Defined\)<\/code> *\./d' $i.bak > $i + sed -e '/<span class="keyword">Proof<\/span> *\./,/<span class="keyword">\(Qed\|Defined\)<\/span> *\./d' \ + -e "s/\"'do' X <- A ; B\" error_monad_scope/doXAB error_monad_scope/g" \ + $i.bak > $i rm $i.bak done |