Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Shrink Proofs/Obligations by default and deprecate option #218

Closed
wants to merge 13 commits into from
Closed

Shrink Proofs/Obligations by default and deprecate option #218

wants to merge 13 commits into from

Commits on Jun 27, 2016

  1. Fix apparent off-by-1 bug in coq_makefile

    @mattam82
    mattam82 committed Jun 27, 2016
    Configuration menu
    Copy the full SHA
    acb40a0 View commit details
    Browse the repository at this point in the history

  2. Typeclasses: mark unresolvable goals in new implementation

    @mattam82
    mattam82 committed Jun 27, 2016
    Configuration menu
    Copy the full SHA
    6ffb187 View commit details
    Browse the repository at this point in the history

  3. Typeclasses: fix treatment of exceptions in compat

    @mattam82
    mattam82 committed Jun 27, 2016
    Configuration menu
    Copy the full SHA
    0ce92e8 View commit details
    Browse the repository at this point in the history

  4. Shrink Proofs/Obligations by default and deprecate 

    Fix bug in Shrink obligations with Program in the process.
    @mattam82
    mattam82 committed Jun 27, 2016
    Configuration menu
    Copy the full SHA
    4952664 View commit details
    Browse the repository at this point in the history

  5. Fix implementation of shrink for abstract proofs 

    - Update doc in term.mli to reflect the fact that let-in's
  are part of what is returned by [decompose_lam_assum].
    @mattam82
    mattam82 committed Jun 27, 2016
    Configuration menu
    Copy the full SHA
    6967e85 View commit details
    Browse the repository at this point in the history

  6. Add Unset Shrink Abstract/Obligations in Coq85 

    For compatibility with 8.5.
    @mattam82
    mattam82 committed Jun 27, 2016
    Configuration menu
    Copy the full SHA
    2056e54 View commit details
    Browse the repository at this point in the history

  7. Update CHANGES and COMPATIBILITY

    @mattam82
    mattam82 committed Jun 27, 2016
    Configuration menu
    Copy the full SHA
    3b594da View commit details
    Browse the repository at this point in the history

  8. Rework treatment of default transparency of obligations 

    By default obligations defined by tactics are defined
transparently or opaque according to the Obligations Transparent flag,
except proofs of subset obligations which are treated
as opaque by default. When the user proves the obligation using
Qed or Defined, this information takes precedence, and only
when the obligation cannot be Qed'ed because it contains
references to a recursive function an error is raised
(this prevents the guardness checker error).
Shrinked obligations were not doings this correctly.
    @mattam82
    mattam82 committed Jun 27, 2016
    Configuration menu
    Copy the full SHA
    6140d62 View commit details
    Browse the repository at this point in the history

  9. Fix semantics of obligation status. 

    Forcing transparency due to fixpoint prototypes
takes precedence over the user preference.
    @mattam82
    mattam82 committed Jun 27, 2016
    Configuration menu
    Copy the full SHA
    e12e74b View commit details
    Browse the repository at this point in the history

  10. Program: refine shrinking of obligations 

    Ensure correspondence between the term and type to shrink, so that Lets
are preserved when they are used relevantly in either of them.  This
avoids e.g. "simpl" in the shrinked hypotheses to reduce shrinking,
while maintaining unsimplified types in the type of the shrinked
obligations (for compatibility).
    @mattam82
    mattam82 committed Jun 27, 2016
    Configuration menu
    Copy the full SHA
    4109c88 View commit details
    Browse the repository at this point in the history

  11. Program: do not force opacity of subset proofs 

    This maintains compatibility.
    @mattam82
    mattam82 committed Jun 27, 2016
    Configuration menu
    Copy the full SHA
    ea7336d View commit details
    Browse the repository at this point in the history

  12. Update COMPATIBILITY

    @mattam82
    mattam82 committed Jun 27, 2016
    Configuration menu
    Copy the full SHA
    4a0eecd View commit details
    Browse the repository at this point in the history

  13. Simplify Lambda, Prod case of shrinking 

    By invariant (we start with a term and its type), the abstraction's
types correspond.
    @mattam82
    mattam82 committed Jun 27, 2016
    Configuration menu
    Copy the full SHA
    8f686e6 View commit details
    Browse the repository at this point in the history