coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Mandy Martino <tesleft AT hotmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] make error for geocoq
Date: Fri, 11 Dec 2015 19:08:02 +0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tesleft AT hotmail.com; spf=Pass smtp.mailfrom=tesleft AT hotmail.com; spf=None smtp.helo=postmaster AT BAY004-OMC1S16.hotmail.com
Importance: Normal
Ironport-phdr: 9a23:Wel87xXiawbS5hap52uLt0jcPHrV8LGtZVwlr6E/grcLSJyIuqrYZhGFt8tkgFKBZ4jH8fUM07OQ6PC+HzRYqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh770o8WbSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6Lpyv/JHBO/xeL19RrhFBhwnNXo07Yvlr1OLGQCI/z4XVngcuhtOGQnMqh/gCMTfqCz/48903iWLdej/V6w1XzPqu7tmUxvlhjsvNzkl9WjWjop7i6cN80HpnAB234OBONLdD/F5ZK6IJd4=

martin@ubuntu:~/geo/GeoCoq$ git clone https://github.com/GeoCoq/GeoCoq

martin@ubuntu:~/geo/GeoCoq$ ./configure.sh

martin@ubuntu:~/geo/GeoCoq$ make

make: ocamlc.opt: Command not found

coqc -q -R . GeoCoq Tarski_dev/Ch02_cong

File "/home/martin/geo/GeoCoq/Tarski_dev/Ch02_cong.v", line 90, characters 13-31:

Error: Cannot infer the implicit parameter M of

cong_commutativity.

Could not find an instance for "Tarski_neutral_dimensionless".

make: *** [Tarski_dev/Ch02_cong.vo] Error 1

Regards,

Martin

[Coq-Club] make error for geocoq, Mandy Martino, 12/11/2015
- Re: [Coq-Club] make error for geocoq, Julien Narboux, 12/12/2015
  - [Coq-Club] Add Load Path however still can not find library, Mandy Martino, 12/20/2015
    - Re: [Coq-Club] Add Load Path however still can not find library, Abhishek Anand, 12/20/2015