Ssreflect Users Discussion List

[<>]

Hello.

Is there a way to set Implicit Arguments so that it only takes effect
when unresolved wildcards are generalized (ssr's behavior), 
but does not when they generate a type error outright (Coq's behavior)?

Concretely, I want the following script to work, 
without setting Implicit Arguments. 

Variable a : nat.
Variable g: nat -> nat -> nat.
Variable p: nat -> Prop.

Axiom f_p: forall a1 a2, p a1 -> p a2 -> p (g a1 2).

Goal p a ->True.
 move => pa.
 have:= f_p pa.

This ML-like generalization would make my tactic script robust
against minor modifications of axioms, 
which I often do for better structuring the script; 
it is attractive for me to decrease the potential of painful bugs,
but I do not want to use Implicit Arguments otherwise,
since it could make the script fragile.

With best,
Keiko