MetaCoq CI

Merge pull request #1089 from MetaCoq/force-lazy-evaluation #2783

Annotations

10 warnings

Overwriting previous delimiting key B in scope bool_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.

The following logical axioms were

There is no flag or option with this name:

Setting extraction output directory by default to

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

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