]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c5cd7e0) | patch
- use CicUtil.term_of_uri instead of deprecated HelmLibrayObjects
authorStefano Zacchiroli <zack@upsilon.cc>
Fri, 22 Oct 2004 09:54:49 +0000 (09:54 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Fri, 22 Oct 2004 09:54:49 +0000 (09:54 +0000)
commit1e61e4290c96600e3758b30b660712514ba379e3
tree0eafab318d2f0d6cd0f34cc61de86e7224f93a15tree | snapshot
parentc5cd7e02a5f443fdbd1151cd861e4723b91c8bcecommit | diff
- use CicUtil.term_of_uri instead of deprecated HelmLibrayObjects
  similar function
- reverted to old syntax for binders (e.g. \forall x,y:nat.x=y)
- use ";;" as phrases terminator
helm/ocaml/cic_disambiguation/cicTextualParser2.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.