From cd1ed3dd8fa30f140996d809b9dac87adf1b9e43 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 19 Feb 2018 17:46:14 +0100
Subject: [PATCH] Fix horrible typo.

---
 theories/base.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/base.v b/theories/base.v
index 12e6afd7..3185a023 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -66,7 +66,7 @@ Hint Extern 0 (NoBackTrack _) => constructor; apply _ : typeclass_instances.
 as [TCOr (TCAnd P Q) R]: the latter will backtrack to [R] if it fails to
 establish [R], i.e. does not have the behavior of a conditional. Furthermore,
 note that [TCOr (TCAnd P Q) (TCAnd (TCNot P) R)] would not work; we generally
-would not be able to proof the negation of [P]. *)
+would not be able to prove the negation of [P]. *)
 Inductive TCIf (P Q R : Prop) :=
   | TCIf_true : P → Q → TCIf P Q R
   | TCIf_false : R → TCIf P Q R.
-- 
GitLab