Changeset 1608 for src/common

Timestamp:

Dec 14, 2011, 2:30:39 PM (9 years ago)

Author:

sacerdot

Message:

Porting to new library still in progress.

File:

• src/common/Errors.ma (modified) (1 diff)

src/common/Errors.ma

@@ -91 +91 @@
 (* Dependent pair version. *)
 notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40
-  for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp ${ident v} ${ident p} ⇒ ${e'} ]) }.
+  for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ mk_Sig ${ident v} ${ident p} ⇒ ${e'} ]) }.
 
 lemma Prod_extensionality: