Changeset 3248 for Deliverables/D4.4/report.tex

Timestamp:

May 1, 2013, 1:40:42 AM (7 years ago)

Author:

sacerdot

Message:

Typos fixed.

File:

• Deliverables/D4.4/report.tex (modified) (2 diffs)

Deliverables/D4.4/report.tex

@@ -128 +128 @@
 The aim of WP4 is is to build the trusted version of the compiler back-end,
 from the intermediate \textsf{RTLabs} language down to assembly. The development
-is made in \textsf{matita}, and it allows the trsuted compiler to be extracted
+is made in \textsf{matita}, and it allows the trusted compiler to be extracted
 to \textsf{OCaml}.
 
@@ -143 +143 @@
 starts to be able to meddle with return addresses that live in memory, the call structure
 is no more guaranteed to be preserved after the high-level, structured
-languages. This is has little meaning as far as pure extensional semantic
+languages. This has little meaning as far as pure extensional semantic
 preservation is required---after all, if the source language meddles with the
 call structure there is no problem as long as the target language will follow.