]> matita.cs.unibo.it Git - helm.git/commit
new cicEnvironment implementation
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 17 Jan 2005 16:24:17 +0000 (16:24 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 17 Jan 2005 16:24:17 +0000 (16:24 +0000)
commit218c0062f93dd3221b0266cfbc26fd9cf787ad18
tree39eaa0e4f07cf3b739bc5468dcce5fbb196c7cdb
parent72e5ddf0f07b0e692f5e3544438f77f2e346b12a
new cicEnvironment implementation
20 files changed:
helm/gTopLevel/gTopLevel.ml
helm/gTopLevel/testlibrary.ml
helm/ocaml/cic_disambiguation/disambiguate.ml
helm/ocaml/cic_omdoc/cic2content.ml
helm/ocaml/cic_omdoc/doubleTypeInference.ml
helm/ocaml/cic_omdoc/eta_fixing.ml
helm/ocaml/cic_proof_checking/cicElim.ml
helm/ocaml/cic_proof_checking/cicEnvironment.ml
helm/ocaml/cic_proof_checking/cicEnvironment.mli
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/cicSubstitution.ml
helm/ocaml/cic_proof_checking/cicTypeChecker.ml
helm/ocaml/cic_proof_checking/cicUnivUtils.ml
helm/ocaml/cic_transformations/acic2Ast.ml
helm/ocaml/cic_unification/cicRefine.ml
helm/ocaml/tactics/discriminationTactics.ml
helm/ocaml/tactics/primitiveTactics.ml
helm/ocaml/tactics/proofEngineReduction.ml