]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0ba52f4) | patch
when we build the elimination principle we fresh universes to not
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 11 Apr 2008 10:33:49 +0000 (10:33 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 11 Apr 2008 10:33:49 +0000 (10:33 +0000)
commit8d2fe36efcace8af46c8b478061c3fa8bb72bc04
tree21c8c84ac1b6600d18d150e2ea44e859c5208a0dtree | snapshot
parent0ba52f4592974fc2f4aeba0135cec03f07cf662dcommit | diff
when we build the elimination principle we fresh universes to not
generate tems with different
helm/software/components/library/cicElim.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.