]> matita.cs.unibo.it Git - helm.git/commit - matita/components/ng_refiner/nCicUnification.ml
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 95b2fec) | patch
New behaviour of fo_unif: in case of ?f args == t args'
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 25 Nov 2010 11:45:10 +0000 (11:45 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 25 Nov 2010 11:45:10 +0000 (11:45 +0000)
commit48a389fa5b4c7d80f97c8c6c7a1f47e840977f39
treeeba6d47810514e1f61b8c94c0118c4d280559199tree | snapshot
parent95b2fec522138b2a17e6f8ddc71683eb9dbf3413commit | diff
New behaviour of fo_unif: in case of  ?f args == t args'
where at least one args is flexible, it now unifies in parallel even if the
two args have different lenghts (as in the old version of Matita).
matita/components/ng_refiner/nCicUnification.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.