From d2642b1c38d75eb41e3f86edb1112c65a0145945 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Wed, 23 Sep 2015 18:08:15 -0400 Subject: [PATCH] Fixed typo --- scribblings/oll.scrbl | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/scribblings/oll.scrbl b/scribblings/oll.scrbl index ce3c855..9c562bc 100644 --- a/scribblings/oll.scrbl +++ b/scribblings/oll.scrbl @@ -4,14 +4,13 @@ @title{OLL: Ott-like Library} @defmodule[cur/oll] -The OLL provides syntax extensions for defining programming languages as -inductive data. The library is inspired by Ott, which provides an -language that resembles math notation for generating Coq definitions. -The purpose of the OLL is not to replace Ott, but to demonstrate how -powerful syntactic meta-programming can bring features previously only -provided by external tools into the language. +The OLL provides syntax extensions for defining programming languages as inductive data. The library +is inspired by Ott@todo{Citation needed}, which provides an language that resembles math notation for +generating Coq definitions. The purpose of the OLL is not to replace Ott, but to demonstrate how +powerful syntactic meta-programming can bring features previously only provided by external tools into +the language. -@defform[(define-lanugage name +@defform[(define-language name maybe-vars maybe-output-coq maybe-output-latex