diff src/Subset.v @ 533:8921cfa2f503

Use TeX magic to prevent -- from being displayed as an en dash
author Cl?ment Pit--Claudel <clement.pitclaudel@live.com>
date Tue, 07 Apr 2015 18:59:24 -0400
parents b7419a10e52e
children ed829eaa91b2
line wrap: on
line diff
--- a/src/Subset.v	Fri Nov 21 11:21:37 2014 -0500
+++ b/src/Subset.v	Tue Apr 07 18:59:24 2015 -0400
@@ -671,12 +671,15 @@
 
 (** We can build a [sumor] version of the "bind" notation and use it to write a similarly straightforward version of this function.  %Again, the notation definition exposes the ASCII syntax with an operator \texttt{<-{}-}, while the later code uses a nicer long left arrow $\longleftarrow$.% *)
 
+(** %\def\indash{-}\catcode`-=13\def-{\indash\kern0pt }% *)
+
 Notation "x <-- e1 ; e2" := (match e1 with
                                | inright _ => !!
                                | inleft (exist x _) => e2
                              end)
 (right associativity, at level 60).
 
+(** %\catcode`-=12% *)(* *)
 (** printing * $\times$ *)
 
 (* EX: Write a more expressively typed version of the last exercise. *)