Fix typos

wintersteiger · wintersteiger · commit 3a9baca7a1bd · 2025-03-20T18:13:52.000Z
diff --git a/src/lib/proof3/gen/proof_spec.json b/src/lib/proof3/gen/proof_spec.json
@@ -180,7 +180,7 @@
       "args": {
         "concl": "Sequent"
       },
-      "doc": "`trivial (G,t ?- t, _)` proves `(G,t|-t, …)`"
+      "doc": "`trivial (G, t ?- t, _)` proves `(G, t |- t, …)`"
     },
     {
       "name": "and_elim",
diff --git a/src/lib/proof3/types.ml b/src/lib/proof3/types.ml
@@ -61,7 +61,7 @@ type proof_step =
   | Trivial of {
       concl: Imandrax_api_mir.Sequent.t
     }
-    (** [trivial (G,t ?- t, _)] proves [(G,t|-t, …)] *)
+    (** [trivial (G, t ?- t, _)] proves [(G, t |- t, …)] *)
   | And_elim of {
       concl: Imandrax_api_mir.Sequent.t;
       lhs: proof_step offset_for;

Original file line number	Diff line number	Diff line change
`@@ -61,7 +61,7 @@ type proof_step =`
`61`	`61`	`\| Trivial of {`
`62`	`62`	`concl: Imandrax_api_mir.Sequent.t`
`63`	`63`	`}`
`64`		`- (** [trivial (G,t ?- t, _)] proves [(G,t\|-t, …)] *)`
	`64`	`+ (** [trivial (G, t ?- t, _)] proves [(G, t \|- t, …)] *)`
`65`	`65`	`\| And_elim of {`
`66`	`66`	`concl: Imandrax_api_mir.Sequent.t;`
`67`	`67`	`lhs: proof_step offset_for;`