Changeset 2645 for src/ERTL


Ignore:
Timestamp:
Feb 7, 2013, 9:22:22 PM (7 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/ERTL/ERTL.ma

    r2604 r2645  
    9797definition ertl_seq_joint ≝ extension_seq ERTL.
    9898coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ERTL globals ≝ ertl_seq_joint
    99   on _s : ertl_seq to joint_seq ERTL.
     99  on _s : ertl_seq to joint_seq ERTL ?.
Note: See TracChangeset for help on using the changeset viewer.