From f41384ca3cb83167e80c4f2ed6daf80cad44fe80 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Sun, 14 Mar 2004 20:55:58 +0000
Subject: minor changes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5480 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/cc/README | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'contrib/cc/README')

diff --git a/contrib/cc/README b/contrib/cc/README
index f19820d32b..073b140eae 100644
--- a/contrib/cc/README
+++ b/contrib/cc/README
@@ -1,16 +1,18 @@
 
 cctac: congruence-closure for coq
 
-author: Pierre Corbineau, Stage de DEA au LSV, ENS Cachan 
+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
-- CC.v : a few lemmas to handle eq/eqT conversions and congruence
+- CCSolve.v : a small Ltac tactic based on congruence 
 
-Known Bugs : CC tactic can fail due to type dependencies.
+Known Bugs : the congruence tactic can fail due to type dependencies.
 
 Related documents:
 	Peter J. Downey, Ravi Sethi, and Robert E. Tarjan.
-- 
cgit v1.2.3