]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3a0c716) | patch
new internal flags for auto:
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 5 Nov 2008 21:29:05 +0000 (21:29 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 5 Nov 2008 21:29:05 +0000 (21:29 +0000)
commit87fdda71e8e0dcf886852f70be9a4b3d627b8e9c
tree7953512406a976613e9bd69fd0f588aeee2409f8tree | snapshot
parent3a0c71609f757f4ad3aadd234b84486fec97b791commit | diff
new internal flags for auto:
- skip_context
- skip_trie_filtering

together they allow a decent semantics for
by H, H1, H2 we proved foo.

since only H, H1 and H2 are used (no other context entry, not library stuff)
and full blown unification is used (no terms are ignored, between the one
specified, because they fail a trie search)
helm/software/components/tactics/auto.ml diff | blob | history
helm/software/components/tactics/autoTypes.ml diff | blob | history
helm/software/components/tactics/autoTypes.mli diff | blob | history
helm/software/components/tactics/declarative.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.