]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 75514fe) | patch
1) better implementation of NObj that now calls recursively NQed
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 8 May 2009 16:47:23 +0000 (16:47 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 8 May 2009 16:47:23 +0000 (16:47 +0000)
commitef9c7ecffee95d77cd10fa2d37bd2b26b94b9eb9
tree7cc8e9a41a184ea6956665bccd16aeb12c14666dtree | snapshot
parent75514fe2207992ebc549822a7cbd5d37688690accommit | diff
1) better implementation of NObj that now calls recursively NQed
   to avoid code duplication
2) NQed now calls the kernel to check the object, since add_obj is too
   low level for that (this makes a huge difference with the previous
   architecture, but will probably break when dealing with undo)
helm/software/components/grafite_engine/grafiteEngine.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.