]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: be742cc) | patch
Record projections:
authorWilmer Ricciotti <ricciott@cs.unibo.it>
Thu, 12 May 2011 16:03:08 +0000 (16:03 +0000)
committerWilmer Ricciotti <ricciott@cs.unibo.it>
Thu, 12 May 2011 16:03:08 +0000 (16:03 +0000)
commit3ffb8f47701d127211a095d3b9f64d363760430f
tree6444685d793dddd9c992cddad9baee4ed464eae4tree | snapshot
parentbe742cc27bb15a8c7bd9cf030e8a16f266e36f03commit | 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).
matitaB/components/ng_tactics/nCicElim.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.