The Coq mailing list

[Line Jakubiec-Jamet <jakubiec AT lif.univ-mrs.fr>]

   Hello,

I have a question about the synthesis of implicit parameters
in the case of a coercion. Suppose we have the following declarations:

  Parameters (A A1 : Prop) (A1_A : A1->A).
  Coercion A1_A:A1>->A.
  Parameters (P:A->Prop) (P1:A1->Prop).

We can define :

  Definition test1 := exists x, P1(x) /\ P(x).  (* x:A1 inferred *)

But the following definition fails (more exactly the synthesis
of the implicit parameter is not the one that I want):

  Definition test2 := exists x, P(x) /\ P1(x). (* x:A inferred and so 
P1(x) is not typable*)

In order to avoid this problem, is there an easy way to infer 
automatically the right type?


Thanks for help,

 Line



--
(**********************************************************)
(* Line Jakubiec-Jamet                                    *)
(* Laboratoire d'Informatique Fondamentale de Marseille   *)
(* Université de la Méditerranée (Aix-Marseille II)       *)
(* Faculté des Sciences de Luminy                         *)
(* 163, Avenue de Luminy                                  *)
(* 13288 - MARSEILLE Cedex 9                              *)
(**********************************************************)