1 files changed, 0 insertions, 32 deletions
diff --git a/distrib/MacOS-X/ReadMe.rtf.template b/distrib/MacOS-X/ReadMe.rtf.template
deleted file mode 100644
index 2878e1c4d2..0000000000
--- a/distrib/MacOS-X/ReadMe.rtf.template
+++ /dev/null
@@ -1,32 +0,0 @@
-{\rtf1\mac\ansicpg10000\cocoartf100
-{\fonttbl\f0\fswiss\fcharset77 Helvetica;}
-{\colortbl;\red255\green255\blue255;}
-\margl1440\margr1440\vieww9000\viewh9000\viewkind0
-\pard\tx1440\tx2880\tx4320\tx5760\tx7200\ql\qnatural
-
-\f0\fs24 \cf0 Developed in the LogiCal project, the Coq tool is a formal\
-proof management system: a proof done with Coq is mechanically\
-checked by the machine. In particular, Coq allows:\
-\
-- the definition of functions or predicates,\
-- to state mathematical theorems and software specifications,\
-- to develop interactively formal proofs of these theorems,\
-- to check these proofs by a small certification "kernel".\
-\
-Coq is based on a logical framework called "Calculus of Inductive\
-Constructions" extended by a modular development system for\
-theories.\
-\
-Coq also includes\
-\
-- a mechanism for automatic generation of certified programs\
-  from proofs of their specifications\
-- a graphical user interface based on gtk (CoqIde)\
-  [not included in this package]\
-- a documentation tool (coqdoc)\
-- dependency and makefile generation tools for Coq (coq_makefile\
-  and coqdep)\
-- a preprocessor for TeX files that include Coq commands (coq-tex)\
-\
-Coq is written in the Objective Caml language.\
-}