diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
| commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
| tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /contrib/cc/README | |
| parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) | |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'contrib/cc/README')
| -rw-r--r-- | contrib/cc/README | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/contrib/cc/README b/contrib/cc/README deleted file mode 100644 index 073b140e..00000000 --- a/contrib/cc/README +++ /dev/null @@ -1,20 +0,0 @@ - -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. |