2
cctac: congruence-closure for coq
4
author: Pierre Corbineau,
5
Stage de DEA au LSV, ENS Cachan
6
Th�se au LRI, Universit� Paris Sud XI
10
- ccalgo.ml : congruence closure algorithm
11
- ccproof.ml : proof generation code
12
- cctac.ml4 : the tactic itself
13
- CCSolve.v : a small Ltac tactic based on congruence
15
Known Bugs : the congruence tactic can fail due to type dependencies.
18
Peter J. Downey, Ravi Sethi, and Robert E. Tarjan.
19
Variations on the common subexpression problem.
20
JACM, 27(4):758-771, October 1980.