Changeset 2645 for src/RTL


Ignore:
Timestamp:
Feb 7, 2013, 9:22:22 PM (8 years ago)
Author:
sacerdot
Message:
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL_semantics.ma

    r2601 r2645  
    1 include "joint/SemanticUtils.ma".
     1include "joint/semanticsUtils.ma".
    22include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
    33include alias "common/Identifiers.ma".
     
    2626
    2727(*CSC: could we use here a dependent type to avoid the Error case? *)
    28 axiom EmptyStack: String.
    29 axiom OutOfBounds: String.
    3028
    3129definition rtl_fetch_ra:
Note: See TracChangeset for help on using the changeset viewer.