]> matita.cs.unibo.it Git - helm.git/commit
implemented normalize (used in new_metasenv_for_apply)
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 31 May 2005 15:41:09 +0000 (15:41 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 31 May 2005 15:41:09 +0000 (15:41 +0000)
commit5530db2f72548a8c579ae5f9868cbd38290eb065
tree9e67b33e2cdf9624e23670ed1944f59815617ed3
parente2beb1cd1269cc4dd94c184b85193f0fbc935324
implemented normalize (used in new_metasenv_for_apply)
helm/ocaml/cic_proof_checking/cicReduction.ml
helm/ocaml/cic_proof_checking/cicReduction.mli
helm/ocaml/cic_proof_checking/cicSubstitution.ml
helm/ocaml/cic_unification/cicUnification.ml
helm/ocaml/tactics/primitiveTactics.ml