]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 79684e8) | patch
to me, the problem:
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 10 Sep 2009 14:41:22 +0000 (14:41 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 10 Sep 2009 14:41:22 +0000 (14:41 +0000)
commit686f7f4f4444125885bc7ef9e8ec3e0b6f567137
treef8d9db3f3d7e85478d0aa0779068d8fbca8c9dc0tree | snapshot
parent79684e8bd0f54b5c88fff981366bd8c78dd0fbe9commit | diff
to me, the problem:
  ? t ==?== ?->?
where the first ? has an empty local context
is always Uncertain... to be fully understood
why unification gives Failure. It may be correct if
t has type (Rel k). I wrap it in the refiner.
helm/software/components/ng_refiner/nCicRefiner.ml diff | blob | history
helm/software/components/ng_refiner/nCicUnification.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.