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

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

author	Enrico Tassi <enrico.tassi@inria.fr>
	Wed, 1 Dec 2004 09:42:42 +0000 (09:42 +0000)
committer	Enrico Tassi <enrico.tassi@inria.fr>
	Wed, 1 Dec 2004 09:42:42 +0000 (09:42 +0000)
commit	31851952e1cc2db59168c5fd6f6093d9bc37ea86
tree	a048deac3243d5f00396cdce514e7589f2e08256	tree \| snapshot
parent	e09713d333183e929f108ff8bb8fbe2a25bfcac7	commit \| diff

Added universes handling. The PRE_UNIVERSES tag may help ;)

53 files changed:

helm/ocaml/METAS/meta.helm-cic.src		diff \| blob \| history
helm/ocaml/cic/Makefile		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_disambiguation/disambiguate.mli		diff \| blob \| history
helm/ocaml/cic_disambiguation/disambiguateTypes.ml		diff \| blob \| history
helm/ocaml/cic_disambiguation/disambiguateTypes.mli		diff \| blob \| history
helm/ocaml/cic_omdoc/cic2acic.ml		diff \| blob \| history
helm/ocaml/cic_omdoc/cic2content.ml		diff \| blob \| history
helm/ocaml/cic_omdoc/doubleTypeInference.ml		diff \| blob \| history
helm/ocaml/cic_omdoc/eta_fixing.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/cicEnvironment.ml		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicEnvironment.mli		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicPp.ml		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicReduction.mli		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicReductionMachine.ml		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicReductionMachine.mli		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicReductionNaif.ml		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicReductionNaif.mli		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicSubstitution.ml		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_proof_checking/cicUnivUtils.ml	[new file with mode: 0644]	blob
helm/ocaml/cic_proof_checking/cicUnivUtils.mli	[new file with mode: 0644]	blob
helm/ocaml/cic_transformations/acic2Ast.ml		diff \| blob \| history
helm/ocaml/cic_transformations/content_expressions.ml	[new file with mode: 0644]	blob
helm/ocaml/cic_unification/cicRefine.ml		diff \| blob \| history
helm/ocaml/cic_unification/cicRefine.mli		diff \| blob \| history
helm/ocaml/cic_unification/cicUnification.ml		diff \| blob \| history
helm/ocaml/cic_unification/cicUnification.mli		diff \| blob \| history
helm/ocaml/cic_unification/freshNamesGenerator.ml		diff \| blob \| history
helm/ocaml/getter/.depend		diff \| blob \| history
helm/ocaml/getter/http_getter.ml		diff \| blob \| history
helm/ocaml/getter/http_getter_misc.ml		diff \| blob \| history
helm/ocaml/mathql_generator/cGMatchConclusion.ml		diff \| blob \| history
helm/ocaml/metadata/.depend		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/metadataQuery.ml		diff \| blob \| history
helm/ocaml/tactics/negationTactics.ml		diff \| blob \| history
helm/ocaml/tactics/primitiveTactics.ml		diff \| blob \| history
helm/ocaml/tactics/proofEngineReduction.ml		diff \| blob \| history
helm/ocaml/tactics/proofEngineStructuralRules.ml		diff \| blob \| history
helm/ocaml/tactics/proofEngineTypes.ml		diff \| blob \| history
helm/ocaml/tactics/ring.ml		diff \| blob \| history
helm/ocaml/tactics/tacticChaser.ml	[new file with mode: 0644]	blob
helm/ocaml/tactics/tactics.mli		diff \| blob \| history
helm/ocaml/tactics/variousTactics.ml		diff \| blob \| history
helm/ocaml/utf8_macros/utf8MacroTable.ml		diff \| blob \| history

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

RSS Atom