Hugo Herbelin

Fixes #9412: Context command ignored implicit binders

44

**Kind:** bug fix Fixes / closes #9412 This is a quick fix (which will have to be adapted on top of #12272). - [X] Added / updated test-suite - [X]...

Deactivation of notations: providing vernac syntax, vo registration and support for deactivation of abbreviations

37

**Kind:** feature This extends #703 on selective deactivation of notations by adding: - concrete syntax for deactivation/reactivation - registration in vo files - support for deactivation of abbreviations Added: Now...

Fixes #16303: evar defined before its instance was checked, leading to error message trying to unexpectingly display an already defined evar

40

This improves commit 26a5b65df from PR #14797. Fixes #16303 - [x] Added / updated **test-suite**. - [x] Added **changelog**.

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

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

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

Addressing proposal #15562: cleaning API of functions for destructing/constructing abstractions or products wrt contexts

4

**Kind:** cleanup Fixes / closes #15562 This organizes the naming of functions for destructing/constructing abstractions or products wrt contexts around the schemes "{decompose_,strip_,}{lam,prod}{_n,}{_assum,_decls,}{_red,}" and "dest{Lambda,Prod}{_red,}". See #15562 for details. Better...

Syntax of `-arg` in `_CoqProject`

13

Hi, I'm writing in relation with a CoqIDE issue coq/coq#5773. The `_CoqProject` file supports a syntax `-arg` which is not documented in the Coq reference manual but which we fortunately...

To fix coq/coq#16303, we enforce the stronger invariant on Evarsolve.check_evar_instance that the evar is not yet defined at the time we check the well-typing of its instance. This PR enforces...

To be merged synchronously with coq/coq#15582.