Andrej Dudenhefner
Setting this flag in `auto` (and `eauto`) makes the resolution be slightly closer to `simple (e)apply`. Also, this behavior is closer to `typeclasses eauto`. Fixes #16323 Fixes #16062 Currently, `debug...
#### Description of the problem Possibly related: https://github.com/coq/coq/issues/6544 (but here the behavior is the other way around). The documentation of `Hint Immediate` states that > adds the tactic [simple apply](https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:tacv.simple-apply)...
#### Description of the problem When `auto` is called on a goal containing an evar, the outcome is difficult to predict and the debug log on `exact` is misleading. ```coq...
#### Description of the problem `typeclasses eauto` may fail on a trivial goal, whereas `typeclasses eauto with nocore` succeeds (using stronger unification). ```coq Create HintDb empty. Goal forall (P :...
#### Description of the problem `congruence` is designed to work on non-dependent terms. However, its obliviousness can lead to unexpected behavior and regressions https://github.com/coq/coq/issues/16140. The example below shows `congruence` both...
Improves robustness in case of stronger (e)auto (see [coq/#16293](https://github.com/coq/coq/pull/16293)).
**Brief Summary** `move /(in_app_or).` always seems to produce > _view_subject_ is used in conclusion. **Minimal Example** ``` From Coq Require Import ssreflect ssrfun ssrbool. Set Implicit Arguments. Unset Strict Implicit....
Universal, binary Turing machine with 1 tape The construction is via a universal Krivine machine simulation.
We currently have - `MM 2` two-counter Minsky machines - `MM2` two-counter (alternative) Minsky machines - `MMA 2` two-counter (alternative) Minsky machines - ~`CM2`~ two-counter (alternative) Minsky machines Much of...
Goals of this PR: - Top-level (universal) Turing machine halting `Definition HaltUTM : tape (finType_CS bool) -> Prop := fun t => HaltsTM UTM [t].` and `Lemma HaltUTM_undec : undecidable...