Skip to content

Add Ltac2 Char.is_space, String.split_on_char and String.trim#22239

Open
JasonGross wants to merge 1 commit into
rocq-prover:masterfrom
JasonGross:ltac2-string-split-trim
Open

Add Ltac2 Char.is_space, String.split_on_char and String.trim#22239
JasonGross wants to merge 1 commit into
rocq-prover:masterfrom
JasonGross:ltac2-string-split-trim

Add Ltac2 Char.is_space, String.split_on_char and String.trim

f855903
Select commit
Loading
Failed to load commit list.
coqbot-app / GitLab CI pipeline (pull request) completed Jul 8, 2026 in 0s

Light pipeline completed successfully on GitLab CI

This GitLab pipeline sets the following variables:

  • FULL_CI: false

It contains the following stages and jobs:

GitLab Project ID: 4504

View more details on coqbot-app