]> matita.cs.unibo.it Git - helm.git/commit - helm/ocaml/cic_unification/cicUnification.ml
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f7a0f0c) | patch
A failing unification of a coercion vs a term is now tried again after
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 26 Jan 2006 17:50:09 +0000 (17:50 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 26 Jan 2006 17:50:09 +0000 (17:50 +0000)
commit1db3c6d81f853f98f145cd9924dd18b79ca846e9
treeaea375650903cee554e854beef19da64e0de851ftree | snapshot
parentf7a0f0c8e5bf52d3bfa946d32c42a0224fc9f789commit | diff
A failing unification of a coercion vs a term is now tried again after
a delta-beta weak head reduction of the coercion. This is necessary to handle
the case (f (g ?)) vs (fg t) where f and g are coercions and fg is the
composite coercion.

As a result the notation in algebra is now nicer and more notation can be
parsed.
helm/matita/library/algebra/groups.ma diff | blob | history
helm/matita/library/algebra/monoids.ma diff | blob | history
helm/ocaml/cic_unification/cicUnification.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.