Fix Alectryon example

Author: shilangyu

.github/pip-requirements.txt

@@ -1,4 +1,4 @@
-alectryon @ git+https://github.com/cpitclaudel/alectryon@next
+alectryon @ git+https://github.com/cpitclaudel/alectryon@a02a99c75c4166efc8812a600e8cbf4588424c0f
 git+https://github.com/epfl-systemf/SpecMerger
 requests == 2.32.4
 beautifulsoup4 == 4.12.3

examples/rocq_proof/Example.v

@@ -56,17 +56,20 @@ Section AbstractMatching.
   Definition compilation_result :=
     Semantics.compilePattern regex_of_interest rer.
 
-  Lemma compiles_successfully:
+  Lemma compiles_successfully_refl:
      exists m, compilation_result = Result.Success m.
   Proof.
     (** Again, since the regex is concrete, we can just compute. **)
     eexists. cbn. reflexivity.
+  Qed.
 
-    (** But we can also use some theorems from the development, which would work even if the regex was left more abstract. **)
-    Restart.
+  (** But we can also use some theorems from the development, which would work even if the regex was left more abstract: **)
 
-    Search Semantics.compilePattern Result.Success.
+  Search Semantics.compilePattern Result.Success.
 
+  Lemma compiles_successfully_thm:
+     exists m, compilation_result = Result.Success m.
+  Proof.
     (** We use the theorem listed in section 4.2.1 in the paper, [compilePattern_success], which states that compilation always succeeds if a regex passes early error checks. **)
     apply compilePattern_success.
     - (** We have to show that the number of groups per [rer] matches the actual number