]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e11e617) | patch
commented out are_convertible in is_identity
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 3 Oct 2006 16:08:31 +0000 (16:08 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 3 Oct 2006 16:08:31 +0000 (16:08 +0000)
commitcae7dd50468e5ba0dec9d3cf4fa14daee2c3da2e
treefe0f6f8ba88b8270a83e305d84eec8af99e64e7dtree | snapshot
parente11e617809bbf3757ddfcbd6ef6d28d20e14a4f0commit | diff
commented out are_convertible in is_identity
fixed metadataquery so that only are calculated without the DB (but are calculated)
removed is_meta_convertible left right in is_weak_identity
added extra dependencies between gcd < relevant_equations < ord to make
paramodulation happy. In the past this used to be the order used by make.
added an hack in applys.ma, since it used to work due to convertibility.
components/tactics/metadataQuery.ml diff | blob | history
components/tactics/paramodulation/equality.ml diff | blob | history
components/tactics/paramodulation/equality_retrieval.ml diff | blob | history
matita/library/nat/ord.ma diff | blob | history
matita/library/nat/relevant_equations.ma diff | blob | history
matita/tests/applys.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.