]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b4027b8) | 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)
commit579d312fed0670e7528e106d2df94d72a18ee277
treeebde259dce5305352d45b8d86c1bc1d3bfa8da81tree | snapshot
parentb4027b84fae91e907b6874060b91d89b6a1ad780commit | 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)
helm/software/components/acic_procedural/acic2Procedural.ml diff | blob | history
helm/software/components/cic/cicUtil.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.