Adding the congruence closure tactics (CC and CCsolve).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3061 85f007b7-540e-0410-9357-904b9bb8a0f7

11 files changed, 810 insertions, 78 deletions

diff --git a/.depend b/.depend
index 5f1d262c06..c82436adc7 100644
--- a/.depend
+++ b/.depend
@@ -15,10 +15,10 @@ kernel/indtypes.cmi: kernel/declarations.cmi kernel/entries.cmi \
     kernel/univ.cmi 
 kernel/inductive.cmi: kernel/declarations.cmi kernel/environ.cmi \
     kernel/names.cmi kernel/term.cmi kernel/univ.cmi 
-kernel/modops.cmi: kernel/declarations.cmi kernel/entries.cmi \
-    kernel/environ.cmi kernel/names.cmi kernel/univ.cmi 
 kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \
     kernel/environ.cmi 
+kernel/modops.cmi: kernel/declarations.cmi kernel/entries.cmi \
+    kernel/environ.cmi kernel/names.cmi kernel/univ.cmi 
 kernel/names.cmi: lib/pp.cmi lib/predicate.cmi 
 kernel/reduction.cmi: kernel/environ.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/univ.cmi 
@@ -37,6 +37,9 @@ kernel/typeops.cmi: kernel/entries.cmi kernel/environ.cmi kernel/names.cmi \
     kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
 kernel/univ.cmi: kernel/names.cmi lib/pp.cmi 
 lib/pp.cmi: lib/pp_control.cmi 
+lib/rtree.cmi: lib/pp.cmi 
+lib/system.cmi: lib/pp.cmi 
+lib/util.cmi: lib/pp.cmi 
 library/declare.cmi: kernel/cooking.cmi kernel/declarations.cmi \
     kernel/entries.cmi kernel/indtypes.cmi library/libnames.cmi \
     library/libobject.cmi library/library.cmi kernel/names.cmi \
@@ -64,9 +67,6 @@ library/nameops.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
 library/nametab.cmi: library/libnames.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi lib/util.cmi 
 library/summary.cmi: library/libnames.cmi kernel/names.cmi 
-lib/rtree.cmi: lib/pp.cmi 
-lib/system.cmi: lib/pp.cmi 
-lib/util.cmi: lib/pp.cmi 
 parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi parsing/genarg.cmi \
     library/libnames.cmi kernel/names.cmi lib/pp.cmi proofs/tacexpr.cmo \
     lib/util.cmi 
@@ -86,12 +86,12 @@ parsing/esyntax.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
     library/libnames.cmi lib/pp.cmi toplevel/vernacexpr.cmo 
 parsing/extend.cmi: parsing/ast.cmi parsing/coqast.cmi library/libnames.cmi \
     kernel/names.cmi lib/pp.cmi 
-parsing/genarg.cmi: kernel/closure.cmi parsing/coqast.cmi pretyping/evd.cmi \
-    library/libnames.cmi kernel/names.cmi pretyping/rawterm.cmi \
-    kernel/term.cmi lib/util.cmi 
 parsing/g_minicoq.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     kernel/term.cmi 
 parsing/g_zsyntax.cmi: parsing/coqast.cmi 
+parsing/genarg.cmi: kernel/closure.cmi parsing/coqast.cmi pretyping/evd.cmi \
+    library/libnames.cmi kernel/names.cmi pretyping/rawterm.cmi \
+    kernel/term.cmi lib/util.cmi 
 parsing/pcoq.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/genarg.cmi \
     library/libnames.cmi kernel/names.cmi pretyping/rawterm.cmi \
     proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmo 
@@ -285,19 +285,21 @@ toplevel/recordobj.cmi: library/libnames.cmi proofs/proof_type.cmi
 toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
     kernel/term.cmi 
 toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi 
+toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi \
+    toplevel/vernacexpr.cmo 
 toplevel/vernacentries.cmi: parsing/coqast.cmi kernel/environ.cmi \
     pretyping/evd.cmi library/libnames.cmi kernel/names.cmi kernel/term.cmi \
     lib/util.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi 
 toplevel/vernacinterp.cmi: proofs/tacexpr.cmo 
-toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi \
-    toplevel/vernacexpr.cmo 
+contrib/cc/ccalgo.cmi: kernel/names.cmi kernel/term.cmi 
+contrib/cc/ccproof.cmi: contrib/cc/ccalgo.cmi kernel/names.cmi 
 contrib/correctness/past.cmi: parsing/coqast.cmi kernel/names.cmi \
     contrib/correctness/ptype.cmi kernel/term.cmi 
+contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
+    pretyping/rawterm.cmi 
 contrib/correctness/pcicenv.cmi: kernel/names.cmi \
     contrib/correctness/penv.cmi contrib/correctness/prename.cmi \
     kernel/sign.cmi kernel/term.cmi 
-contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
-    pretyping/rawterm.cmi 
 contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/past.cmi \
     contrib/correctness/ptype.cmi 
 contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi 
@@ -447,12 +449,6 @@ kernel/inductive.cmo: kernel/declarations.cmi kernel/environ.cmi \
 kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \
     kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
     kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx kernel/inductive.cmi 
-kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
-    kernel/environ.cmi kernel/names.cmi kernel/term.cmi kernel/univ.cmi \
-    lib/util.cmi kernel/modops.cmi 
-kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
-    kernel/environ.cmx kernel/names.cmx kernel/term.cmx kernel/univ.cmx \
-    lib/util.cmx kernel/modops.cmi 
 kernel/mod_typing.cmo: kernel/declarations.cmi kernel/entries.cmi \
     kernel/environ.cmi kernel/modops.cmi kernel/names.cmi \
     kernel/reduction.cmi kernel/subtyping.cmi kernel/term_typing.cmi \
@@ -461,6 +457,12 @@ kernel/mod_typing.cmx: kernel/declarations.cmx kernel/entries.cmx \
     kernel/environ.cmx kernel/modops.cmx kernel/names.cmx \
     kernel/reduction.cmx kernel/subtyping.cmx kernel/term_typing.cmx \
     kernel/typeops.cmx kernel/univ.cmx lib/util.cmx kernel/mod_typing.cmi 
+kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
+    kernel/environ.cmi kernel/names.cmi kernel/term.cmi kernel/univ.cmi \
+    lib/util.cmi kernel/modops.cmi 
+kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
+    kernel/environ.cmx kernel/names.cmx kernel/term.cmx kernel/univ.cmx \
+    lib/util.cmx kernel/modops.cmi 
 kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/predicate.cmi lib/util.cmi \
     kernel/names.cmi 
 kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/predicate.cmx lib/util.cmx \
@@ -541,24 +543,34 @@ lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi
 lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi 
 lib/explore.cmo: lib/explore.cmi 
 lib/explore.cmx: lib/explore.cmi 
-lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi 
-lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi 
 lib/gmap.cmo: lib/gmap.cmi 
 lib/gmap.cmx: lib/gmap.cmi 
+lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi 
+lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi 
 lib/gset.cmo: lib/gset.cmi 
 lib/gset.cmx: lib/gset.cmi 
 lib/hashcons.cmo: lib/hashcons.cmi 
 lib/hashcons.cmx: lib/hashcons.cmi 
 lib/options.cmo: lib/util.cmi lib/options.cmi 
 lib/options.cmx: lib/util.cmx lib/options.cmi 
-lib/pp_control.cmo: lib/pp_control.cmi 
-lib/pp_control.cmx: lib/pp_control.cmi 
 lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
 lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
+lib/pp_control.cmo: lib/pp_control.cmi 
+lib/pp_control.cmx: lib/pp_control.cmi 
 lib/predicate.cmo: lib/predicate.cmi 
 lib/predicate.cmx: lib/predicate.cmi 
 lib/profile.cmo: lib/profile.cmi 
 lib/profile.cmx: lib/profile.cmi 
+lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi 
+lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi 
+lib/stamps.cmo: lib/stamps.cmi 
+lib/stamps.cmx: lib/stamps.cmi 
+lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi 
+lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi 
+lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi 
+lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
+lib/util.cmo: lib/pp.cmi lib/util.cmi 
+lib/util.cmx: lib/pp.cmx lib/util.cmi 
 library/declare.cmo: kernel/declarations.cmi kernel/entries.cmi \
     kernel/environ.cmi library/global.cmi library/impargs.cmi \
     kernel/indtypes.cmi kernel/inductive.cmi library/lib.cmi \
@@ -651,16 +663,6 @@ library/states.cmx: library/lib.cmx library/library.cmx library/summary.cmx \
     lib/system.cmx library/states.cmi 
 library/summary.cmo: lib/dyn.cmi lib/pp.cmi lib/util.cmi library/summary.cmi 
 library/summary.cmx: lib/dyn.cmx lib/pp.cmx lib/util.cmx library/summary.cmi 
-lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi 
-lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi 
-lib/stamps.cmo: lib/stamps.cmi 
-lib/stamps.cmx: lib/stamps.cmi 
-lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi 
-lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi 
-lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi 
-lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
-lib/util.cmo: lib/pp.cmi lib/util.cmi 
-lib/util.cmx: lib/pp.cmx lib/util.cmi 
 parsing/argextend.cmo: parsing/ast.cmi parsing/genarg.cmi parsing/pcoq.cmi \
     parsing/q_coqast.cmo parsing/q_util.cmi lib/util.cmi \
     toplevel/vernacexpr.cmo 
@@ -743,12 +745,6 @@ parsing/g_constr.cmo: parsing/ast.cmi parsing/coqast.cmi kernel/names.cmi \
     parsing/pcoq.cmi 
 parsing/g_constr.cmx: parsing/ast.cmx parsing/coqast.cmx kernel/names.cmx \
     parsing/pcoq.cmx 
-parsing/genarg.cmo: parsing/coqast.cmi pretyping/evd.cmi kernel/names.cmi \
-    library/nametab.cmi pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi \
-    parsing/genarg.cmi 
-parsing/genarg.cmx: parsing/coqast.cmx pretyping/evd.cmx kernel/names.cmx \
-    library/nametab.cmx pretyping/rawterm.cmx kernel/term.cmx lib/util.cmx \
-    parsing/genarg.cmi 
 parsing/g_ltac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/genarg.cmi \
     kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/rawterm.cmi \
     proofs/tacexpr.cmo lib/util.cmi toplevel/vernacexpr.cmo 
@@ -807,6 +803,12 @@ parsing/g_zsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
 parsing/g_zsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \
     parsing/esyntax.cmx parsing/extend.cmx kernel/names.cmx parsing/pcoq.cmx \
     lib/pp.cmx lib/util.cmx parsing/g_zsyntax.cmi 
+parsing/genarg.cmo: parsing/coqast.cmi pretyping/evd.cmi kernel/names.cmi \
+    library/nametab.cmi pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi \
+    parsing/genarg.cmi 
+parsing/genarg.cmx: parsing/coqast.cmx pretyping/evd.cmx kernel/names.cmx \
+    library/nametab.cmx pretyping/rawterm.cmx kernel/term.cmx lib/util.cmx \
+    parsing/genarg.cmi 
 parsing/lexer.cmo: parsing/lexer.cmi 
 parsing/lexer.cmx: parsing/lexer.cmi 
 parsing/pcoq.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/genarg.cmi \
@@ -1653,12 +1655,12 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \
     proofs/proof_trees.cmx pretyping/reductionops.cmx proofs/refiner.cmx \
     kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx \
     lib/util.cmx tactics/wcclausenv.cmi 
-tools/coqdep_lexer.cmo: config/coq_config.cmi 
-tools/coqdep_lexer.cmx: config/coq_config.cmx 
-tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
-tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
 tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi 
 tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx 
+tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
+tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
+tools/coqdep_lexer.cmo: config/coq_config.cmi 
+tools/coqdep_lexer.cmx: config/coq_config.cmx 
 tools/gallina.cmo: tools/gallina_lexer.cmo 
 tools/gallina.cmx: tools/gallina_lexer.cmx 
 toplevel/cerrors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \
@@ -1851,6 +1853,16 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/cerrors.cmx library/lib.cmx \
     toplevel/vernac.cmx toplevel/vernacexpr.cmx toplevel/toplevel.cmi 
 toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi 
 toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi 
+toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \
+    library/library.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \
+    lib/pp.cmi library/states.cmi lib/system.cmi lib/util.cmi \
+    toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \
+    toplevel/vernacinterp.cmi toplevel/vernac.cmi 
+toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \
+    library/library.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \
+    lib/pp.cmx library/states.cmx lib/system.cmx lib/util.cmx \
+    toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \
+    toplevel/vernacinterp.cmx toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astmod.cmi \
     parsing/astterm.cmi tactics/auto.cmi toplevel/class.cmi \
     pretyping/classops.cmi toplevel/command.cmi parsing/coqast.cmi \
@@ -1907,28 +1919,28 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx \
     kernel/names.cmx lib/options.cmx lib/pp.cmx proofs/proof_type.cmx \
     proofs/tacexpr.cmx tactics/tacinterp.cmx lib/util.cmx \
     toplevel/vernacexpr.cmx toplevel/vernacinterp.cmi 
-toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \
-    library/library.cmi kernel/names.cmi lib/options.cmi parsing/pcoq.cmi \
-    lib/pp.cmi library/states.cmi lib/system.cmi lib/util.cmi \
-    toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \
-    toplevel/vernacinterp.cmi toplevel/vernac.cmi 
-toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \
-    library/library.cmx kernel/names.cmx lib/options.cmx parsing/pcoq.cmx \
-    lib/pp.cmx library/states.cmx lib/system.cmx lib/util.cmx \
-    toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \
-    toplevel/vernacinterp.cmx toplevel/vernac.cmi 
-contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
-    contrib/correctness/past.cmi contrib/correctness/penv.cmi \
-    contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
-    contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
-    contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/univ.cmi contrib/correctness/pcicenv.cmi 
-contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
-    contrib/correctness/past.cmi contrib/correctness/penv.cmx \
-    contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
-    contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
-    contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
-    kernel/univ.cmx contrib/correctness/pcicenv.cmi 
+contrib/cc/ccalgo.cmo: kernel/names.cmi kernel/term.cmi contrib/cc/ccalgo.cmi 
+contrib/cc/ccalgo.cmx: kernel/names.cmx kernel/term.cmx contrib/cc/ccalgo.cmi 
+contrib/cc/ccproof.cmo: contrib/cc/ccalgo.cmi kernel/names.cmi \
+    contrib/cc/ccproof.cmi 
+contrib/cc/ccproof.cmx: contrib/cc/ccalgo.cmx kernel/names.cmx \
+    contrib/cc/ccproof.cmi 
+contrib/cc/cctac.cmo: contrib/cc/ccalgo.cmi contrib/cc/ccproof.cmi \
+    toplevel/cerrors.cmi parsing/coqlib.cmi library/declare.cmi \
+    parsing/egrammar.cmi pretyping/evd.cmi library/libnames.cmi \
+    library/library.cmi library/nameops.cmi kernel/names.cmi \
+    library/nametab.cmi parsing/pcoq.cmi lib/pp.cmi parsing/pptactic.cmi \
+    proofs/proof_type.cmi proofs/refiner.cmi tactics/tacinterp.cmi \
+    proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+    kernel/term.cmi lib/util.cmi 
+contrib/cc/cctac.cmx: contrib/cc/ccalgo.cmx contrib/cc/ccproof.cmx \
+    toplevel/cerrors.cmx parsing/coqlib.cmx library/declare.cmx \
+    parsing/egrammar.cmx pretyping/evd.cmx library/libnames.cmx \
+    library/library.cmx library/nameops.cmx kernel/names.cmx \
+    library/nametab.cmx parsing/pcoq.cmx lib/pp.cmx parsing/pptactic.cmx \
+    proofs/proof_type.cmx proofs/refiner.cmx tactics/tacinterp.cmx \
+    proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+    kernel/term.cmx lib/util.cmx 
 contrib/correctness/pcic.cmo: parsing/ast.cmi kernel/declarations.cmi \
     library/declare.cmi pretyping/detyping.cmi kernel/entries.cmi \
     library/global.cmi kernel/indtypes.cmi library/libnames.cmi \
@@ -1943,6 +1955,18 @@ contrib/correctness/pcic.cmx: parsing/ast.cmx kernel/declarations.cmx \
     contrib/correctness/pmisc.cmx pretyping/rawterm.cmx toplevel/record.cmx \
     kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx kernel/typeops.cmx \
     lib/util.cmx toplevel/vernacexpr.cmx contrib/correctness/pcic.cmi 
+contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
+    contrib/correctness/past.cmi contrib/correctness/penv.cmi \
+    contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
+    contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
+    contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \
+    kernel/univ.cmi contrib/correctness/pcicenv.cmi 
+contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
+    contrib/correctness/past.cmi contrib/correctness/penv.cmx \
+    contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
+    contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
+    contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
+    kernel/univ.cmx contrib/correctness/pcicenv.cmi 
 contrib/correctness/pdb.cmo: library/declare.cmi library/global.cmi \
     kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \
     contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
@@ -2479,14 +2503,6 @@ contrib/interface/pbp.cmx: parsing/astterm.cmx parsing/coqast.cmx \
     tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
     tactics/tactics.cmx kernel/term.cmx parsing/termast.cmx \
     pretyping/typing.cmx lib/util.cmx contrib/interface/pbp.cmi 
-contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
-    parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
-    parsing/printer.cmi contrib/interface/translate.cmi \
-    contrib/interface/vtp.cmi contrib/interface/xlate.cmi 
-contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
-    parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
-    parsing/printer.cmx contrib/interface/translate.cmx \
-    contrib/interface/vtp.cmx contrib/interface/xlate.cmx 
 contrib/interface/showproof.cmo: parsing/ast.cmi parsing/astterm.cmi \
     proofs/clenv.cmi parsing/coqast.cmi kernel/declarations.cmi \
     kernel/environ.cmi pretyping/evd.cmi parsing/genarg.cmi \
@@ -2511,6 +2527,14 @@ contrib/interface/showproof.cmx: parsing/ast.cmx parsing/astterm.cmx \
     pretyping/termops.cmx contrib/interface/translate.cmx \
     pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx \
     contrib/interface/showproof.cmi 
+contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
+    parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
+    parsing/printer.cmi contrib/interface/translate.cmi \
+    contrib/interface/vtp.cmi contrib/interface/xlate.cmi 
+contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
+    parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
+    parsing/printer.cmx contrib/interface/translate.cmx \
+    contrib/interface/vtp.cmx contrib/interface/xlate.cmx 
 contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
     contrib/interface/ctast.cmo kernel/environ.cmi pretyping/evarutil.cmi \
     pretyping/evd.cmi library/libobject.cmi library/library.cmi \
@@ -2677,6 +2701,8 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \
     proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \
     proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
     kernel/term.cmx lib/util.cmx 
+contrib/xml/xml.cmo: contrib/xml/xml.cmi 
+contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 contrib/xml/xmlcommand.cmo: kernel/declarations.cmi library/declare.cmi \
     library/declaremods.cmi kernel/environ.cmi pretyping/evd.cmi \
     library/global.cmi library/lib.cmi library/libnames.cmi \
@@ -2703,8 +2729,6 @@ contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
     parsing/extend.cmx parsing/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \
     parsing/pptactic.cmx tactics/tacinterp.cmx lib/util.cmx \
     toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx 
-contrib/xml/xml.cmo: contrib/xml/xml.cmi 
-contrib/xml/xml.cmx: contrib/xml/xml.cmi 
 tactics/tauto.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
 tactics/tauto.cmx: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
 tactics/eqdecide.cmo: parsing/grammar.cma
@@ -2739,6 +2763,8 @@ contrib/xml/xmlentries.cmo: parsing/grammar.cma
 contrib/xml/xmlentries.cmx: parsing/grammar.cma
 contrib/jprover/jprover.cmo: parsing/grammar.cma
 contrib/jprover/jprover.cmx: parsing/grammar.cma
+contrib/cc/cctac.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
+contrib/cc/cctac.cmx: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
 parsing/lexer.cmo: 
 parsing/lexer.cmx: 
 parsing/q_util.cmo: 
diff --git a/.depend.camlp4 b/.depend.camlp4
index 91bd4ef062..bccd1a4b1f 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -15,6 +15,7 @@ contrib/fourier/g_fourier.ml: parsing/grammar.cma
 contrib/extraction/g_extraction.ml: parsing/grammar.cma
 contrib/xml/xmlentries.ml: parsing/grammar.cma
 contrib/jprover/jprover.ml: parsing/grammar.cma
+contrib/cc/cctac.ml: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
 parsing/lexer.ml: 
 parsing/q_util.ml: 
 parsing/q_coqast.ml: 
diff --git a/Makefile b/Makefile
index 460b36d6ed..5f789d1727 100644
--- a/Makefile
+++ b/Makefile
@@ -43,7 +43,7 @@ LOCALINCLUDES=-I config -I tools -I scripts -I lib -I kernel -I library \
 	      -I contrib/ring -I contrib/xml \
 	      -I contrib/extraction -I contrib/correctness \
               -I contrib/interface -I contrib/fourier \
-	      -I contrib/jprover
+	      -I contrib/jprover -I contrib/cc
 
 MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
 
@@ -279,11 +279,13 @@ JPROVERCMO=contrib/jprover/opname.cmo \
            contrib/jprover/jtunify.cmo contrib/jprover/jall.cmo \
            contrib/jprover/jprover.cmo
 
-ML4FILES += contrib/jprover/jprover.ml4
+CCCMO=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo  
+
+ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/cctac.ml4
 
 CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(FIELDCMO) \
 	$(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \
-	$(CORRECTNESSCMO) 
+	$(CORRECTNESSCMO) $(CCCMO)
 
 CMA=$(CLIBS) $(CAMLP4OBJS)
 CMXA=$(CMA:.cma=.cmxa)
@@ -608,6 +610,8 @@ FOURIERVO = contrib/fourier/Fourier_util.vo    contrib/fourier/Fourier.vo
 
 JPROVERVO = 
 
+CCVO = contrib/cc/CC.vo
+
 contrib/interface/Centaur.vo: contrib/interface/Centaur.v $(INTERFACE)
 	$(BESTCOQTOP) -boot -byte  $(COQINCLUDES) -compile $*
 
@@ -616,7 +620,7 @@ contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) states/init
 
 CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \
 	    $(CORRECTNESSVO) $(FOURIERVO) \
-	    $(JPROVERVO) $(INTERFACEV0)
+	    $(JPROVERVO) $(INTERFACEV0) $(CCVO)
 
 $(CONTRIBVO): states/initial.coq
 
@@ -630,6 +634,7 @@ correctness: $(CORRECTNESSCMO) $(CORRECTNESSVO)
 field: $(FIELDVO) $(FIELDCMO)
 fourier: $(FOURIERVO) $(FOURIERCMO)
 jprover: $(JPROVERVO) $(JPROVERCMO)
+cc: $(CCVO) $(CCCMO)
 
 ALLVO = $(INITVO) $(THEORIESVO) $(CONTRIBVO) $(EXTRACTIONVO)
 
diff --git a/contrib/cc/CC.v b/contrib/cc/CC.v
new file mode 100644
index 0000000000..7bd3497872
--- /dev/null
+++ b/contrib/cc/CC.v
@@ -0,0 +1,36 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $id$ *)
+
+Require Export Eqdep_dec.
+
+(* Congruence lemma *)
+
+Theorem Congr_nodep: (A,B:Type)(f,g:A->B)(x,y:A)f==g->x==y->(f x)==(g y).
+Intros A B f g x y eq1 eq2;Rewrite eq1;Rewrite eq2;Reflexivity.
+Defined.
+
+Theorem Congr_dep:
+	(A:Type; P:(A->Type); f,g:((a:A)(P a)); x:A)f==g->(f x)==(g x).
+Intros A P f g x e;Rewrite e;Reflexivity.
+Defined.
+
+(* Basic application : try to prove that goal is equal to one hypothesis *) 
+
+Lemma convert_goal :  (A,B:Prop)B->(A==B)->A.
+Intros A B H E;Rewrite E;Assumption.
+Save.
+
+Tactic Definition CCsolve :=
+ Match Context With
+ [ H: ?1 |- ?2] -> 
+        (Assert (?2==?1);[CC|
+        Match Reverse Context With 
+                [ H: ?1;Heq: (?2==?1)|- ?2] ->(Rewrite Heq;Exact H)]).
+
diff --git a/contrib/cc/README b/contrib/cc/README
new file mode 100644
index 0000000000..f19820d32b
--- /dev/null
+++ b/contrib/cc/README
@@ -0,0 +1,18 @@
+
+cctac: congruence-closure for coq
+
+author: Pierre Corbineau, Stage de DEA au LSV, ENS Cachan 
+
+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
+
+Known Bugs : CC 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.	
diff --git a/contrib/cc/ccalgo.ml b/contrib/cc/ccalgo.ml
new file mode 100644
index 0000000000..93b60531b2
--- /dev/null
+++ b/contrib/cc/ccalgo.ml
@@ -0,0 +1,203 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(* This file implements the basic congruence-closure algorithm by *)
+(* Downey,Sethi and Tarjan. *)
+
+open Names
+open Term
+
+let init_size=251
+  
+type term=Symb of constr|Appli of term*term
+
+
+(* Basic Union-Find algo w/o path compression *)
+    
+module UF = struct
+  type tag=Congr|Ax of identifier
+      
+  type cl=Rep of int*(int list)|Eqto of int*(int*int*tag)
+
+  type vertex=Leaf|Node of (int*int) 
+
+  type t=(int ref)*((int,(cl*vertex*term)) Hashtbl.t)
+	
+  let empty ()=(((ref 0),(Hashtbl.create init_size)):t)
+   	   
+  let add_lst i t ((a,m):t)=
+    match Hashtbl.find m i with
+      ((Rep(l,lst)),v,trm)->Hashtbl.replace m i ((Rep((l+1),(t::lst))),v,trm)
+    | _ ->failwith "add_lst: not a representative"
+	  
+  let rec find ((a,m):t) i=
+    let (cl,_,_)=Hashtbl.find m i in
+    match cl with
+      Rep(_,_) -> i
+    | Eqto(j,_) ->find (a,m) j
+	  
+  let list ((a,m):t) i=
+    match Hashtbl.find m i with
+      ((Rep(_,lst)),_,_)-> lst
+    | _ ->failwith "list: not a class"
+	  
+  let size ((a,m):t) i=
+    match Hashtbl.find m i with
+      ((Rep (l,_)),_,_) -> l
+    | _ ->failwith "size: not a class"
+	  
+  let signature ((a,m):t) i=
+    let (_,v,_)=Hashtbl.find m i in
+    match v with
+      Node(j,k)->(find (a,m) j,find (a,m) k)
+    | _ ->failwith "signature: not a node"
+
+  let nodes ((a,m):t)=  (* cherche les noeuds binaires *)
+    Hashtbl.fold (fun i (_,v,_) l->match v with Node (_,_)->i::l|_->l) m [] 
+
+  let rec add t (a,m) syms = 
+    try Hashtbl.find syms t with Not_found ->
+	match t with
+	  Symb s -> 
+	    let b= !a in incr a;
+	    Hashtbl.add m b ((Rep (0,[])),Leaf,t);
+	    Hashtbl.add syms t b;
+	    b
+	| Appli (t1,t2) -> 
+	    let i1=add t1 (a,m) syms and i2=add t2 (a,m) syms in
+	    let b= !a in incr a;
+	    add_lst (find (a,m) i1) b (a,m);
+            add_lst (find (a,m) i2) b (a,m);
+	    Hashtbl.add m b ((Rep (0,[])),(Node(i1,i2)),t);
+	    Hashtbl.add syms t b;
+	    b
+	      
+  let union ((a,m):t) i1 i2 t=
+    let (cl1,v1,t1)=(Hashtbl.find m i1) and 
+	(cl2,v2,t2)=(Hashtbl.find m i2) in
+    match cl1,cl1 with
+      ((Rep (l1,lst1)),(Rep (l2,lst2))) -> 
+	Hashtbl.replace m i2 ((Eqto (i1,t)),v2,t2);
+	Hashtbl.replace m i1 ((Rep((l2+l1),(lst2@lst1))),v1,t1)
+    | _ ->failwith "union: not classes"
+	  
+	  
+end    
+    
+(* Signature table *)
+
+module ST=struct
+  
+(* l: sign -> term r: term -> sign *)
+	
+  type t = ((int*int,int) Hashtbl.t) * ((int,int*int) Hashtbl.t)
+	
+  let empty ()=((Hashtbl.create init_size),(Hashtbl.create init_size))
+      
+  let enter t sign ((l,r) as st:t)=
+    if Hashtbl.mem l sign then 
+	failwith "enter: signature already entered"
+    else 
+	Hashtbl.replace l sign t;
+	Hashtbl.replace r t sign
+	  
+  let query sign ((l,r):t)=Hashtbl.find l sign
+	  
+  let delete t ((l,r) as st:t)=
+    try let sign=Hashtbl.find r t in
+	Hashtbl.remove l sign;
+	Hashtbl.remove r t
+    with
+	Not_found -> ()
+
+  let rec delete_list l st=
+    match l with
+      []->()
+    | t::q -> delete t st;delete_list q st
+	  
+end
+    
+let rec combine_rec uf st=function 
+    []->[]
+  | v::pending->
+      let combine=(combine_rec uf st pending) in
+      let s=UF.signature uf v in
+      try (v,(ST.query s st))::combine with
+	Not_found->
+	  ST.enter v s st;combine
+	    
+let rec process_rec uf st=function
+    []->[] 
+  | (v,w)::combine->
+      let pending=process_rec uf st combine in
+      let i=UF.find uf v 
+      and j=UF.find uf w in
+      if (i==j)|| ((Hashtbl.hash i)=(Hashtbl.hash j) && (i=j)) then 
+	pending 
+      else
+	if (UF.size uf i)<(UF.size uf j) then
+	  let l=UF.list uf i in
+	  UF.union uf j i (v,w,UF.Congr);
+	  ST.delete_list l st;
+	  l@pending
+	else
+	  let l=UF.list uf j in
+	  UF.union uf i j (w,v,UF.Congr);
+	  ST.delete_list l st;
+	  l@pending
+	  
+let rec cc_rec uf st=function
+    []->()
+  | pending->
+      let combine=combine_rec uf st pending in
+      let pending0=process_rec uf st combine in
+      (cc_rec uf st pending0)
+	
+let cc uf=(cc_rec uf (ST.empty ()) (UF.nodes uf))
+
+let rec make_uf syms=function
+    []->(UF.empty ())
+  | (ax,(v,w))::q->
+      let uf=make_uf syms q in
+      let i1=UF.add v uf syms in
+      let i2=UF.add w uf syms in
+      UF.union uf (UF.find uf i2) (UF.find uf i1) (i1,i2,(UF.Ax ax));
+      uf
+	
+let decide_prb (axioms,(v,w))=
+  let syms=Hashtbl.create init_size in
+  let uf=make_uf syms axioms in
+  let i1=UF.add v uf syms in
+  let i2=UF.add w uf syms in
+  cc uf;
+  (UF.find uf i1)=(UF.find uf i2)
+
+
+
+
+
+    
+    
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/contrib/cc/ccalgo.mli b/contrib/cc/ccalgo.mli
new file mode 100644
index 0000000000..6f55d85418
--- /dev/null
+++ b/contrib/cc/ccalgo.mli
@@ -0,0 +1,67 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+val init_size : int
+
+type term = Symb of Term.constr | Appli of term * term
+
+module UF :
+  sig
+    type tag = Congr | Ax of Names.identifier
+    and cl =
+        Rep of int * int list
+      | Eqto of int * (int * int * tag)
+    and vertex = Leaf | Node of (int * int)
+    and t = int ref * (int, cl * vertex * term) Hashtbl.t
+    val empty : unit -> t
+    val add_lst : int -> int -> t -> unit
+    val find : t -> int -> int
+    val list : t -> int -> int list
+    val size : t -> int -> int
+    val signature : t -> int -> int * int
+    val nodes : t -> int list
+    val add :
+      term ->
+      int ref * (int, cl * vertex * term) Hashtbl.t ->
+      (term, int) Hashtbl.t -> int
+    val union :
+      t -> int -> int -> int * int * tag -> unit
+  end
+
+module ST :
+  sig
+    type t =
+      (int * int, int) Hashtbl.t *
+      (int, int * int) Hashtbl.t
+    val empty :
+      unit -> ('a, 'b) Hashtbl.t * ('c, 'd) Hashtbl.t
+    val enter : int -> int * int -> t -> unit
+    val query : int * int -> t -> int
+    val delete : int -> t -> unit
+    val delete_list : int list -> t -> unit
+  end
+
+val combine_rec :
+  UF.t -> ST.t -> int list -> (int * int) list
+
+val process_rec :
+  UF.t -> ST.t -> (int * int) list -> int list
+
+val cc_rec : UF.t -> ST.t -> int list -> unit
+
+val cc : UF.t -> unit
+
+val make_uf :
+  (term, int) Hashtbl.t ->
+  (Names.identifier * (term * term)) list -> UF.t
+
+val decide_prb :
+  (Names.identifier * (term * term)) list * (term * term) ->
+  bool
diff --git a/contrib/cc/ccproof.ml b/contrib/cc/ccproof.ml
new file mode 100644
index 0000000000..26e2299179
--- /dev/null
+++ b/contrib/cc/ccproof.ml
@@ -0,0 +1,118 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(* This file uses the (non-compressed) union-find structure to generate *) 
+(* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
+
+open Names
+open Ccalgo
+  
+type proof=
+    Ax of identifier
+  | Refl of term
+  | Trans of proof*proof
+  | Sym of proof
+  | Congr of proof*proof
+	
+let rec up_path uf i l=
+  let (cl,_,_)=(Hashtbl.find uf i) in
+  match cl with 
+    UF.Eqto(j,t)->up_path uf j (((i,j),t)::l)
+  | UF.Rep(_,_)->l
+	
+let rec min_path=function 
+    ([],l2)->([],l2)
+  | (l1,[])->(l1,[])
+  | (((c1,t1)::q1),((c2,t2)::q2)) as cpl->
+      if c1=c2 then 
+	min_path (q1,q2) 
+      else 
+	cpl
+	  
+let pcongr=function
+    ((Refl t1),(Refl t2))->Refl (Appli (t1,t2))
+  | (p1,p2) -> Congr (p1,p2)
+
+let rec ptrans=function
+    ((Refl _),p)->p
+  | (p,(Refl _))->p
+  | (Trans(p1,p2),p3)->ptrans(p1,ptrans (p2,p3))
+  | (Congr(p1,p2),Congr(p3,p4))->pcongr(ptrans(p1,p3),ptrans(p2,p4))
+  | (Congr(p1,p2),Trans(Congr(p3,p4),p5))->
+	ptrans(pcongr(ptrans(p1,p3),ptrans(p2,p4)),p5)
+  | (p1,p2)->Trans (p1,p2)
+	
+let rec psym=function
+    Refl p->Refl p
+  | Sym p->p
+  | Ax s-> Sym(Ax s)
+  | Trans (p1,p2)-> ptrans ((psym p2),(psym p1))
+  | Congr (p1,p2)-> pcongr ((psym p1),(psym p2))
+	
+let pcongr=function
+    ((Refl t1),(Refl t2))->Refl (Appli (t1,t2))
+  | (p1,p2) -> Congr (p1,p2)
+	
+let build_proof ((a,m):UF.t) i j=
+  let rec equal_proof i j=
+    let (li,lj)=min_path ((up_path m i []),(up_path m j [])) in
+    ptrans ((path_proof i li),(psym (path_proof j lj)))
+  and arrow_proof ((i,j),t)=
+    let (i0,j0,t0)=t in
+    let pi=(equal_proof i i0) in
+    let pj=psym (equal_proof j j0) in
+    let pij=
+      match t0 with 
+	UF.Ax s->Ax s
+      | UF.Congr->(congr_proof i0 j0)	
+    in  ptrans(ptrans (pi,pij),pj)
+  and path_proof i=function
+      []->let (_,_,t)=Hashtbl.find m i in Refl t
+    | (((_,j),_) as x)::q->ptrans ((path_proof j q),(arrow_proof x))
+  and congr_proof i j=
+    let (_,vi,_)=(Hashtbl.find m i) and (_,vj,_)=(Hashtbl.find m j) in   
+    match (vi,vj) with
+      ((UF.Node(i1,i2)),(UF.Node(j1,j2)))->
+	pcongr ((equal_proof i1 j1),(equal_proof i2 j2))
+    | _ -> failwith "congr_proof: couldn't find subterms"
+  in
+  (equal_proof i j)
+    
+let rec type_proof uf axioms p=
+  match p with
+    Ax s->List.assoc s axioms
+  | Refl t->(t,t)
+  | Trans (p1,p2)->
+      let (s1,t1)=type_proof uf axioms p1 
+      and (t2,s2)=type_proof uf axioms p2 in
+      if t1=t2 then (s1,s2) else failwith "invalid transitivity"
+  | Sym p->let (t1,t2)=type_proof uf axioms p in (t2,t1)
+  | Congr (p1,p2)->
+      let (i1,j1)=(type_proof uf axioms p1)
+      and (i2,j2)=(type_proof uf axioms p2) in
+      ((Appli (i1,i2)),(Appli (j1,j2)))
+	
+let cc_proof (axioms,(v,w))=
+  let syms=Hashtbl.create init_size in
+  let uf=make_uf syms axioms in
+  let i1=(UF.add v uf syms) in
+  let i2=(UF.add w uf syms) in
+  cc uf;
+  if (UF.find uf i1)=(UF.find uf i2) then 
+    let p=(build_proof uf i1 i2) in
+    (if (v,w)=(type_proof uf axioms p) then Some (p,uf,axioms) 
+    else failwith "Proof check failed !!")
+  else
+    None;;
+
+    
+
+
+
diff --git a/contrib/cc/ccproof.mli b/contrib/cc/ccproof.mli
new file mode 100644
index 0000000000..a699af6941
--- /dev/null
+++ b/contrib/cc/ccproof.mli
@@ -0,0 +1,48 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Ccalgo
+
+type proof =
+    Ax of Names.identifier
+  | Refl of term
+  | Trans of proof * proof
+  | Sym of proof
+  | Congr of proof * proof
+
+val up_path :
+  (int, UF.cl * 'a * 'b) Hashtbl.t ->
+  int ->
+  ((int * int) * (int * int * UF.tag)) list ->
+  ((int * int) * (int * int * UF.tag)) list
+
+val min_path :
+  ('a * 'b) list * ('a * 'c) list ->
+  ('a * 'b) list * ('a * 'c) list
+
+val pcongr : proof * proof -> proof
+val ptrans : proof * proof -> proof
+val psym : proof -> proof
+val pcongr : proof * proof -> proof
+
+val build_proof : UF.t -> int -> int -> proof
+
+val type_proof :
+  'a ->
+  (Names.identifier * (term * term)) list ->
+  proof -> term * term
+
+val cc_proof :
+  (Names.identifier * (term * term)) list *
+  (term * term) ->
+  (proof * UF.t *
+   (Names.identifier * (term * term)) list)
+  option
+
diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4
new file mode 100644
index 0000000000..f7a9e723fa
--- /dev/null
+++ b/contrib/cc/cctac.ml4
@@ -0,0 +1,161 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo" i*)
+
+(* $Id$ *)
+
+(* This file is the interface between the c-c algorithm and Coq *)
+
+open Evd
+open Proof_type
+open Names
+open Libnames
+open Nameops
+open Term
+open Tacmach
+open Tactics
+open Tacticals
+open Ccalgo
+open Tacinterp
+open Ccproof
+open Pp
+open Util
+open Format
+
+exception Not_an_eq
+
+let fail()=raise Not_an_eq
+    
+let constr_of_string s () =
+  Declare.constr_of_reference (Nametab.locate (qualid_of_string s))
+
+let eq2eqT_theo = constr_of_string "Coq.Logic.Eqdep_dec.eq2eqT"
+let eqT2eq_theo = constr_of_string "Coq.Logic.Eqdep_dec.eqT2eq"
+let congr_theo = constr_of_string "Coq.cc.CC.Congr_nodep"
+let congr_dep_theo = constr_of_string "Coq.cc.CC.Congr_dep"
+
+let fresh_id1=id_of_string "eq1" and fresh_id2=id_of_string "eq2"
+    
+let t_make_app=(Array.fold_left (fun s t->Appli (s,t)))
+
+(* decompose member of equality in an applicative format *)
+
+let rec decompose_term t=
+  match kind_of_term t with
+    App (f,args)->let targs=Array.map decompose_term args in
+    (t_make_app (Symb f) targs)
+  | _->(Symb t)
+
+(* decompose equality in members and type *)
+	
+let eq_type_of_term term=
+  match kind_of_term term with
+      App (f,args)->
+	(try 
+	   let ref = Declare.reference_of_constr f in
+	     if (ref=Coqlib.glob_eq || ref=Coqlib.glob_eqT) && 
+	       (Array.length args)=3 
+	     then (args.(0),args.(1),args.(2)) 
+	     else fail()
+	 with
+	     Not_found -> fail ())
+    | _ ->fail ()
+
+(* read an equality *)
+	  
+let read_eq term=
+  let (_,t1,t2)=eq_type_of_term term in 
+    ((decompose_term t1),(decompose_term t2))
+
+(* rebuild a term from applicative format *)
+    
+let rec make_term=function
+    Symb s->s
+  | Appli (s1,s2)->make_app [(make_term s2)] s1
+and make_app l=function
+    Symb s->mkApp (s,(Array.of_list l))
+  | Appli (s1,s2)->make_app ((make_term s2)::l) s1
+
+(* store all equalities from the context *)
+	
+let rec read_hyps=function
+    []->[]
+  | (id,_,e)::hyps->let q=(read_hyps hyps) in
+      try (id,(read_eq e))::q with Not_an_eq -> q
+
+(* build a problem ( i.e. read the goal as an equality ) *)
+	
+let make_prb gl=
+  let concl=gl.evar_concl in
+  let hyps=gl.evar_hyps in
+  (read_hyps hyps),(read_eq concl)
+
+(* apply tac, followed (or not) by aplication of theorem theo *)
+
+let st_wrap theo tac= 
+  tclORELSE tac (tclTHEN (apply theo) tac)
+
+(* generate an adhoc tactic following the proof tree  *)
+
+let rec proof_tac uf axioms=function
+    Ax id->(fun gl->(st_wrap (eq2eqT_theo ()) (exact_check (mkVar id)) gl))
+  | Refl t->reflexivity
+  | Trans (p1,p2)->let t=(make_term (snd (type_proof uf axioms p1))) in
+      (tclTHENS (transitivity t) 
+	 [(proof_tac uf axioms p1);(proof_tac uf axioms p2)])
+  | Sym p->tclTHEN symmetry (proof_tac uf axioms p)
+  | Congr (p1,p2)->
+      (fun gl->
+	 let (s1,t1)=(type_proof uf axioms p1) and
+	   (s2,t2)=(type_proof uf axioms p2) in
+         let ts1=(make_term s1) and tt1=(make_term t1) 
+	and ts2=(make_term s2) and tt2=(make_term t2) in
+      let typ1=pf_type_of gl ts1 and typ2=pf_type_of gl ts2 in
+      let (typb,_,_)=(eq_type_of_term gl.it.evar_concl) in
+      let act=mkApp ((congr_theo ()),[|typ2;typb;ts1;tt1;ts2;tt2|]) in
+      tclORELSE 
+	(tclTHENS 
+	   (apply act)	 
+	   [(proof_tac uf axioms p1);(proof_tac uf axioms p2)])		
+	   (tclTHEN
+	      (let p=mkLambda(destProd typ1) in
+	      let acdt=mkApp((congr_dep_theo ()),[|typ2;p;ts1;tt1;ts2|]) in 
+	      apply acdt) (proof_tac uf axioms p1))
+	gl)
+
+(* wrap everything *)
+	
+let cc_tactic gl_sg=
+  Library.check_required_library ["Coq";"cc";"CC"];
+  let gl=gl_sg.it in
+  let prb=try make_prb gl with Not_an_eq ->
+    errorlabstrm  "CC" [< str "Couldn't match goal with an equality" >] in
+  match (cc_proof prb) with
+    None->errorlabstrm  "CC" [< str "CC couldn't solve goal" >] 
+  | Some (p,uf,axioms)->let tac=proof_tac uf axioms p in
+    (tclORELSE (st_wrap (eqT2eq_theo ()) tac)
+       (fun _->errorlabstrm  "CC" 
+	  [< str "CC doesn't know how to handle dependent equality." >]) gl_sg)
+
+(* Tactic registration *)
+      
+TACTIC EXTEND CC
+ [ "CC" ] -> [ cc_tactic ]
+END
+
+
+
+
+
+
+
+
+
+
+   
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
new file mode 100644
index 0000000000..881d6f9e5f
--- /dev/null
+++ b/test-suite/success/cc.v
@@ -0,0 +1,49 @@
+Require CC.
+
+
+Theorem t1: (A:Set)(a:A)(f:A->A)
+	(f a)=a->(f (f a))=a.
+Intros.
+CC.
+Save.
+
+Theorem t2: (A:Set)(a,b:A)(f:A->A)(g:A->A->A)
+	a=(f a)->(g b (f a))=(f (f a))->(g a b)=(f (g b a))->
+	(g a b)=a.
+Intros.
+CC.
+Save.
+
+(* 15=0 /\ 10=0 /\ 6=0 -> 0=1 *)
+
+Theorem t3: (N:Set)(o:N)(s:N->N)(d:N->N)
+	(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s o)))))))))))))))=o->
+	(s (s (s (s (s (s (s (s (s (s o))))))))))=o->
+	(s (s (s (s (s (s o))))))=o->
+	o=(s o).
+Intros.
+CC.
+Save.
+
+(* Examples that fail due to dependencies *) 
+
+(* yields transitivity problem *)
+
+Theorem dep:(A:Set)(P:A->Set)(f,g:(x:A)(P x))(x,y:A)
+    (e:x=y)(e0:(f y)=(g y))(f x)=(g x).
+Intros;Dependent Rewrite -> e;Exact e0.
+Save.
+
+(* yields congruence problem *)
+
+Theorem dep2:(A,B:Set)(f:(A:Set)(b:bool)if b then unit else A->unit)(e:A==B)
+   (f A true)=(f B true).
+Intros;Rewrite e;Reflexivity.
+Save.
+
+(* example with CCSolve *)
+
+Theorem t4 :  (A:Set; P:(A->Prop); u,v:A)u=v->(P u)->(P v).
+Intros.
+CCsolve.
+Save.