CMU Artificial Intelligence Repository
Home INFO Search FAQs Repository Root

Coq: Calculus of Inductive Constructions

areas/reasonng/atp/systems/coq/
This directory contains Coq, the Calculus of Inductive Constructions.
See Also: 

   lang/others/ml/caml_lt/
Origin:   

   ftp.inria.fr:/INRIA/coq/V5.8.3 (unix version)
   ftp.inria.fr:/INRIA/coq/V5.8.2 (mac version)

Version: Unix 5.8.3 (6-DEC-93); Mac 5.8.2 (8-JUL-93) Requires: Caml-Light, C, X11 The Mac version is standalone, not requiring Caml-Light. The unix version requires Caml-Light. Ports: Unix, Macintosh CD-ROM: Prime Time Freeware for AI, Issue 1-1 Contact: Coq hotline . Keywords: Automated Reasoning, Coq, ML!Code, Reasoning!Automated Reasoning, Theorem Proving References: Documentation is included in the distribution.
Last Web update on Mon Feb 13 10:27:27 1995
AI.Repository@cs.cmu.edu