# HG changeset patch
# User Cl?ment Pit--Claudel <clement.pitclaudel@live.com>
# Date 1428447564 14400
# Node ID 8921cfa2f5031bf2489e8c106b628ffb7a168339
# Parent  aed0fcfabdbdee11c7092d636e4c45b44aa2b8d9
Use TeX magic to prevent -- from being displayed as an en dash

diff -r aed0fcfabdbd -r 8921cfa2f503 src/Subset.v
--- 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. *)