From 9695972415a30da081d58e1ac18a51b61faf64bc Mon Sep 17 00:00:00 2001 From: Ambroise Date: Fri, 14 Aug 2026 07:19:27 +0200 Subject: [PATCH] Fix typos in how_to_contradiction.v --- src/metaprogramming/ltac2/how_to_contradiction.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/metaprogramming/ltac2/how_to_contradiction.v b/src/metaprogramming/ltac2/how_to_contradiction.v index aeae68b..055f4a8 100644 --- a/src/metaprogramming/ltac2/how_to_contradiction.v +++ b/src/metaprogramming/ltac2/how_to_contradiction.v @@ -96,7 +96,7 @@ From Ltac2 Require Import Ltac2 Constr Printf. inconsistent context. It is not meant to be linked with other tactics. Consequently, we have no use for [multimatch!] to implement [contradiction]. Choosing between [lazy_match!] and [match!] really depends on whether we need - more than a syntactic checkr, as we will see in the rest of this document. + more than a syntactic checker, as we will see in the rest of this document. *) @@ -159,7 +159,7 @@ Abort. destruct ($np $p) ]] - Notation, to do [Control.hyp] and [$] at once is only available in Rocq 9.1 or above. + Notation to do [Control.hyp] and [$] at once is only available in Rocq 9.1 or above. This leads us to the following script: *)