diff options
| author | corbinea | 2004-03-14 20:55:58 +0000 |
|---|---|---|
| committer | corbinea | 2004-03-14 20:55:58 +0000 |
| commit | f41384ca3cb83167e80c4f2ed6daf80cad44fe80 (patch) | |
| tree | bf6704dbe512e172b4178cd48e7fc15bb68fc006 /contrib/cc/README | |
| parent | aa2e7f2a10323c73660c6a07eb493fdad42f1597 (diff) | |
minor changes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5480 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/cc/README')
| -rw-r--r-- | contrib/cc/README | 8 |
1 files changed, 5 insertions, 3 deletions
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. |