Adapt to Coq PR #19301: unify the syntax of definition and theorem #1328

Adapt to Coq PR #19301: unify the syntax of definition and theorem

Usage Workflow file

11 warnings

The following actions use a deprecated Node.js version and will be forced to run on node20: actions/checkout@v3, actions/setup-node@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/

'DidChangeConfigurationParams' is defined but never used. Allowed unused vars must match /^_/u

'Command' is defined but never used. Allowed unused vars must match /^_/u

'token' is defined but never used. Allowed unused args must match /^_/u

'integer' is defined but never used. Allowed unused vars must match /^_/u

'isMouseOrKeyboardEvent' is defined but never used. Allowed unused vars must match /^_/u

'res' is defined but never used. Allowed unused args must match /^_/u

'goalsHook' is assigned a value but never used. Allowed unused vars must match /^_/u

'editor' is defined but never used. Allowed unused args must match /^_/u

'commands' is defined but never used. Allowed unused vars must match /^_/u

'workspace' is defined but never used. Allowed unused vars must match /^_/u