The Coq mailing list

[Pierre CASTERAN <Pierre.Casteran AT labri.u-bordeaux.fr>]

Hello,

  Which is the criterium with respect to which we can use the
"?" joker for typing ?

 If i try :

  Check [i:?](S (S i)).

 I get the message :

 Error: The term [i:?](S (S i)) failed to typecheck:
 unconstrained isevar

 instead of the "nat->nat" i was expecting.

 Is it impossible for Coq to use a Milner-like typing procedure which
 uses the typings of free variables ?

Best Regards,
Pierre