]> matita.cs.unibo.it Git - helm.git/commit
added oblivion_universe and used it in paxck_coercions
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 2 Jan 2007 18:03:59 +0000 (18:03 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 2 Jan 2007 18:03:59 +0000 (18:03 +0000)
commit001b43beae9e912a921da426d23c1e437328bb9e
treef07094e6a8f0a52b9f6efb1c656fbf052b278010
parentb70dd6eca72985b11d7d223b8a6a84fda44cdf69
added oblivion_universe and used it in paxck_coercions
components/cic/cicUniv.ml
components/cic/cicUniv.mli
components/cic/cicUtil.ml
components/cic/cicUtil.mli
components/cic_proof_checking/cicEnvironment.ml
components/cic_proof_checking/freshNamesGenerator.ml
components/cic_unification/cicRefine.ml