Quelques bricoles autour de l'unification:

- Un patch pour le bug de non vérification du typage de Stéphane L.
- Changement du fameux message "cannot solve a second-order matching problem"
  en espérant, à défaut de savoir résoudre plus souvent le problème, que
  le message est plus explicite.
- Divers changements cosmétiques.



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

1 files changed, 12 insertions, 0 deletions

diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 3b4e8af21f..e3fed09e7d 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -174,3 +174,15 @@ Axiom ax : forall (A : Set) (R : A -> A -> Prop) (x y : A), R x y.
 Theorem t : r true false.
 apply ax with (R := r).
 Qed.
+
+
+(* Check verification of type at unification (Submitted by Stéphane Lengrand)
+   (without verification, the first "apply" works which leads to wrongly
+   instantiate x by Prop) *)
+
+Theorem t: ~(forall x:Prop, ~x).
+unfold not.
+intro.
+eapply H.
+apply (forall B:Prop,B->B) || (instantiate (1:=True); exact I).
+Defined.