]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: aa654b2) | patch
1. fix_arity fixed: the code is totally wrong and this is just a quic&dirty
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 7 Sep 2007 17:58:54 +0000 (17:58 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 7 Sep 2007 17:58:54 +0000 (17:58 +0000)
commit5ec87fab28597f651b2792081da2264504f2dbf1
treee6f2e1f0adef55cf2a2afcaffec52026b1451c2ctree | snapshot
parentaa654b256f9deca4ed5bb2b13b87e1d69377f17dcommit | diff
1. fix_arity fixed: the code is totally wrong and this is just a quic&dirty
   fix
2. first real-word example in coercions_russel: a certified "find" procedure
   from the ocaml library

Note: removing the (... : Prop) cast from the example, unification fails badly.
To be understood and fixed somehow (i.e. with an Uncertain in place of a
Failure).
helm/software/components/cic_unification/cicRefine.ml diff | blob | history
helm/software/matita/tests/coercions_propagation.ma diff | blob | history
helm/software/matita/tests/coercions_russell.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.