Commits · master · coq / coq

This project is mirrored from https://*****@github.com/coq/coq.git. Pull mirroring updated Jan 21, 2022.

20 Jan, 2022 5 commits

Merge PR #15470: Slightly clean the Printing Existential Instances code · 06970e08
coqbot-app[bot] authored Jan 20, 2022
```
Reviewed-by: Alizter
Reviewed-by: ejgallego
Co-authored-by: ejgallego <ejgallego@users.noreply.github.com>
```
06970e08
Merge PR #15507: Check existence of the name in Declare.CInfo.start_core · 8fba1770
coqbot-app[bot] authored Jan 20, 2022
```
Reviewed-by: ejgallego
Co-authored-by: ejgallego <ejgallego@users.noreply.github.com>
```
8fba1770

Merge PR #15515: Moving file in obsolete doc/changelog/08-tools change log... · 5b4ea258

coqbot-app[bot] authored Jan 20, 2022

Merge PR #15515: Moving file in obsolete doc/changelog/08-tools change log directory to a more appropriate change log directory

Reviewed-by: Zimmi48
Co-authored-by: Zimmi48 <Zimmi48@users.noreply.github.com>

5b4ea258

Merge PR #15378: Understand goal selectors in ltac2 · 41668b48
coqbot-app[bot] authored Jan 20, 2022
```
Reviewed-by: ppedrot
Ack-by: Zimmi48
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
```
41668b48
Merge PR #15502: Fix setoid_rewrite on Equiv : Type -> Type -> Type · df8297f2
coqbot-app[bot] authored Jan 20, 2022
```
Reviewed-by: Alizter
Ack-by: ppedrot
Co-authored-by: Alizter <Alizter@users.noreply.github.com>
```
df8297f2

19 Jan, 2022 7 commits
- Moving contents of doc/changelog/08-tools in doc/changelog/08-cli-tools. · 1f7e8e32
  Hugo Herbelin authored Jan 19, 2022
```
08-tools was concurrently repopulated in PR #13460 while it had been
renamed to 08-cli-tools in the meantime.
```
  1f7e8e32
- Merge PR #15503: Add `ocaml-lsp` dev dependency to default.nix · b1c564a1
  coqbot-app[bot] authored Jan 19, 2022
```
Reviewed-by: vbgl
Co-authored-by: Alizter <Alizter@users.noreply.github.com>
```
  b1c564a1
- ocp-indent: strict_with=auto · 17207000
  Gaëtan Gilbert authored Jan 19, 2022
  
  17207000
- Slightly clean the Printing Existential Instances code · 28d9541d
  Gaëtan Gilbert authored Jan 12, 2022
  
  28d9541d
- Fix setoid_rewrite on Equiv : Type -> Type -> Type · 2da49245
  Gaëtan Gilbert authored Jan 18, 2022
```
Fix #6278
```
  2da49245
- Check existence of the name in Declare.Proof.start_core · 342053da
  Gaëtan Gilbert authored Jan 18, 2022
```
Close #15031

Leaving start_dependent (_derive, _equations) alone for now.
```
  342053da
- Merge PR #15443: [CI] Add MathComp Analysis · e7f04bac
  coqbot-app[bot] authored Jan 19, 2022
```
Reviewed-by: Alizter
Ack-by: gares
Ack-by: ppedrot
Ack-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
```
  e7f04bac
18 Jan, 2022 3 commits
- Add `ocaml-lsp` dev dependency to default.nix · 58d7dc6f
  Maxime Dénès authored Jan 18, 2022
```
Useful for devs who use VSCode
```
  58d7dc6f
- Merge PR #13969: Fix bug #7916, allowing `Reflexive` to have mode `! !` · d9aa8fb4
  coqbot-app[bot] authored Jan 18, 2022
```
Reviewed-by: ppedrot
Ack-by: robbertkrebbers
Ack-by: jfehrle
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
```
  d9aa8fb4
- Understand goal selectors in ltac2 · 22a90c4e
  Gaëtan Gilbert authored Dec 16, 2021
```
(par: abstract will not work properly)
```
  22a90c4e
17 Jan, 2022 15 commits
- Add changelog entry · c2ae0244
  Matthieu Sozeau authored Jan 12, 2022
  
  c2ae0244
- Overlays · f16c7eaa
  Matthieu Sozeau authored Apr 23, 2021
  
  f16c7eaa
- Doc about RewriteRelation's use · e67ead38
  Matthieu Sozeau authored Dec 14, 2021
```
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
```
  e67ead38
- Improve is_applied_rewrite_relation test · a98fa072
  Matthieu Sozeau authored Mar 30, 2021
  
  a98fa072
- Fix bug #7916, allowing `Reflexive` to have mode `! !` · 0b82e46c
  Matthieu Sozeau authored Mar 19, 2021
  
  0b82e46c
- Merge PR #15464: Restore compilation of the bytecode interpreter with OCaml 5.00. · d5e61b29
  coqbot-app[bot] authored Jan 17, 2022
```
Reviewed-by: ppedrot
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
```
  d5e61b29
- Merge PR #15466: Delay the merging of universes for type compatibility in old unification. · 9bd46463
  coqbot-app[bot] authored Jan 17, 2022
```
Reviewed-by: mattam82
Ack-by: SkySkimmer
Co-authored-by: mattam82 <mattam82@users.noreply.github.com>
```
  9bd46463
- Merge PR #15484: Stronger invariants on the syntax of records and variants · fa930905
  coqbot-app[bot] authored Jan 17, 2022
```
Reviewed-by: Alizter
Co-authored-by: Alizter <Alizter@users.noreply.github.com>
```
  fa930905
- Merge PR #15490: Remove the unused Namegen.compute_and_force_displayed_name_in function. · 6e8fc012
  coqbot-app[bot] authored Jan 17, 2022
```
Reviewed-by: Alizter
Co-authored-by: Alizter <Alizter@users.noreply.github.com>
```
  6e8fc012
- Merge PR #15461: Explain details of "only" selector · c0c0ff6d
  coqbot-app[bot] authored Jan 17, 2022
```
Reviewed-by: Alizter
Ack-by: SkySkimmer
Co-authored-by: Alizter <Alizter@users.noreply.github.com>
```
  c0c0ff6d
- Merge PR #15358: Avoid bound names in instantiate_notation_constr · 39456108
  coqbot-app[bot] authored Jan 17, 2022
```
Reviewed-by: herbelin
Co-authored-by: Alizter <Alizter@users.noreply.github.com>
```
  39456108
- Merge PR #14759: Improve function napply_except_last, fix its description comment · a40bfaee
  coqbot-app[bot] authored Jan 17, 2022
```
Reviewed-by: herbelin
Co-authored-by: Alizter <Alizter@users.noreply.github.com>
```
  a40bfaee
- Merge PR #15390: Port `eauto` to the new engine · c8a53f1e
  coqbot-app[bot] authored Jan 17, 2022
```
Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
```
  c8a53f1e
- Merge PR #15459: [opam] honor coq-native · 496f5587
  coqbot-app[bot] authored Jan 17, 2022
```
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
```
  496f5587
- Merge PR #15438: Rely on the new case representation in Evarsolve. · 114e3709
  coqbot-app[bot] authored Jan 17, 2022
```
Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
```
  114e3709
16 Jan, 2022 5 commits
- Merge PR #15485: Consistently adding periods in error messages raised in vernac · 4f801602
  coqbot-app[bot] authored Jan 16, 2022
```
Reviewed-by: Alizter
Co-authored-by: Alizter <Alizter@users.noreply.github.com>
```
  4f801602
- Merge PR #15488: Remove Eauto.registered_e_assumption. · 3b9f7554
  coqbot-app[bot] authored Jan 16, 2022
```
Reviewed-by: Alizter
Co-authored-by: Alizter <Alizter@users.noreply.github.com>
```
  3b9f7554
- Merge PR #15442: Make the program naming scheme uniform w.r.t. the standard one. · f4ccedcf
  coqbot-app[bot] authored Jan 16, 2022
```
Reviewed-by: herbelin
Reviewed-by: Alizter
Ack-by: jfehrle
Co-authored-by: Alizter <Alizter@users.noreply.github.com>
```
  f4ccedcf
- Merge PR #14563: Adding user support for naming a variable inhabiting a record type · 11d96242
  coqbot-app[bot] authored Jan 16, 2022
```
Reviewed-by: Alizter
Ack-by: jfehrle
Ack-by: JasonGross
Ack-by: ejgallego
Co-authored-by: Alizter <Alizter@users.noreply.github.com>
```
  11d96242
- Remove the unused Namegen.compute_and_force_displayed_name_in function. · e9db1043
  Pierre-Marie Pédrot authored Jan 13, 2022
  
  e9db1043
15 Jan, 2022 5 commits
- Consistently adding periods in error messages raised in vernac. · 6c04eb72
  Hugo Herbelin authored Jan 14, 2022
```
Co-authored-by: Ali Caglayan <alizter@gmail.com>
```
  6c04eb72
- Changelog for #14563 · e48cb8a8
  Hugo Herbelin authored Jan 15, 2022
  
  e48cb8a8
- Overlay for elpi · 61823298
  Hugo Herbelin authored Jan 15, 2022
  
  61823298
- Adding user support for naming a variable inhabiting a record/class type. · c3ca6968
  Hugo Herbelin authored Jun 27, 2021
```
Syntax is: Record foo := { ... } as ident.
```
  c3ca6968
- Remove Eauto.registered_e_assumption. · 783e19a4
  Pierre-Marie Pédrot authored Jan 15, 2022
```
It was performing literally the same thing as Eauto.e_assumption.
```
  783e19a4