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 | |
| parent | aa2e7f2a10323c73660c6a07eb493fdad42f1597 (diff) | |
minor changes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5480 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/cc/README | 8 | ||||
| -rw-r--r-- | contrib/cc/ccalgo.ml | 2 | ||||
| -rw-r--r-- | contrib/cc/ccproof.ml | 3 | ||||
| -rw-r--r-- | contrib/cc/cctac.ml4 | 10 |
4 files changed, 7 insertions, 16 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. diff --git a/contrib/cc/ccalgo.ml b/contrib/cc/ccalgo.ml index eb640d5d72..6a641c3920 100644 --- a/contrib/cc/ccalgo.ml +++ b/contrib/cc/ccalgo.ml @@ -349,7 +349,7 @@ let add_disaxioms uf disaxioms= let f (id,cpl)=(id,add_one_diseq uf cpl) in List.map f disaxioms -let check_equal uf (i1,i2) = UF.find uf i2 = UF.find uf i2 +let check_equal uf (i1,i2) = UF.find uf i1 = UF.find uf i2 let find_contradiction uf diseq = List.find (fun (id,cpl) -> check_equal uf cpl) diseq diff --git a/contrib/cc/ccproof.ml b/contrib/cc/ccproof.ml index 88669f45d2..2584fbf509 100644 --- a/contrib/cc/ccproof.ml +++ b/contrib/cc/ccproof.ml @@ -127,8 +127,7 @@ let rec type_proof axioms p= let by_contradiction uf diseq axioms disaxioms= try - let id,cpl= - find_contradiction uf diseq in + let id,cpl=find_contradiction uf diseq in let prf=build_proof uf (`Refute_hyp cpl) in if List.assoc id disaxioms=type_proof axioms prf then `Refute_hyp (id,prf) diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4 index 5c2c935ff3..098bfe9dde 100644 --- a/contrib/cc/cctac.ml4 +++ b/contrib/cc/cctac.ml4 @@ -244,14 +244,4 @@ let cc_tactic gls= TACTIC EXTEND CC [ "Congruence" ] -> [ tclSOLVE [tclTHEN (tclREPEAT introf) cc_tactic] ] END - - - - - - - - - - |