]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3a5ad4a) | patch
Big change:
authorAndrea Asperti <andrea.asperti@unibo.it>
Fri, 10 Dec 2010 12:35:26 +0000 (12:35 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Fri, 10 Dec 2010 12:35:26 +0000 (12:35 +0000)
commitfa3139698294b99889afd375298f9b071cdfbd67
treea68f578808d2540a6fd4b19ac17c1da0776df5d3tree | snapshot
parent3a5ad4a99fd7f312424200a9241ea1a4ce7fcd29commit | diff
Big change:
 - new command "include alias" to include only the aliases
 - "include" now always includes the aliases and it includes everything else
   only if the file has not been already included
matita/components/grafite/grafiteAst.ml diff | blob | history
matita/components/grafite_engine/grafiteEngine.ml diff | blob | history
matita/components/grafite_engine/nCicCoercDeclaration.ml diff | blob | history
matita/components/grafite_parser/grafiteParser.ml diff | blob | history
matita/components/ng_library/nCicLibrary.ml diff | blob | history
matita/components/ng_library/nCicLibrary.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.