]> matita.cs.unibo.it Git - helm.git/commit
Universes introduction
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 23 Apr 2004 10:37:00 +0000 (10:37 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 23 Apr 2004 10:37:00 +0000 (10:37 +0000)
commitc5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944
treefc5a39a01398d779aa5a38eab183361061dce8ae
parent7af6bb6e640a44489bdab79a38300cf103e45bd4
Universes introduction
27 files changed:
helm/ocaml/cic/.depend
helm/ocaml/cic/Makefile
helm/ocaml/cic/cic.ml
helm/ocaml/cic/cicParser3.ml
helm/ocaml/cic/cicUniv.ml [new file with mode: 0644]
helm/ocaml/cic/cicUniv.mli [new file with mode: 0644]
helm/ocaml/cic_disambiguation/disambiguate.ml
helm/ocaml/cic_omdoc/cic2acic.ml
helm/ocaml/cic_omdoc/doubleTypeInference.ml
helm/ocaml/cic_proof_checking/cicPp.ml
helm/ocaml/cic_proof_checking/cicReductionMachine.ml
helm/ocaml/cic_proof_checking/cicReductionNaif.ml
helm/ocaml/cic_proof_checking/cicTypeChecker.ml
helm/ocaml/cic_textual_parser/cicTextualParser.mly
helm/ocaml/cic_transformations/.depend
helm/ocaml/cic_transformations/acic2Ast.ml
helm/ocaml/cic_transformations/cic2Xml.ml
helm/ocaml/cic_transformations/content_expressions.ml
helm/ocaml/cic_unification/cicMkImplicit.ml
helm/ocaml/cic_unification/cicRefine.ml
helm/ocaml/cic_unification/cicUnification.ml
helm/ocaml/getter/.depend
helm/ocaml/mathql_generator/cGSearchPattern.ml
helm/ocaml/mathql_interpreter/.depend
helm/ocaml/tactics/.depend
helm/ocaml/tactics/primitiveTactics.ml
helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly