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

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

author	Enrico Tassi <enrico.tassi@inria.fr>
	Tue, 1 Jun 2004 13:44:34 +0000 (13:44 +0000)
committer	Enrico Tassi <enrico.tassi@inria.fr>
	Tue, 1 Jun 2004 13:44:34 +0000 (13:44 +0000)
commit	655906d74521fa49de332f54ec34bfc9d9744151
tree	b9730fa0aea8b4bb1967c3ca439c3193db03d542	tree \| snapshot
parent	87ad71faeb3f544a3a21b2b57a589fc55543bae6	commit \| diff

new universes implementation

31 files changed:

helm/gTopLevel/gTopLevel.ml		diff \| blob \| history
helm/gTopLevel/proofEngine.ml		diff \| blob \| history
helm/gTopLevel/testlibrary.ml		diff \| blob \| history
helm/ocaml/cic/cicUniv.ml		diff \| blob \| history
helm/ocaml/cic/cicUniv.mli		diff \| blob \| history
helm/ocaml/cic_disambiguation/disambiguate.ml		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicEnvironment.ml		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicEnvironment.mli		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicTypeChecker.ml		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicTypeChecker.mli		diff \| blob \| history
helm/ocaml/cic_unification/cicRefine.ml		diff \| blob \| history
helm/ocaml/getter/.depend		diff \| blob \| history
helm/ocaml/tactics/.depend		diff \| blob \| history
helm/ocaml/tactics/Makefile		diff \| blob \| history
helm/ocaml/tactics/discriminationTactics.ml		diff \| blob \| history
helm/ocaml/tactics/eliminationTactics.ml		diff \| blob \| history
helm/ocaml/tactics/equalityTactics.ml		diff \| blob \| history
helm/ocaml/tactics/fourierR.ml		diff \| blob \| history
helm/ocaml/tactics/introductionTactics.ml		diff \| blob \| history
helm/ocaml/tactics/negationTactics.ml		diff \| blob \| history
helm/ocaml/tactics/primitiveTactics.ml		diff \| blob \| history
helm/ocaml/tactics/proofEngineStructuralRules.ml		diff \| blob \| history
helm/ocaml/tactics/proofEngineTypes.ml		diff \| blob \| history
helm/ocaml/tactics/proofEngineTypes.mli	[new file with mode: 0644]	blob
helm/ocaml/tactics/reductionTactics.ml		diff \| blob \| history
helm/ocaml/tactics/ring.ml		diff \| blob \| history
helm/ocaml/tactics/statefulProofEngine.ml		diff \| blob \| history
helm/ocaml/tactics/tacticChaser.ml		diff \| blob \| history
helm/ocaml/tactics/tacticals.ml		diff \| blob \| history
helm/ocaml/tactics/variousTactics.ml		diff \| blob \| history
helm/ocaml/tactics/variousTactics.mli		diff \| blob \| history

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

RSS Atom