]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 589abc8) | patch
Record projections:
authorWilmer Ricciotti <ricciott@cs.unibo.it>
Thu, 12 May 2011 15:59:10 +0000 (15:59 +0000)
committerWilmer Ricciotti <ricciott@cs.unibo.it>
Thu, 12 May 2011 15:59:10 +0000 (15:59 +0000)
commitbe742cc27bb15a8c7bd9cf030e8a16f266e36f03
tree88494781baab0a23b26d46b7e971336b995b8b13tree | snapshot
parent589abc887494582fb011df38897bb142d6da42c9commit | diff
Record projections:
no need to synthesize an ast term from a CIC term: just use NotationPt.NCic ;
this also fixes a bug that used to prevent generation of projections when the
types of some fields was associated to a notation (example: natural numbers
expressed using \naturals).
matita/components/ng_tactics/nCicElim.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.