]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1dd2a5f) | patch
alpha equivalence fixed: in the case "meta against meta" we did not recur on theexpli...
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 4 Apr 2007 15:01:50 +0000 (15:01 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 4 Apr 2007 15:01:50 +0000 (15:01 +0000)
commitf8791fd4e018c691d1b22a4fe748bc57f79f1b89
treebbda6d65fb0f50bae7aec5269e071bf8a6220132tree | snapshot
parent1dd2a5ffce1a935d18372d298e0d85df96ef53bdcommit | diff
alpha equivalence fixed: in the case "meta against meta" we did not recur on theexplicit substitutions. The case "Type against Type" and "Implicit against Implicit" need to be checked. Are we really sure that structural equality is enough?
(when we compare universes and implict annotations)
components/acic_procedural/acic2Procedural.ml diff | blob | history
components/cic/cicUtil.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.