From 7d220f8b61649646692983872626d6a8042446a9 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 20 Mar 2009 01:22:58 +0000
Subject: Directory 'contrib' renamed into 'plugins', to end confusion with
 archive of user contribs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/cc/README | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 plugins/cc/README

(limited to 'plugins/cc/README')

diff --git a/plugins/cc/README b/plugins/cc/README
new file mode 100644
index 000000000..073b140ea
--- /dev/null
+++ b/plugins/cc/README
@@ -0,0 +1,20 @@
+
+cctac: congruence-closure for coq
+
+author: Pierre Corbineau, 
+	Stage de DEA au LSV, ENS Cachan
+	Thèse au LRI, Université Paris Sud XI 
+
+Files :
+
+- ccalgo.ml : congruence closure algorithm
+- ccproof.ml : proof generation code
+- cctac.ml4 : the tactic itself
+- CCSolve.v : a small Ltac tactic based on congruence 
+
+Known Bugs : the congruence tactic can fail due to type dependencies.
+
+Related documents:
+	Peter J. Downey, Ravi Sethi, and Robert E. Tarjan.
+	Variations on the common subexpression problem.
+	JACM, 27(4):758-771, October 1980.	
-- 
cgit v1.2.3