Commit 5727c9aa authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'patch-1' into 'master'

Fix typo in doc

See merge request !68
parents 10bc4e2a f33ed547
Pipeline #16309 passed with stage
in 11 minutes and 41 seconds
...@@ -65,7 +65,7 @@ Hint Extern 0 (TCNoBackTrack _) => constructor; apply _ : typeclass_instances. ...@@ -65,7 +65,7 @@ Hint Extern 0 (TCNoBackTrack _) => constructor; apply _ : typeclass_instances.
(* A conditional at the type class level. Note that [TCIf P Q R] is not the same (* A conditional at the type class level. Note that [TCIf P Q R] is not the same
as [TCOr (TCAnd P Q) R]: the latter will backtrack to [R] if it fails to 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, establish [Q], 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 note that [TCOr (TCAnd P Q) (TCAnd (TCNot P) R)] would not work; we generally
would not be able to prove the negation of [P]. *) would not be able to prove the negation of [P]. *)
Inductive TCIf (P Q R : Prop) : Prop := Inductive TCIf (P Q R : Prop) : Prop :=
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment