# HG changeset patch # User Adam Chlipala # Date 1391363295 18000 # Node ID 8f9f1e5b2fe3fb29f809fe17cfebd68fa19a5d62 # Parent 4fa68336895856f3b45ebc6ffebf21f6e43fcf2d Fix HTML formatting bug diff -r 4fa683368958 -r 8f9f1e5b2fe3 src/GeneralRec.v --- a/src/GeneralRec.v Sat Jan 25 11:46:00 2014 -0500 +++ b/src/GeneralRec.v Sun Feb 02 12:48:15 2014 -0500 @@ -940,6 +940,6 @@ exists 1; reflexivity. Qed. -(** One further disadvantage of [comp] is that we cannot prove an inversion lemma for executions of [Bind] without appealing to an %\emph{axiom}%, a logical complication that we discuss at more length in Chapter 12. The other three techniques allow proof of all the important theorems within the normal logic of Coq. +(** One further disadvantage of [comp] is that we cannot prove an inversion lemma for executions of [Bind] without appealing to an _axiom_, a logical complication that we discuss at more length in Chapter 12. The other three techniques allow proof of all the important theorems within the normal logic of Coq. Perhaps one theme of our comparison is that one must trade off between, on one hand, functional programming expressiveness and compatibility with normal Coq types and computation; and, on the other hand, the level of proof obligations one is willing to handle at function definition time. *)