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

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

Fixes #16152: Deduplicate rewrite hints imported multiple times.

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.

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

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

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

All the recursive arguments were ignored already, so we enforce this
statically in the type of patterns.

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

We only perform one lookup into the environment to fetch the inductive block.

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>

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>

Hugo Herbelin authored Jul 15, 2022 and Pierre Roux committed Aug 05, 2022

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.

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

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

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

Fixing a misleading use of the old eventually/possibly false friend.

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

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

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

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

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

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.

This is a semantic-preserving cleanup.

We remove some exported functions that are now dead code.

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.

It was only used once with a single trivial instance.

These functions were eerily specific and not used anywhere else, it is thus
better to seal them inside the one module that uses them.

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

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