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/ERTLptr/ERTLptr.ma

    r2604 r2645  
    2929definition ertlptr_seq_joint ≝ extension_seq ERTLptr.
    3030coercion ertlptr_seq_to_joint_seq : ∀globals.∀s : ertlptr_seq.joint_seq ERTLptr globals ≝ ertlptr_seq_joint
    31   on _s : ertlptr_seq to joint_seq ERTLptr.
     31  on _s : ertlptr_seq to joint_seq ERTLptr ?.
    3232 
Note: See TracChangeset for help on using the changeset viewer.