1 files changed, 136 insertions, 0 deletions
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index ad69ced1..082cbfbe 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -68,9 +68,145 @@ Proof. trivial. Qed.
 Hint Resolve contradiction.
 Goal False.
 eauto.
+Abort.
 
 (* This used to fail in V8.1beta because first-order unification was
    used before using type information *)
 
 Check (exist _ O (refl_equal 0) : {n:nat|n=0}).
 Check (exist _ O I : {n:nat|True}).
+
+(* An example (initially from Marseille/Fairisle) that involves an evar with
+   different solutions (Input, Output or bool) that may or may not be
+   considered distinct depending on which kind of conversion is used *)
+
+Section A.
+Definition STATE := (nat * bool)%type.
+Let Input := bool.
+Let Output := bool.
+Parameter Out : STATE -> Output.
+Check fun (s : STATE) (reg : Input) => reg = Out s.
+End A.
+
+(* The return predicate found should be: "in _=U return U" *)
+(* (feature already available in V8.0) *)
+
+Definition g (T1 T2:Type) (x:T1) (e:T1=T2) : T2 :=
+  match e with
+  | refl_equal => x
+  end.
+
+(* An example extracted from FMapAVL which (may) test restriction on
+   evars problems of the form ?n[args1]=?n[args2] with distinct args1
+   and args2 *)
+
+Set Implicit Arguments.
+Parameter t:Set->Set.
+Parameter map:forall elt elt' : Set, (elt -> elt') -> t elt -> t elt'.
+Parameter avl: forall elt : Set, t elt -> Prop.
+Parameter bst: forall elt : Set, t elt -> Prop.
+Parameter map_avl: forall (elt elt' : Set) (f : elt -> elt') (m : t elt),
+   avl m -> avl (map f m).
+Parameter map_bst: forall (elt elt' : Set) (f : elt -> elt') (m : t elt),
+   bst m -> bst (map f m).
+Record bbst (elt:Set) : Set := 
+  Bbst {this :> t elt; is_bst : bst this; is_avl: avl this}.
+Definition t' := bbst.
+Section B.
+Variables elt elt': Set.
+Definition map' f (m:t' elt) : t' elt' := 
+  Bbst (map_bst f m.(is_bst)) (map_avl f m.(is_avl)).
+End B.
+Unset Implicit Arguments.
+
+(* An example from Lexicographic_Exponentiation that tests the 
+   contraction of reducible fixpoints in type inference *)
+
+Require Import List.
+Check (fun (A:Set) (a b x:A) (l:list A) 
+  (H : l ++ cons x nil = cons b (cons a nil)) =>
+  app_inj_tail l (cons b nil) _ _ H).
+
+(* An example from NMake (simplified), that uses restriction in solve_refl *)
+
+Parameter h:(nat->nat)->(nat->nat).
+Fixpoint G p cont {struct p} :=
+  h (fun n => match p with O => cont | S p => G p cont end n).
+
+(* An example from Bordeaux/Cantor that applies evar restriction 
+   below  a binder *)
+
+Require Import Relations.
+Parameter lex : forall (A B : Set), (forall (a1 a2:A), {a1=a2}+{a1<>a2})
+-> relation A -> relation B -> A * B -> A * B -> Prop.
+Check 
+ forall (A B : Set) eq_A_dec o1 o2, 
+ antisymmetric A o1 -> transitive A o1 -> transitive B o2 ->
+ transitive _ (lex _ _ eq_A_dec o1 o2).
+
+(* Another example from Julien Forest that tests unification below binders *)
+
+Require Import List.
+Set Implicit Arguments.
+Parameter
+ merge : forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2})
+                         (eqB : forall (b1 b2 : B), {b1=b2}+{b1<>b2})
+                        (partial_res l : list (A*B)), option (list (A*B)).
+Axiom merge_correct :
+   forall (A B : Set) eqA eqB (l1 l2 : list (A*B)),
+       (forall a2 b2 c2, In (a2,b2) l2 -> In (a2,c2) l2 -> b2 = c2) ->
+       match merge eqA eqB l1 l2 with _ => True end.
+Unset Implicit Arguments.
+
+(* An example from Bordeaux/Additions that tests restriction below binders *)
+
+Section Additions_while.
+
+Variable A : Set.
+Variables P Q : A -> Prop.
+Variable le : A -> A -> Prop.
+Hypothesis Q_dec : forall s : A, P s -> {Q s} + {~ Q s}.
+Hypothesis le_step : forall s : A, ~ Q s -> P s -> {s' | P s' /\ le s' s}.
+Hypothesis le_wf : well_founded le.
+
+Lemma loopexec : forall s : A, P s -> {s' : A | P s' /\ Q s'}.
+refine
+  (well_founded_induction_type le_wf (fun s => _ -> {s' : A | _ /\ _})
+    (fun s hr i =>
+       match Q_dec s i with
+       | left _ => _
+       | right _ =>
+           match le_step s _ _ with
+           | exist s' h' =>
+               match hr s' _ _ with
+               | exist s'' _ => exist _ s'' _
+               end
+           end
+       end)).
+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.
+*)