]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 61948e2) | patch
Better (but still broken) fix for the case ?sort vs ?term.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 30 Sep 2009 12:55:49 +0000 (12:55 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 30 Sep 2009 12:55:49 +0000 (12:55 +0000)
commit7ca0a000878e864c92d94f77900bc2ca0ac143b9
tree9074cefe133f84a763c57079fdfc2fe3314f7d6ftree | snapshot
parent61948e2e9b31460eb6a0bbd627c90a6549d65414commit | diff
Better (but still broken) fix for the case ?sort vs ?term.
To implement the right thing, we need to be able to mark metas as sort without
using the fact that their type is an Implicit.
helm/software/components/ng_refiner/nCicUnification.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.