]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bc7d32f) | patch
Function to map NCic.term to CicNotationPt.term finished.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 24 Jul 2009 21:24:46 +0000 (21:24 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 24 Jul 2009 21:24:46 +0000 (21:24 +0000)
commit4b85428dfb96b90fc8f00402b21affad9d99f905
tree76cef9037d53762dd2053724b046525b693da2cbtree | snapshot
parentbc7d32fd5c34cc2ac0edff13292662585e6ffa51commit | diff
Function to map NCic.term to CicNotationPt.term finished.
Note: it is almost identical to ncic_of_ast0, but it uses a different data
type for contexts that allow to perform "substitution" in a single operation.
Moreover, the terms that are substituted are CicNotationPt.terms and not
NCic.terms. The two codes really ought to be unified.
helm/software/components/ng_tactics/nCicElim.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.