]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4ccb69a) | patch
- changed moo representation in MatitaTypes.status, no longer a string list, but...
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 13 Sep 2005 13:27:53 +0000 (13:27 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 13 Sep 2005 13:27:53 +0000 (13:27 +0000)
commitf2551cc0cc563b34b88a70a6bb0ef5e352a5d542
tree7f4b91b9c376bea77abfba4c577c7f71da24213atree | snapshot
parent4ccb69a58caed6f5da5b64abaf9f65c7a38f8cc3commit | diff
- changed moo representation in MatitaTypes.status, no longer a string list, but a command (in AST format) list
- fixed redundancy in moo: aliases, interpretation, and default commands are always present only once in a single moo
- added MatitaTypes.add_moo_content: from now on it must be then only function used to add content to moo objects
helm/matita/matitaEngine.ml diff | blob | history
helm/matita/matitaSync.ml diff | blob | history
helm/matita/matitaTypes.ml diff | blob | history
helm/matita/matitaTypes.mli diff | blob | history
helm/matita/matitacLib.ml diff | blob | history
helm/matita/matitacLib.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.