]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: aa5f71b) | patch
include statement better implemented:
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 26 Sep 2008 12:28:15 +0000 (12:28 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 26 Sep 2008 12:28:15 +0000 (12:28 +0000)
commiteb9ca860db8cb06083765f7698179f16dee5303e
tree8a7b27227c17efc095685db366dda575b31279eetree | snapshot
parentaa5f71baeba0299c0d29be01798f7a1ad13656f9commit | diff
include statement better implemented:
- push/pop operation for both Lexicon and Grafite stuff, instead of reset
- this (if properly working) opens the doors to a completely functional
  matita status
helm/software/components/acic_content/termAcicContent.ml diff | blob | history
helm/software/components/acic_content/termAcicContent.mli diff | blob | history
helm/software/components/content_pres/cicNotationParser.ml diff | blob | history
helm/software/components/content_pres/cicNotationParser.mli diff | blob | history
helm/software/components/content_pres/termContentPres.ml diff | blob | history
helm/software/components/content_pres/termContentPres.mli diff | blob | history
helm/software/components/lexicon/cicNotation.ml diff | blob | history
helm/software/components/lexicon/cicNotation.mli diff | blob | history
helm/software/components/lexicon/lexiconSync.ml diff | blob | history
helm/software/components/lexicon/lexiconSync.mli diff | blob | history
helm/software/matita/matitaScript.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.