]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 23043db) | patch
a non necessary but morally required change. The matched term in
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 5 Feb 2009 10:48:28 +0000 (10:48 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 5 Feb 2009 10:48:28 +0000 (10:48 +0000)
commit02ae6637b48f03db431e5722243235710957c5b6
tree03927c5d9e2f297fcc5756f71034b34232c8f65etree | snapshot
parent23043db144b24b8cd2072800b61137bb396f891ecommit | diff
a non necessary but morally required change. The matched term in
are_convertible is compared with test_eq_only=true (not really needed since
if it reduces to something it is a constructor an thus an application that already honors the test_eq_only=true check for arguments
helm/software/components/cic_proof_checking/cicReduction.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.