]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: eec7beb) | patch
- added support for contexts (terms with holes)
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 11 Jan 2005 16:01:46 +0000 (16:01 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 11 Jan 2005 16:01:46 +0000 (16:01 +0000)
commitb24d13c4dcc96a204951857ddfa18c5ded4cecd0
tree5dbac22e28f11b4708262ca0b61439e303f22ab8tree | snapshot
parenteec7bebeef825af62d31a75686e62ab3a1c9b202commit | diff
- added support for contexts (terms with holes)
- added CicUtil.pack/unpack to pack/unpack several terms in a single term
- added CicUtil.strip_prods to removed a given number of head prods from a term
- added CicUtil.context_of/select to create contexts/select a subterm
  matching a context
helm/ocaml/cic/cic.ml diff | blob | history
helm/ocaml/cic/cicUtil.ml diff | blob | history
helm/ocaml/cic/cicUtil.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.