The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Perhaps it's just a syntax error, if you put nat_ind at a place where  
a tactic is expected.

You should try to write something like :

exact (nat_ind ... ...)
or
apply nat_ind with ...
or
intros n; pattern; apply nat_ind.

Pierre


Quoting Patricia Peratto 
<psperatto AT vera.com.uy>:

> I want to prove (using nat_ind) the following proposition.
> I adjoin the proof I have written myself.
>
> Definition aux1b (n:nat) : forall m:nat,
> forall (e:n=m),S n = S m.
> nat_ind (fun n:nat =>
> (forall m:nat, forall e:n=m, S n = S m))
>
> (fun m:nat, fun e:O=m,
> (f_equal nat nat S O m e))
>
> (fun p:nat, fun q:(forall m:nat,
> forall e:p = m, S p = S m) =>
> (fun m2:nat =>
> (fun e2:(S p)=m2 =>
> (f_equal nat nat S (S p) m2 e2))))
> n.
>
> I have proved it using "induction" but I want to
> find the proof using nat_ind.
>
> I have gotten the following message:
>
> Error: The reference nat_ind was not found in the current environment.
>
> Someone can say me where I'm wrong?
>
> Regards
>
> Patricia