Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk

(résolution entre autres des bugs 1882, 1883, 1884).



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

1 files changed, 24 insertions, 0 deletions

diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index e117bf62f..082cbfbe1 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -186,3 +186,27 @@ refine
 Abort.
 
 End Additions_while.
+
+(* Two examples from G. Melquiond (bugs #1878 and #1884) *)
+
+Parameter F1 G1 : nat -> Prop.
+Goal forall x : nat, F1 x -> G1 x.
+refine (fun x H => proj2 (_ x H)).
+Abort.
+
+Goal forall x : nat, F1 x -> G1 x.
+refine (fun x H => proj2 (_ x H) _).
+Abort.
+
+(* Remark: the following example does not succeed any longer in 8.2 because,
+   the algorithm is more general and does exclude a solution that it should
+   exclude for typing reason. Handling of types and backtracking is still to
+   be done
+
+Section S.
+Variables A B : nat -> Prop.
+Goal forall x : nat, A x -> B x.
+refine (fun x H => proj2 (_ x H) _).
+Abort.
+End S.
+*)