Add is_closed_term tactic

This MR adds a tactic that has been proven quite useful in RefinedC. An example usecase can be found here: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/4168f736be2fd735dc9680fda0a3b3a6af2b1b5e/theories/bitvector.v#L294 (There it is still called checked_closed).

added 5 commits

• 7d8088c2...78b6bc41 - 4 commits from branch master
• fb74bea1 - Add assert_closed tactic

Compare with previous version

Interesting. Some comments:

• I don't like the name. There's already Coq's assert tactic, and this one has nothing to do with that. Maybe something like is_closed or is_closed_term would be better?
• It would be good to explain in comments how this code works. The link to Zulip is nice for giving the initial author credit, but it would be better if the comments in the code are self-contained.
• I think there are some caveats. This tactic succeeds if the term depends on section variables, or axioms, or opaque terms. Is that correct? Can we do something about that?

added 1 commit

• a757d4e3 - Add assert_closed tactic

Compare with previous version

changed title from Add assert_closed tactic to Add is_closed_term tactic

added 5 commits

• a757d4e3...ea36eb94 - 4 commits from branch master
• 18280afe - Add is_closed_term tactic

Compare with previous version

added 1 commit

• 47b4b4ad - Add is_closed_term tactic

Compare with previous version

added 1 commit

• 602ca8a4 - Add is_closed_term tactic

Compare with previous version

added 1 commit

• decf292d - Apply 4 suggestion(s) to 1 file(s)

Compare with previous version

added 1 commit

• 5e1af28f - Add is_closed_term tactic

Compare with previous version

added 1 commit

• a8233857 - Add is_closed_term tactic

Compare with previous version

added 1 commit

• bba9ccaf - Add is_closed_term tactic

Compare with previous version

added 1 commit

• cc82d848 - Add is_closed_term tactic

Compare with previous version

Do you want to write a changelog entry?

added 1 commit

• 0088d876 - Add is_closed_term tactic

Compare with previous version

added 9 commits

• 0088d876...9135fcfe - 8 commits from branch master
• 5afe58c4 - Add is_closed_term tactic

Compare with previous version