This commit introduces changes in induction and destruct.

The main change is that selection of subterm is made similar whether
the given term is fully applied or not.
- The selection of subterm now works as follows depending on whether
  the "at" is given, of whether the subterm is fully applied or not,
  and whether there are incompatible subterms matching the pattern. In
  particular, we have:
  "at" given
  | subterm fully applied
  | | incompatible subterms
  | | |
  Y Y - it works like in 8.4
  Y N - this was broken in 8.4 ("at" was ineffective and it was finding
        all subterms syntactically equal to the first one which matches)
  N Y Y it now finds all subterms like the first one which matches
        while in 8.4 it used to fail (I hope it is not a too risky in-draft
        for a semantics we would regret...) (e.g. "destruct (S _)" on
        goal "S x = S y + S x" now selects the two occurrences of "S x"
        while it was failing before)
  N Y N it works like in 8.4
  N N - it works like in 8.4, selecting all subterms like the
        first one which matches
- Note that the "historical" semantics, when looking for a subterm, to
  select all subterms that syntactically match the first subterm to
  match the pattern (looking from left to right) is now internally called
  "like first".
- Selection of subterms can now find the type by pattern-matching (useful e.g.
  for "induction (nat_rect _ _ _ _)")
- A version of Unification.w_unify w/o any conversion is used for
  finding the subterm: it could be easily replaced by an other
  matching algorithm.

In particular, "destruct H" now works on a goal such as "H:True -> x<=y |- P y".

Secondary change is in the interpretation of terms with existential
variables:
- When several arguments are given, interpretation is delayed at the
  time of execution
- Because we aim at eventually accepting "edestruct c" with unresolved
  holes in c, we need the sigma obtained from c to be an extension of
  the sigma of the tactics, while before, we just type-checked c
  independently of the sigma of the tactic
- Finishing the resolution of evars (using type classes, candidates,
  pending conversion problems) is made slightly cleaner: it now takes
  three states: a term is evaluated in state sigma, leading to state
  sigma' >= sigma, with evars finally solved in state sigma'' >=
  sigma'; we solve evars in the diff of sigma' and sigma and report
  the solution in sigma''
- We however renounce to give now a success semantics to "edestruct c"
  when "c" has unresolved holes, waiting instead for a decision on
  what to do in the case of a similar eapply (see mail to coqdev).

An auxiliary change is that an "in" clause can be attached to each component
of a "destruct t, u, v", etc.

Incidentally, make_abstraction does not do evar resolution itself any longer.

2 files changed, 85 insertions, 7 deletions

diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 48927b6cc3..314b612e1c 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -98,25 +98,105 @@ Abort.
 
 Goal exists x, S x = S 0.
 eexists.
-Fail destruct (S _). (* Incompatible occurrences *)
+destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *)
+change (0 = S 0).
 Abort.
 
 Goal exists x, S 0 = S x.
 eexists.
-Fail destruct (S _). (* Incompatible occurrences *)
+destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *)
+change (0 = S ?x).
 Abort.
 
 Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n.
 do 2 eexists.
-Fail destruct (_, S _). (* Was succeeding at some time in trunk *)
-Show Proof.
+destruct (_, S _). (* Was unifying at some time in trunk, now takes the first occurrence *)
+change ((n, n0) = (S ?p, S ?p) /\ ?p = ?n0).
+Abort.
 
 (* Avoid unnatural selection of a subterm larger than expected *)
 
 Goal let g := fun x:nat => x in g (S 0) = 0.
 intro.
 destruct S.
-(* Check that it is not the larger subterm "f (S 0)" which is
+(* Check that it is not the larger subterm "g (S 0)" which is
    selected, as it was the case in 8.4 *)
 unfold g at 1.
 Abort.
+
+(* Some tricky examples convenient to support *)
+
+Goal forall x, nat_rect (fun _ => nat) O (fun x y => S x) x = nat_rect (fun _ => nat) O (fun x y => S x) x.
+intros.
+destruct (nat_rect _ _ _ _).
+Abort.
+(* Check compatibility in selecting what is open or "shelved" *)
+
+Goal (forall x, x=0 -> nat) -> True.
+intros.
+Fail destruct H.
+edestruct H.
+- reflexivity.
+- exact Logic.I.
+- exact Logic.I.
+Qed.
+
+(* Check an example which was working with case/elim in 8.4 but not with
+   destruct/induction *)
+
+Goal forall x, (True -> x = 0) -> 0=0. 
+intros.
+destruct H.
+- trivial.
+- apply (eq_refl x).
+Qed.
+
+(* Check an example which was working with case/elim in 8.4 but not with
+   destruct/induction (not the different order between induction/destruct) *)
+
+Goal forall x, (True -> x = 0) -> 0=0. 
+intros.
+induction H.
+- apply (eq_refl x).
+- trivial.
+Qed.
+
+(* This test assumes that destruct/induction on non-dependent hypotheses behave the same
+   when using holes or not
+
+Goal forall x, (True -> x = 0) -> 0=0. 
+intros.
+destruct (H _).
+- apply I.
+- apply (eq_refl x).
+Qed.
+*)
+
+(* Check destruct vs edestruct *)
+
+Goal forall x, (forall y, y = 0 -> x = 0) -> 0=0.
+intros.
+Fail destruct H.
+edestruct H.
+- trivial.
+- apply (eq_refl x).
+Qed.
+
+Goal forall x, (forall y, y = 0 -> x = 0) -> 0=0.
+intros.
+Fail destruct (H _).
+edestruct (H _).
+- trivial.
+- apply (eq_refl x).
+Qed.
+
+Goal forall x, (forall y, y = 0 -> x = 0) -> 0=0.
+intros.
+Fail destruct (H _ _).
+(* Now a test which assumes that destruct/induction on non-dependent hypotheses behave the same
+   when using holes or not
+edestruct (H _ _).
+- trivial.
+- apply (eq_refl x).
+Qed.
+*)
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 4e20a50774..1c2a6a0f2f 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -73,5 +73,3 @@ intros.
 induction x as [y * IHx].
 change (x = x) in IHx. (* We should have IHx:x=x *)
 Abort.
-
-