… allowing projections themselves to be made opaque

Reviewed-by: ppedrot
Ack-by: Janno
Ack-by: herbelin
Ack-by: jfehrle
Ack-by: SkySkimmer
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

… allowing projections themselves to be made opaque

Reviewed-by: ppedrot
Ack-by: Janno
Ack-by: herbelin
Ack-by: jfehrle
Ack-by: SkySkimmer
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

… allowing projections themselves to be made opaque

Reviewed-by: ppedrot
Ack-by: Janno
Ack-by: herbelin
Ack-by: jfehrle
Ack-by: SkySkimmer
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

… allowing projections themselves to be made opaque

Reviewed-by: ppedrot
Ack-by: Janno
Ack-by: herbelin
Ack-by: jfehrle
Ack-by: SkySkimmer
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

… allowing projections themselves to be made opaque

Reviewed-by: ppedrot
Ack-by: Janno
Ack-by: herbelin
Ack-by: jfehrle
Ack-by: SkySkimmer
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

… allowing projections themselves to be made opaque

Reviewed-by: ppedrot
Ack-by: Janno
Ack-by: herbelin
Ack-by: jfehrle
Ack-by: SkySkimmer
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

… allowing projections themselves to be made opaque

Reviewed-by: ppedrot
Ack-by: Janno
Ack-by: herbelin
Ack-by: jfehrle
Ack-by: SkySkimmer
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

… allowing projections themselves to be made opaque

Reviewed-by: ppedrot
Ack-by: Janno
Ack-by: herbelin
Ack-by: jfehrle
Ack-by: SkySkimmer
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

… allowing projections themselves to be made opaque

Reviewed-by: ppedrot
Ack-by: Janno
Ack-by: herbelin
Ack-by: jfehrle
Ack-by: SkySkimmer
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

… allowing projections themselves to be made opaque

Reviewed-by: ppedrot
Ack-by: Janno
Ack-by: herbelin
Ack-by: jfehrle
Ack-by: SkySkimmer
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

… allowing projections themselves to be made opaque

Reviewed-by: ppedrot
Ack-by: Janno
Ack-by: herbelin
Ack-by: jfehrle
Ack-by: SkySkimmer
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

* Changes for compatibility with 8.19

* Adapt files for the build process

* Update README.md

* Don't use opam to build and install for now

* Adapt dune files to make build with dune possible

* Change name field in dune file to Waterproof

* Revert to dune language 3.6

* Remove line on theory Ltac2

* Adapt to rocq-prover/rocq#17836 (sort poly)

* Revert "Adapt to rocq-prover/rocq#17836 (sort poly)"

* Adapt to rocq-prover/rocq#18174 (Clenv.unify takes cv_pb)

* Adapt to rocq-prover/rocq#17836 (sort poly) (#28)

* Adapt to rocq-prover/rocq#18280 (case relevance outside case info) (#37)

* Merge features of version 2.1.1 into coq-master (#46)

* [build] Initial port to Dune

This was done at the interest of Vincent WENDLING for jsCoq use.

The setup is fairly standard, other than excluding the deprecated
dir (which doesn't compile)

* Update README.md

* Update dune file in theories

* Change importing Ltac2 modules and build only with dune

* Update version numbers

* Restore changes file and rename license file

* Fix metadata in files

* Add template tags

* Add @install, minimal dune version, dev-repo to opam file

* Added infrastructure for enforcing users to mention use of definitions.

* Removed some unnecessary lemma's and corresponding tactics (that were apparently throwing errors anyway).

* Restored old lemmas in 'SupAndInf' necessary for keeping limsup file working. To be rewritten in future.

* Moved tests in SupAndInf.v file to separate test file. Small bug fix in rewrite rule sup and infimum.

* 'We need to show'-tactic now also accepts equivalent goals. Added 'By ...' clause to allow for an additional lemma from which equivalence follows.

* Replaced use of 'it suffices to show' by 'we need to show' for unfolding definitions.

* Added testcases new behaviour tactic.

* Improved feedback given new restricted proof automation.

* Updated documentation.

* Small change in error message.

* Moved 'AutomationFailure' exception type to 'Wateprove' file.

* Improved feedback 'ItHolds' for new restricted proof automation.

* Replaced custom error shielded goal by standard error that can be caught using Ltac2.

* Added 'Since ...' clause as alternative to 'By ...' that accepts statements instead of references. (No 'Since ... we need to show ...' because the 'By'-version is to be removed soon. )

* Removed acceptation equivalent goals from 'We need to show' tactic.

* Improved feedback 'By ... we conclude ...' for new restricted automated proof finding. Added 'Since ... we conclude that ...' alternative.

* Improved feedback, now it says which part of a chain of (in)equalities it failed to prove. Refactored checking whether additional lemma is actually used: now check is done in 'Waterprove.v', it throws errors with relevant information that other tactics use to display user-readable errors.

* 'Contradiction' now tries to find a contradiction to the previous statement.

* Moved 'Obtain' tactic to separate file.

* Simplified old notation 'Obtain' tactic. Now it automatically tries to destruct previous statement and users no longer need to specify the corresponding property.

* Simplified names for hypotheses not labeled by user.

* Added 'change' to 'Expand definition', so putting in different dummy variables actually has effect.

* Added StateGoal wrappers to subgoals of non-natural induction.

* Added workaround for unexpected anomalies in restricted automation.

* Strengthened workaround. Both to prevent more anomalies with hypotheses and to prevent endless searching for proof with hypothesis because it is used implicitly by the 'assumption' tactic.

* Replaced axiomatic definitions with locked ones. Also strengthened shielded automation to depth 3 to be able to use definition supremum..

* Fixed dune build.

* feat: add warnings

* refactor: change the names of the warning functions

* feat: add error function

* Add files to _CoqProject.in

* feat: use the warning in Conclusion.v

* feat: deal with Rabs Rmax Rmin more easily by destructing them

* Readded shortened 'Obtain accoriding to ...' tactic.

* Reworked shielding to use Shorten database type. Includes new tactics for explicitly unfolding definitions, optimized for speed automation (i.e. they explicitly fail to prevent large growth search tree).

* Improved expanding def for sup and inf.

* Implemented user-level error throwing in tactics.

* Fixed small error from merge.

* Disabled debug mode automation.

* Reverted back to old SupAndInf.v file.

* Replaced wrapping after 'Expand the definition of ...' by throwing errors suggesting user to replace the line by a tactic with a similar effect as unfolding the definitions. (Also slightly simplified notation base case natural induction.)

* Added tactic for unfolding that prints a message instead of throwing an errror. For internal use by Waterproof editor only.

* chore: bump version number

* fix: add internal unfold for general terms and tests for internal unfold

* Hint fixes (#30)

fix: change hint priorities

* Automation debug (#31)

* fix: change hint priorities

* fix: change hint priorities

* fix: fight line endings

* feat: add switch for debugging of the automation

* feat: Add description on how to enable debugging to readme

* feat: use N1 instead of N in definition convergence

* Improve either (#32)

* fix: definition of divergence to infinity and min infinity

* feat: add double_is_even to wp_integers rather than subsequences

* feat: let either work with uninformative or if the goal is a prop

* feat: also separate either code for prop for three statements. Refactor some decidability statements

* refactor: use new either code in alternative characterization of continuity in R

* feat: add alternative characterization continuity for natural numbers as subset of metric space of reals

* feat: some adaptations for the continuity exercises

* chore: update changelog and bump version number in opam file

* Tactics for using strong induction to define index sequence (#33)

* Added strong induction for defining index sequence. Warning: uses fixed letters 'n' and 'k' for index sequence and induction variable.

* Removed 'Check' and 'Print's.

* Removed old code.

* Show version number (#34)

* feat: Add tactic to show version number

* fix: Add version file to _CoqProject.in

* Allow testing against a folder with dune's runtest and set version number (#35)

* feat: add exercises as dune test

* feat: add python script for testing

* feat: abstract the testing scripts and deal with errors better

* fix: call the correct test script

* Set Help to use default automation system. (#36)

* Change required version number

* Try to fix coq requirement

* Fix for problems with strong induction for defining index sequence. (#38)

* Fix for problems with strong induction for defining subsequence.

* Updated formatting goal wrapper.

* fix: some small fixes to be compatible with dev

* fix: change order fold_right arguments in index sequence

* fix: Small changes to the sequences and subsequences files because autorewrite no longer seems to work as before

* chore: Change version number

* try to allow for dev version

* fix: try with version numbers

* fix: try to fix version numbers

* fix: Remove unnecessary import in Sequences.v

* feat: add logging sentence for wp_autorewrite

* feat: add logging sentence for wp_autorewrite (#43)

* feat: create option to print rewrite hints (#44)

* fix: Fix autorewrite (the env variable didn't come through properly)

* fix: Compatibility with compilers >= 4.09.0 (#45)

* fix: Exclude s390x architecture

* refactor: put *.install and *.diags in gitignore

---------

Co-authored-by: Emilio Jesus Gallego Arias
Co-authored-by: Jelle

* Adapt to rocq-prover/rocq#18327 (projection opacity) (#41)

* Adapt to rocq-prover/rocq#18529 (no Dyn.anonymous) (#47)

* Adapt to rocq-prover/rocq#18624 (Tac2ffi / Tac2val split) (#49)

* Adapt to rocq-prover/rocq#18546. (#48)

* Adapt to rocq-prover/rocq#18880 (#52)

* Adapt to rocq-prover/rocq#18938 (EConstr.ERelevance) (#53)

* Update README.md

Update installation instructions

* Testmaster (#54)

Implement a better way to do a case analyse on a type

Co-authored-by: DikieDick

* fix: Change 'Variable' to 'local Parameter'

* feat: add a test for awp_autorewrite from coq-master

* Refactor: incorporate some changes from 8.17 and update version numbers (#57)

* [build] Fix use of plugin aliases in findlib loading. (#58)

Note that both lines where loading the same plugin, but activating
different syntax rules; that's not really allowed as it leaves the
system in a partial state. If something like that is needed, true two
plugins are necessary (Which is not hard to support nowadays).

* feat: Postponing choices in the Choose tactic (#59)

* Merge 8.17 into main (#61)

Main change according to (PR #58): we only declare one plugin now.

* Renamed variables to prevent having  actual exercise solution in repo (#64)

* Specialize (#51)

* feat: first version of waterproof specialize tactic

* feat: Improve new specialize tactic, so it throws an error when a wrong variable is getting introduced.

* Avoid doubling hypothesis, allow for multiple binders, prevent matching on functions, rename hypothesis to user-specified one

---------

Co-authored-by: Jelle <jellewemmenhove@live.nl>

* feat: Postponing choices in the Choose tactic

* No longer rename variables in exists-statements

---------

Co-authored-by: Jelle <jellewemmenhove@live.nl>

---------

Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Co-authored-by: Rodolphe Lepigre <lepigre@mpi-sws.org>
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org>
Co-authored-by: Jelle <jellewemmenhove@live.nl>