1 files changed, 58 insertions, 11 deletions
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index a7b6d6d8..64875fba 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -1,23 +1,70 @@
 (* The "?" of cons and eq should be inferred *)
-Variable list:Set -> Set.
-Variable cons:(T:Set) T -> (list T) -> (list T).
-Check (n:(list nat)) (EX l| (EX x| (n = (cons ? x l)))).
+Variable list : Set -> Set.
+Variable cons : forall T : Set, T -> list T -> list T.
+Check (forall n : list nat, exists l : _, (exists x : _, n = cons _ x l)).
 
 (* Examples provided by Eduardo Gimenez *)
 
-Definition c [A;Q:(nat*A->Prop)->Prop;P] :=
-   (Q [p:nat*A]let (i,v) = p in (P i v)).
+Definition c A (Q : (nat * A -> Prop) -> Prop) P :=
+  Q (fun p : nat * A => let (i, v) := p in P i v).
 
 (* What does this test ? *)
-Require PolyList.
-Definition list_forall_bool  [A:Set][p:A->bool][l:(list A)] : bool := 
- (fold_right ([a][r]if (p a) then r else false) true l).
+Require Import List.
+Definition list_forall_bool (A : Set) (p : A -> bool) 
+  (l : list A) : bool :=
+  fold_right (fun a r => if p a then r else false) true l.
 
 (* Checks that solvable ? in the lambda prefix of the definition are harmless*)
-Parameter A1,A2,F,B,C : Set.
+Parameter A1 A2 F B C : Set.
 Parameter f : F -> A1 -> B.
-Definition f1 [frm0,a1]: B := (f frm0 a1).
+Definition f1 frm0 a1 : B := f frm0 a1.
 
 (* Checks that solvable ? in the type part of the definition are harmless *)
-Definition f2 : (frm0:?;a1:?)B := [frm0,a1](f frm0 a1).
+Definition f2 frm0 a1 : B := f frm0 a1.
 
+(* Checks that sorts that are evars are handled correctly (bug 705) *)
+Require Import List.
+
+Fixpoint build (nl : list nat) :
+ match nl with
+ | nil => True
+ | _ => False
+ end -> unit :=
+  match nl return (match nl with
+                   | nil => True
+                   | _ => False
+                   end -> unit) with
+  | nil => fun _ => tt
+  | n :: rest =>
+      match n with
+      | O => fun _ => tt
+      | S m => fun a => build rest (False_ind _ a)
+      end
+  end.
+
+
+(* Checks that disjoint contexts are correctly set by restrict_hyp *)
+(* Bug de 1999 corrigé en déc 2004 *)
+
+Check
+  (let p :=
+     fun (m : nat) f (n : nat) =>
+     match f m n with
+     | exist a b => exist _ a b
+     end in
+   p
+   :forall x : nat,
+    (forall y n : nat, {q : nat | y = q * n}) ->
+    forall n : nat, {q : nat | x = q * n}).
+
+(* Check instantiation of nested evars (bug #1089) *)
+
+Check (fun f:(forall (v:Set->Set), v (v nat) -> nat) => f _ (Some (Some O))).
+
+(* This used to fail with anomaly "evar was not declared" in V8.0pl3 *)
+
+Theorem contradiction : forall p, ~ p -> p -> False.
+Proof. trivial. Qed.
+Hint Resolve contradiction.
+Goal False.
+eauto.