coq

coq copied to clipboard

intros '(x,y)

48

Hi, the idea of an introduction pattern following the `'pat`-style quantification is in the air for some time. This PR is proposing a (very) raw first proof of concept. Basic...

herbelin

#### Description of the problem ```coq Goal True. Proof. ``` gives ``` Error: Anomaly "Stm.join: tip not cached" Please report at http://coq.inria.fr/bugs/. ``` cc @coq/stm-maintainers #### Coq Version https://gitlab.com/coq/coq/-/jobs/2740357137/artifacts/download i.e....

JasonGross

Typeclass search distinguishes folded from unfolded primitive projections

9

#### Description of the problem The folded and unfolded state of `Hint Opaque` projections are not unified by `autoapply`. ```coq From Coq Require Import ssreflect. #[local] Set Primitive Projections. Class...

Janno

Support for 'Hint Exact' for when Resolve (apply) does not unify

12

Note: the issue was created automatically with bugzilla2github tool Original bug ID: BZ#3104 From: @ezyang Reported version: trunk CC: @JasonGross, @ppedrot

coqbot

`auto using` uses more powerful unification than `simple apply`

3

#### Version Coq 8.8+alpha (commit a2b02cb91) #### Operating system macOS #### Description of the problem `auto using pf` is more powerful than adding pf as a hint because it doesn't...

tchajed

eauto fails with `Hint Immediate`/`Hint Resolve` on matching head symbol where `simple apply` succeeds

3

#### 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)...

mrhaandi

auto incoherent on goal with evars

1

#### 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...

mrhaandi

Universe Polymorphism, JMeq, and dependent types cause a QED anomaly.

6

#### Description of the problem Universe Polymorphism, JMeq, and a simple dependent type cause (previously working) proofs to fail at QED time. The exact error message is `Anomaly "File "kernel/term_typing.ml",...

jsarracino

Issue #16262: do not override generic format if not reserved and only printing

5

**Kind**: enhancement This is an experimental change of heuristic about when a notation defined using the `Notation "..." := ...` syntax is liable to modify a generic printing rule. The...

herbelin

Dispatch consistently it_mkLambda and cie between econstr.ml and termops.ml

5

**Kind:** cleanup This is part 2 of proposal at #15562. It includes: - removal redundancy between termops and econstr - move of `it_mkLambda`/`it_mkProd` combinators from `termops.ml` to `eConstr.ml` when on...

herbelin