The Coq mailing list

[Ismael Figueroa <ifigueroap AT gmail.com>]

Hi club,

Apologies if this is not the right venue for this kind of questions

I installed Coq 8.4pl5 using Homebrew (brew install coq), but for some reason I cannot use the admit tactic. As far as I understand, admit is now built-in in Coq. I asked a colleague to check if it was available and indeed it was working on his machine, hence I assume it is some weird installation issue... Can anyone please point me to where is the issue happening?

I attach a small file with my interaction with coqtop and the actual error message.

Thanks

--

Ismael

ismael@Macintosh:~$ coqtop -v
The Coq Proof Assistant, version 8.4pl5 (February 2015)
compiled on Feb 24 2015 11:29:56 with OCaml 4.02.1

ismael@Macintosh:~$ coqtop -config
LOCAL=0
COQLIB=/usr/local/lib/coq/
DOCDIR=/usr/local/Cellar/coq/8.4pl5/share/doc/coq/
OCAMLDEP=ocamldep
OCAMLC=ocamlc
OCAMLOPT=ocamlopt
OCAMLDOC=ocamldoc
CAMLBIN=/usr/local/bin/
CAMLLIB=/usr/local/lib/ocaml/
CAMLP4=camlp5
CAMLP4BIN=/usr/local/bin/
CAMLP4LIB=/usr/local/Cellar/camlp5/6.12_2/lib/ocaml/camlp5
HASNATDYNLINK=true

ismael@Macintosh:~$ coqtop
Welcome to Coq 8.4pl5 (February 2015)

Coq < Definition foo (a:nat) (b:nat): nat := admit.
Toplevel input, characters 39-44:
> Definition foo (a:nat) (b:nat): nat := admit.
>                                        ^^^^^
Error: The reference admit was not found in the current environment.

Coq < Definition admit {T: Type} : T. Admitted.
1 subgoal
  
  T : Type
  ============================
   T

admit is assumed

Coq < Definition foo (a:nat) (b:nat): nat := admit.
foo is defined

Coq <