Changeset 1601 for src/common/Errors.ma


Ignore:
Timestamp:
Dec 13, 2011, 2:49:52 PM (8 years ago)
Author:
sacerdot
Message:

Files ported to new version of the standard library.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Errors.ma

    r1599 r1601  
    1818include "basics/lists/list.ma".
    1919include "common/PreIdentifiers.ma".
    20 include "utilities/lists.ma".
    21 include "utilities/deppair.ma".
     20include "basics/lists/list.ma".
     21include "basics/russell.ma".
    2222
    2323(* * Error reporting and the error monad. *)
     
    103103λA,B,C,P,e,f.
    104104  match e with
    105   [ OK v ⇒ match v with [ dp v' p ⇒ f (fst … v') (snd … v') ? ]
     105  [ OK v ⇒ match v with [ mk_Sig v' p ⇒ f (fst … v') (snd … v') ? ]
    106106  | Error msg ⇒ Error ? msg
    107107  ].
     
    165165].
    166166whd // %
    167 [ @(use_sig B P)
     167[ @(pi2 … h')
    168168| cases t' #l' #p @p
    169169] qed.
Note: See TracChangeset for help on using the changeset viewer.