matita.cs.unibo.it Git - helm.git/commit

]> matita.cs.unibo.it Git - helm.git/commit

author	Andrea Asperti <andrea.asperti@unibo.it>
	Thu, 12 Jan 2006 12:38:36 +0000 (12:38 +0000)
committer	Andrea Asperti <andrea.asperti@unibo.it>
	Thu, 12 Jan 2006 12:38:36 +0000 (12:38 +0000)
commit	b1527286e32c8651d65619af61e3f638b3b89f8d
tree	287a9450fe4512daf459bd743807d4a1d2d3a4f7	tree \| snapshot
parent	d3e3b22ce9cca9e4ca80f75a6bdc4c2df93efb0b	commit \| diff

Moved paramodulation inside tactics.
Added a new (reduction) tactic demodulate.

38 files changed:

helm/ocaml/grafite/grafiteAst.ml		diff \| blob \| history
helm/ocaml/grafite/grafiteAstPp.ml		diff \| blob \| history
helm/ocaml/grafite_engine/grafiteEngine.ml		diff \| blob \| history
helm/ocaml/grafite_parser/grafiteDisambiguate.ml		diff \| blob \| history
helm/ocaml/grafite_parser/grafiteParser.ml		diff \| blob \| history
helm/ocaml/paramodulation/.depend	[deleted file]	blob \| history
helm/ocaml/paramodulation/Makefile	[deleted file]	blob \| history
helm/ocaml/paramodulation/README	[deleted file]	blob \| history
helm/ocaml/paramodulation/equality_indexing.ml	[deleted file]	blob \| history
helm/ocaml/paramodulation/equality_indexing.mli	[deleted file]	blob \| history
helm/ocaml/paramodulation/indexing.ml	[deleted file]	blob \| history
helm/ocaml/paramodulation/inference.ml	[deleted file]	blob \| history
helm/ocaml/paramodulation/inference.mli	[deleted file]	blob \| history
helm/ocaml/paramodulation/saturate_main.ml	[deleted file]	blob \| history
helm/ocaml/paramodulation/saturation.ml	[deleted file]	blob \| history
helm/ocaml/paramodulation/test_indexing.ml	[deleted file]	blob \| history
helm/ocaml/paramodulation/utils.ml	[deleted file]	blob \| history
helm/ocaml/paramodulation/utils.mli	[deleted file]	blob \| history
helm/ocaml/tactics/.depend		diff \| blob \| history
helm/ocaml/tactics/Makefile		diff \| blob \| history
helm/ocaml/tactics/autoTactic.ml		diff \| blob \| history
helm/ocaml/tactics/autoTactic.mli		diff \| blob \| history
helm/ocaml/tactics/paramodulation/.depend	[new file with mode: 0644]	blob
helm/ocaml/tactics/paramodulation/Makefile	[new file with mode: 0644]	blob
helm/ocaml/tactics/paramodulation/README	[new file with mode: 0644]	blob
helm/ocaml/tactics/paramodulation/equality_indexing.ml	[new file with mode: 0644]	blob
helm/ocaml/tactics/paramodulation/equality_indexing.mli	[new file with mode: 0644]	blob
helm/ocaml/tactics/paramodulation/indexing.ml	[new file with mode: 0644]	blob
helm/ocaml/tactics/paramodulation/inference.ml	[new file with mode: 0644]	blob
helm/ocaml/tactics/paramodulation/inference.mli	[new file with mode: 0644]	blob
helm/ocaml/tactics/paramodulation/saturate_main.ml	[new file with mode: 0644]	blob
helm/ocaml/tactics/paramodulation/saturation.ml	[new file with mode: 0644]	blob
helm/ocaml/tactics/paramodulation/saturation.mli	[new file with mode: 0644]	blob
helm/ocaml/tactics/paramodulation/test_indexing.ml	[new file with mode: 0644]	blob
helm/ocaml/tactics/paramodulation/utils.ml	[new file with mode: 0644]	blob
helm/ocaml/tactics/paramodulation/utils.mli	[new file with mode: 0644]	blob
helm/ocaml/tactics/tactics.ml		diff \| blob \| history
helm/ocaml/tactics/tactics.mli		diff \| blob \| history

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom