Merge pull request #199 from coq-community/master+adapting-cast-using… · coq-community/corn@f865fa8

The following actions uses node12 which is deprecated and will be forced to run on node16: actions/checkout@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/

Notation "_ = _" was already used in scope type_scope.

Notation "_ ≠ _" was already used in scope type_scope.

Declaring a scope implicitly is deprecated; use in advance an

Adding and removing hints in the core database implicitly is

Declaring a scope implicitly is deprecated; use in advance an

Notation "_ = _" was already used in scope type_scope.

Notation "_ ≠ _" was already used in scope type_scope.

Notation "_ ≠ _" was already used in scope type_scope.

Notation "_ ≠ _" was already used in scope type_scope.

Notation "_ = _" was already used in scope type_scope.

Provide feedback