New reflexive implementation of setoid_rewrite. The new implementation

introduces a few backward incompatibilities:
 1. setoid_replace used to try to close the new goal using full_trivial.
    The new implementation does not try to close the goal.
    To fix the script it is sufficient to add a "; [ idtac | trivial ]."
    after every application of setoid_replace that used to generate just
    one goal.
 2. (setoid_replace c1 c2) used to replace either c1 with c2 or c2 with c1
    (if c1 did not occur in the goal). The new implementation only replaces
    c1 with c2.
    To fix the script it is sufficient to replace
    (setoid_replace c1 with c2) with
    (setoid_replace c1 with c2) || (setoid_replace c2 with c1)
    in those cases where it is unknown what should be substituted with what.
 3. the goal generated by the "Add Morphism" command has the hypothesis
    permutated w.r.t. the old implementation. I.e. the old implementation
    used to generate: forall x1 x2, forall x3 x4, x1=x2 -> x3=x4 -> ...
    whereas the new implementation generates
     forall x1 x2, x1=x2 -> forall x3 x4, x3 = x4 -> ...
    Fixing the script is usually trivial.
 4. the "Add Morphism P" command used to generate a non-standard goal in the
    case of P being a predicate (i.e. a function whose codomain is Prop).
    In that case the goal ended with an implication (instead of ending with
    a coimplication). The new implementation generates a standard goal that
    ends with a coimplication.
    To fix the script you can add the following line at the very beginning:
     cut <<old_goal>>; intro Hold; split; apply Hold;
      assumption || (symmetry;assumption).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6049 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions