]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 01b29f4) | patch
- content/interpretations.ml and ng_cic_content/nTermCicContent.ml where
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 4 Nov 2010 20:26:10 +0000 (20:26 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 4 Nov 2010 20:26:10 +0000 (20:26 +0000)
commit551861bf1adbb1db5b0b9941b98ba54531157364
tree9aa4d655d7a3e7dec6d322b1b75caabfe73259ddtree | snapshot
parent01b29f47d0d3e6c131fbdcc7a4180d428c8c97b9commit | diff
- content/interpretations.ml and ng_cic_content/nTermCicContent.ml where
  mutually recursive and part of the status was kept imperatively;
  the two files have been merged together into ng_cic_content/interpretations.ml
18 files changed:
matita/components/METAS/meta.helm-ng_disambiguation.src diff | blob | history
matita/components/Makefile diff | blob | history
matita/components/content/.depend diff | blob | history
matita/components/content/Makefile diff | blob | history
matita/components/content/interpretations.ml [deleted file] blob | history
matita/components/content/interpretations.mli [deleted file] blob | history
matita/components/content_pres/content2pres.mli diff | blob | history
matita/components/content_pres/sequent2pres.mli diff | blob | history
matita/components/ng_cic_content/.depend diff | blob | history
matita/components/ng_cic_content/Makefile diff | blob | history
matita/components/ng_cic_content/interpretations.ml [new file with mode: 0644] blob
matita/components/ng_cic_content/interpretations.mli [new file with mode: 0644] blob
matita/components/ng_cic_content/nTermCicContent.ml [deleted file] blob | history
matita/components/ng_cic_content/nTermCicContent.mli [deleted file] blob | history
matita/components/statuses.txt diff | blob | history
matita/matita/applyTransformation.ml diff | blob | history
matita/matita/applyTransformation.mli diff | blob | history
matita/matita/matitaGui.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.