]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e892d4c) | 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)
commit01b688447c18c1992b0c19ac5583ca9fee692514
tree8b076d60d3fc504b7482fbab331377316b668c06tree | snapshot
parente892d4cb9d19305ff88aa1b7dba6e3eaee41fd92commit | 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.
components/cic_unification/cicRefine.ml diff | blob | history
matita/tests/coercions_propagation.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.