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