diff src/Interps.v @ 292:2c88fc1dbe33

A pass of double-quotes and LaTeX operator beautification
author Adam Chlipala <adam@chlipala.net>
date Wed, 10 Nov 2010 16:31:04 -0500
parents 05250878e4ca
children b441010125d4
line wrap: on
line diff
--- a/src/Interps.v	Wed Nov 10 15:42:05 2010 -0500
+++ b/src/Interps.v	Wed Nov 10 16:31:04 2010 -0500
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2009, Adam Chlipala
+(* Copyright (c) 2008-2010, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -64,7 +64,9 @@
 
   Notation "# v" := (Var v) (at level 70).
 
+  (** printing ^ $\dag$ *)
   Notation "^ n" := (Const n) (at level 70).
+  (** printing +^ $\hat{+}$ *)
   Infix "+^" := Plus (left associativity, at level 79).
 
   Infix "@" := App (left associativity, at level 77).