Changeset 1608 for src/common


Ignore:
Timestamp:
Dec 14, 2011, 2:30:39 PM (8 years ago)
Author:
sacerdot
Message:

Porting to new library still in progress.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Errors.ma

    r1601 r1608  
    9191(* Dependent pair version. *)
    9292notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40
    93   for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp ${ident v} ${ident p} ⇒ ${e'} ]) }.
     93  for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ mk_Sig ${ident v} ${ident p} ⇒ ${e'} ]) }.
    9494
    9595lemma Prod_extensionality:
Note: See TracChangeset for help on using the changeset viewer.