]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a15e3ba) | 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)
commit589ea43c8916e765e43f27b80a2596010527042c
treed83750e58b6ae54df153619c8c3263f05968bae4tree | snapshot
parenta15e3bafc1c4b8e5d12fbf562531becc0153edfecommit | 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.
helm/software/components/tactics/metadataQuery.ml diff | blob | history
helm/software/components/tactics/paramodulation/equality.ml diff | blob | history
helm/software/components/tactics/paramodulation/equality_retrieval.ml diff | blob | history
helm/software/matita/library/nat/ord.ma diff | blob | history
helm/software/matita/library/nat/relevant_equations.ma diff | blob | history
helm/software/matita/tests/applys.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.