matita.cs.unibo.it Git - helm.git/commit - helm/ocaml/library/cicRecord.ml

]> matita.cs.unibo.it Git - helm.git/commit - helm/ocaml/library/cicRecord.ml

author	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Wed, 30 Nov 2005 10:11:00 +0000 (10:11 +0000)
committer	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Wed, 30 Nov 2005 10:11:00 +0000 (10:11 +0000)
commit	2034db684e1d295527afad07a94f2f3b6b4ed7e2
tree	6510ca81980ece556c32c2c91e2e1f65df0f43af	tree \| snapshot
parent	0ac236dda6f80f6dc86a7f12d8c88b25e64e3251	commit \| diff

Generation of auxiliary lemmas for inductive types and records moved
from cic_proof_checking and matita to ocaml/library.

16 files changed:

helm/matita/matitaEngine.ml		diff \| blob \| history
helm/matita/matitaSync.ml		diff \| blob \| history
helm/ocaml/cic_proof_checking/.depend		diff \| blob \| history
helm/ocaml/cic_proof_checking/Makefile		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicElim.ml	[deleted file]	blob \| history
helm/ocaml/cic_proof_checking/cicElim.mli	[deleted file]	blob \| history
helm/ocaml/cic_proof_checking/cicRecord.ml	[deleted file]	blob \| history
helm/ocaml/cic_proof_checking/cicRecord.mli	[deleted file]	blob \| history
helm/ocaml/library/.depend	[new file with mode: 0644]	blob
helm/ocaml/library/Makefile		diff \| blob \| history
helm/ocaml/library/cicElim.ml	[new file with mode: 0644]	blob
helm/ocaml/library/cicElim.mli	[new file with mode: 0644]	blob
helm/ocaml/library/cicRecord.ml	[new file with mode: 0644]	blob
helm/ocaml/library/cicRecord.mli	[new file with mode: 0644]	blob
helm/ocaml/library/librarySync.ml		diff \| blob \| history
helm/ocaml/library/librarySync.mli		diff \| blob \| history

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