]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0c7ccf8) | patch
1. we compare the expected branching with the actual one and
authorAndrea Asperti <andrea.asperti@unibo.it>
Thu, 3 Nov 2011 12:48:32 +0000 (12:48 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Thu, 3 Nov 2011 12:48:32 +0000 (12:48 +0000)
commitd6f1365a9f1cb48af8a7b32cf074373466779e7e
tree8a765e835960d42f29583ac19c4490658e504abbtree | snapshot
parent0c7ccf8fc6a32cb187b5464ff36e1ff0502ae054commit | diff
1. we compare the expected branching with the actual one and
   prune the candidate when the latter is larger. The optimization
   is meant to rule out stange applications of flexible terms,
   such as the application of eq_f that always succeeds.
2. At top level, we index local equalitites for paramodulation for
   each cluster (i.e. we assume metas in a same cluster shares the
   same context *)
matitaB/components/ng_tactics/nnAuto.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.