Commits on Jun 19, 2016
  1. Rebase on trunk, new syntax for Hint Cut.

    Also try to improve the subrelation_tac tactic
    to start with the resolution of the most constrained
    goals first, w/o affecting completeness thanks to goal
    committed Jun 19, 2016
Commits on Jun 18, 2016
  1. Fix rewriting under binders

    - guardedrew strategy was buggy
    - the relation on arguments of lambdas was made too dependent
      by default
    committed May 2, 2016
  2. Rewrite: refined treatment of applications

    The related_app_tac tactic tries to drive unification
    to avoid too dependent goals, and unsolvable unification
    Also set most definitions as volatile for simpl, so that
    the proof terms can be (greatly) simplified.
    committed May 2, 2016
  3. Rewrite: refine treatment of applications

    To get faster resolution of non-dependent cases.
    committed May 2, 2016
  4. Add test for Hint Cut

    committed May 2, 2016
  5. Indentation

    committed May 2, 2016
  6. More work in progress for dependent/relevant rewriting

    Now the tactic is relatively working on basic examples and much more general.
    It does:
    - Generation of evars and hypotheses for each rewrite
    proof, that can be used in dependent cases.
    - These hyps are now also used by the "app" rule to solve
    subgoals when looking at Related ? (f a) (f' a'). This
    changes the resolution algorithm quite a bit...
    - I switched back non-dependent products to use the impl/arrow
    - Tried to cleanup a bit the code of subterm, but this is not
    finished yet.
    committed Apr 30, 2016
  7. Add a variant of refine which does no typeclass resolution

    For use in implementing Hint Externs during typeclass resolution.
    committed Apr 30, 2016
  8. Change subrelation inst priority for iff/impl

    Would otherwise prefer subrelation iff impl over subrelation iff iff
    on a goal of the form subrelation iff ?X.
    committed Apr 23, 2016
  9. Add a debug flag to setoid_rewrite/rewrite_strat

    leaving the typeclass constraints as subgoals.
    committed Apr 23, 2016
  10. First working version with "full" rewriting under binders.

    This is not ideal yet, the strategy when going under binders
    is pretty ad-hoc, forcing to rewrite x to x' after the current
    strategy is done rewriting the body of a lambda.
    committed Apr 21, 2016
  11. Deactivate full rewriting under binders temporarily

    Add Ltac substitution for strategies ast's so that one can
    use them in Ltac. Add new StratSet constructor, not implemented
    yet. stdlib compiles.
    committed Apr 9, 2016
  12. Fix any/many/repeat semantics

    committed Apr 14, 2016
  13. Implement patterns for strategies

    Both a "pattern" tactic that can guard any strategy and an automatic
    inference of the pattern of a rewrite rule are available. Also implement
    optional "all occurences of the first instance" semantics for matching
    a lemma. They can of course be combined.
    committed Apr 8, 2016
  14. Strategical, generalized rewriting with equality

    Build a predicate instead of using congruence reasoning when
    possible. Can be mixed with general relations.
    committed Mar 9, 2016
  15. Add stm dir to .merlin

    committed Apr 6, 2016
  16. Fix priorities of pointwise_relation instances,

    They perturb the search for setoid_rewrite proofs which are more easy
    for @eq.
    Fix test-suite file: change due to different instances in standard library.
    committed Apr 6, 2016
  17. Fixing the checker.

    I had to remove code handling the -type-in-type option introduced by commit
    9c732a5. We should fix it at some point, but I am not sure that using the
    checker with a system known to be blatantly inconsistent makes much sense
    ppedrot committed Jun 18, 2016
  18. Test-suite fix to 1744e37 (injection in context).

    Preserve a compatibility whether the Structural Injection flag is on
    or not.
    herbelin committed Jun 18, 2016
  19. Backporting c064fb9 from 8.5 (another regression with Ltac trace repo…

    Doing it explicitly because it is in another file.
    herbelin committed Jun 18, 2016
  20. Adding an "as" clause to specialize.

    - The tactic specialize conveys a somehow intuitive reasoning concept
      and I would support continuing maintaining it even if the design
      comes in my opinion with some oddities. (Note that the experience of
      MathComp and SSReflect also suggests that specialize is an
      interesting concept in itself).
    There are two variants to specialize:
    - specialize (H args) with H an hypothesis looks natural: we
      specialize H with extra arguments and the "as pattern" clause comes
      naturally as an extension of it, destructuring the result using the
    - specialize term with bindings makes the choice of fully applying the
      term filling missing expressions with bindings and to then behave as
      generalize. Wouldn't we like a more fine-grained approach and the
      result to remain in the context?
      In this second case, the "as" clause works as if the term were posed
      in the context with "pose proof".
    herbelin committed Dec 21, 2015
  21. Giving a more natural semantics to injection by default.

    There were three versions of injection:
    1. "injection term" without "as" clause:
       was leaving hypotheses on the goal in reverse order
    2. "injection term as ipat", first version:
       was introduction hypotheses using ipat in reverse order without
       checking that the number of ipat was the size of the injection
       (activated with "Unset Injection L2R Pattern Order")
    3. "injection term as ipat", second version:
       was introduction hypotheses using ipat in left-to-right order
       checking that the number of ipat was the size of the injection
       and clearing the injecting term by default if an hypothesis
       (activated with "Set Injection L2R Pattern Order", default one from 8.5)
    There is now:
    4. "injection term" without "as" clause, new version:
       introducing the components of the injection in the context in
       left-to-right order using default intro-patterns "?"
       and clearing the injecting term by default if an hypothesis
       (activated with "Set Structural Injection")
    The new versions 3. and 4. are the "expected" ones in the sense that
    they have the following good properties:
    - introduction in the context is in the natural left-to-right order
    - "injection" behaves the same with and without "as", always
      introducing the hypotheses in the goal what corresponds to the
      natural expectation as the changes I made in the proof scripts for
      adaptation confirm
    - clear the "injection" hypothesis when an hypothesis which is the
      natural expectation as the changes I made in the proof scripts for
      adaptation confirm
    The compatibility can be preserved by "Unset Structural Injection" or
    by calling "simple injection".
    The flag is currently off.
    herbelin committed Dec 10, 2015
  22. Exporting a generic argument induction_arg. As a consequence,

    simplifying and generalizing the grammar entries for injection,
    discriminate and simplify_eq.
    herbelin committed Dec 20, 2015