Ssreflect Users Discussion List

[Georges Gonthier <>]

  It really is the same engine -- Coq's type inference engine, namely.
An Implicit Argument is just one that's automatically replaced by a wildcard 
before type inference does it's thing. The Unset Strict Implicit directive 
does help by making the assignment of the Implicit status more reliable: an 
argument is made implicit when it occurs in the type of another argument 
(Coq's default uses a complex heuristic to try to determine if the occurrence 
is rigid).

-- Georges

-----Original Message-----
From:  []
Sent: 02 July 2008 12:14
To: 
Subject: Re: RE: RE: wildcards insertion in the Specialising assumptions 
mechanism


> Obviously, you're not using Implicit Arguments; you REALLY should.

I have been avoiding using Implicit Arguments since I do not well-understand
when it succeeds or fails, (for instance it looked fragile about permutation
of arguments, which does not seem to change anything to me )
and since I do not like my tactics to fail
due to a reason that I do not understand;
it was another source of painful bugs,
i.e. to detect arguments that were not inferred.

It looks to me that ssr's inference engine is more robust,
so I thought I can try to rely on it. And if the same engine is available
for Implicit Arguments, I will try it too.

Thank you.

Best regards,
Keiko