The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

Hi,

A possibility is to use the refine tactic. Starting in proof mode,
giving the term value with refine and place holdeers and ending with 
definition in interactive mode. A little example:


Require Import ZArith.

Open Scope Z_scope.

Parameter Zdiv: forall (a b: Z), b<>0 -> Z.

Definition halft: Z.
refine (Zdiv 1 2 _).
auto with zarith.
Defined.