Skip to content
Fetching latest commit…
Cannot retrieve the latest commit at this time.
..
Failed to load latest commit information.
README
cc_plugin.mllib
ccalgo.ml
ccalgo.mli
ccproof.ml
ccproof.mli
cctac.ml
cctac.mli
g_congruence.ml4

README

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.	
Something went wrong with that request. Please try again.