From 654133b47df896e4ca074502aa5dcf74f8beac30 Mon Sep 17 00:00:00 2001
From: notin
Date: Fri, 9 Jun 2006 16:59:42 +0000
Subject: Suppression du répertoire distrib: il fait désormais partie du projet
 coq-dev-tools sur GForge

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8943 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 distrib/MacOS-X/ReadMe.rtf.template | 32 --------------------------------
 1 file changed, 32 deletions(-)
 delete mode 100644 distrib/MacOS-X/ReadMe.rtf.template

(limited to 'distrib/MacOS-X/ReadMe.rtf.template')

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.\
-}
-- 
cgit v1.2.3