]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0972948) | patch
fixed propagation under Fix/Lambda/Case of coercions, better names are
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 7 Sep 2007 09:59:52 +0000 (09:59 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 7 Sep 2007 09:59:52 +0000 (09:59 +0000)
commitc2c8816478b504e236cdc7f10cb96ca66dc33c32
tree8ff281d5703708c8c7d7558b057d3437c2ad4d58tree | snapshot
parent0972948bb0b578df99c1bf6ae7c805418b11206acommit | diff
fixed propagation under Fix/Lambda/Case of coercions, better names are
generated.

there is still a question for CSC about the context of the metavariables opened
by example 51 that seems too long.

code still needs some refactoring, auxiliary functions are ready to be
lambdalifet out.

potential slowdown: The coerce_atom_to_something now looks for the *best*
coercion, where best means the one that opens the least number of metas.
helm/software/components/cic_unification/cicRefine.ml diff | blob | history
helm/software/matita/tests/coercions_propagation.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.