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/common/Globalenvs.ma

    r2624 r2645  
    274274
    275275(* init *)
    276 
    277 axiom InitDataStoreFailed : String.
    278276
    279277definition add_globals : ∀F,V:Type[0].
     
    11361134] qed.
    11371135
    1138 record related_globals_gen (tag:String) (A,B:Type[0]) (t: universe tag → A → B × (universe tag)) (ge:genv_t A) (ge':genv_t B) : Prop ≝ {
     1136record related_globals_gen (tag:identifierTag) (A,B:Type[0]) (t: universe tag → A → B × (universe tag)) (ge:genv_t A) (ge':genv_t B) : Prop ≝ {
    11391137  rgg_find_symbol: ∀s.
    11401138    find_symbol … ge s = find_symbol … ge' s;
Note: See TracChangeset for help on using the changeset viewer.