]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8272528) | patch
- sort inclusion must be restricted to term backbone in order to avoid
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 20 Aug 2009 09:57:51 +0000 (09:57 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 20 Aug 2009 09:57:51 +0000 (09:57 +0000)
commitbc9fca01f135aecc2940e7318f77fea34fd6ef30
tree0e546c26ad99225341445be60ecf41fa1144c0eatree | snapshot
parent8272528f48b942a80024aeb9b625d99cfe3f0f44commit | diff
- sort inclusion must be restricted to term backbone in order to avoid
validity of non-normalizing terms (see the omega.aut example)
- command-line options -a and -p rearranged
helm/software/lambda-delta/automath/omega.aut [new file with mode: 0644] blob
helm/software/lambda-delta/basic_rg/brgReduction.ml diff | blob | history
helm/software/lambda-delta/toplevel/top.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.