This project is mirrored from https://github.com/coq/coq.
Pull mirroring updated .
- 12 Aug, 2022 1 commit
-
-
coqbot-app[bot] authored
Reviewed-by: SkySkimmer Co-authored-by:
SkySkimmer <SkySkimmer@users.noreply.github.com>
-
- 11 Aug, 2022 1 commit
-
-
coqbot-app[bot] authored
Reviewed-by: SkySkimmer Co-authored-by:
SkySkimmer <SkySkimmer@users.noreply.github.com>
-
- 08 Aug, 2022 4 commits
-
-
Pierre-Marie Pédrot authored
Fixes #16152: Deduplicate rewrite hints imported multiple times.
-
Pierre-Marie Pédrot authored
This is a horribly hacky vernac command that is only used by ProofGeneral. There is no need to expose the broken internals of this command to the OCaml plugin developer.
-
Pierre-Marie Pédrot authored
-
coqbot-app[bot] authored
Reviewed-by: Alizter Co-authored-by:
Alizter <Alizter@users.noreply.github.com>
-
- 07 Aug, 2022 1 commit
-
-
coqbot-app[bot] authored
Reviewed-by: olaure01 Reviewed-by: Alizter Co-authored-by:
Alizter <Alizter@users.noreply.github.com>
-
- 06 Aug, 2022 5 commits
-
-
Andrej Dudenhefner authored
added stronger Nat.Div0, Nat.Lcm0 modules added stronger N.Div0, N.Lcm0 modules added stronger NExtraProp0 module type added NZDivSpec0 added measure_right_induction, measure_left_induction to NZOrder added measure_induction to NOrder removed rs'_rs'', rbase, A'A_right, ls_ls', ls'_ls'', lbase, A'A_left from NZOrder simplified NGcd proofs deprecated weak NGcd lemmas
-
Pierre-Marie Pédrot authored
-
Pierre-Marie Pédrot authored
All the recursive arguments were ignored already, so we enforce this statically in the type of patterns.
-
Pierre-Marie Pédrot authored
-
coqbot-app[bot] authored
Reviewed-by: SkySkimmer Co-authored-by:
SkySkimmer <SkySkimmer@users.noreply.github.com>
-
- 05 Aug, 2022 8 commits
-
-
Pierre-Marie Pédrot authored
We only perform one lookup into the environment to fetch the inductive block.
-
coqbot-app[bot] authored
Merge PR #16322: Addressing issue #4712 : keyword detection preserves contiguous characters forming a valid identifier subsequence Reviewed-by: proux01 Co-authored-by:
proux01 <proux01@users.noreply.github.com>
-
coqbot-app[bot] authored
Reviewed-by: gares Ack-by: Blaisorblade Ack-by: ppedrot Ack-by: silene Ack-by: SkySkimmer Ack-by: Alizter Co-authored-by:
gares <gares@users.noreply.github.com>
-
Pierre Roux authored
-
Pierre Roux authored
-
-
A contiguous sequence of characters must be fully inside or fully outside a keyword: no break of a keyword in the middle of a sequence of contiguous characters.
-
coqbot-app[bot] authored
Reviewed-by: proux01 Co-authored-by:
proux01 <proux01@users.noreply.github.com>
-
- 31 Jul, 2022 1 commit
-
-
Jim Fehrle authored
-
- 28 Jul, 2022 1 commit
-
-
coqbot-app[bot] authored
Reviewed-by: jfehrle Co-authored-by:
jfehrle <jfehrle@users.noreply.github.com>
-
- 27 Jul, 2022 3 commits
-
-
coqbot-app[bot] authored
Reviewed-by: jfehrle Co-authored-by:
jfehrle <jfehrle@users.noreply.github.com>
-
Valentin Robert authored
Fixing a misleading use of the old eventually/possibly false friend.
-
coqbot-app[bot] authored
Reviewed-by: SkySkimmer Co-authored-by:
SkySkimmer <SkySkimmer@users.noreply.github.com>
-
- 26 Jul, 2022 13 commits
-
-
coqbot-app[bot] authored
Reviewed-by: SkySkimmer Co-authored-by:
SkySkimmer <SkySkimmer@users.noreply.github.com>
-
coqbot-app[bot] authored
Reviewed-by: ejgallego Reviewed-by: Blaisorblade Co-authored-by:
ejgallego <ejgallego@users.noreply.github.com>
-
coqbot-app[bot] authored
Reviewed-by: ejgallego Reviewed-by: Blaisorblade Co-authored-by:
ejgallego <ejgallego@users.noreply.github.com>
-
coqbot-app[bot] authored
Reviewed-by: ejgallego Co-authored-by:
ejgallego <ejgallego@users.noreply.github.com>
-
Pierre-Marie Pédrot authored
-
Pierre-Marie Pédrot authored
This allows messing with the internals without impacting the callers. We observe in passing that two fields were never used outside of the Autorewrite internals.
-
Pierre-Marie Pédrot authored
This is a semantic-preserving cleanup.
-
Pierre-Marie Pédrot authored
We remove some exported functions that are now dead code.
-
Pierre-Marie Pédrot authored
-
Pierre-Marie Pédrot authored
No point in keeping this module around given that it was only used internally and in addition relying on dubious features because of the lack of a proper interface.
-
Pierre-Marie Pédrot authored
-
Pierre-Marie Pédrot authored
It was only used once with a single trivial instance.
-
Pierre-Marie Pédrot authored
These functions were eerily specific and not used anywhere else, it is thus better to seal them inside the one module that uses them.
-
- 25 Jul, 2022 2 commits
-
-
coqbot-app[bot] authored
Reviewed-by: SkySkimmer Co-authored-by:
SkySkimmer <SkySkimmer@users.noreply.github.com>
-
coqbot-app[bot] authored
Reviewed-by: ppedrot Co-authored-by:
ppedrot <ppedrot@users.noreply.github.com>
-