]> matita.cs.unibo.it Git - helm.git/commit - helm/matita/matitaScript.ml
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c487af1) | patch
Stupid bug of mine fixed: sometimes (Some ~-1) was used in place of None.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 9 Jan 2006 09:39:14 +0000 (09:39 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 9 Jan 2006 09:39:14 +0000 (09:39 +0000)
commit0b79601e4c529cacbba2b64f99f3548df412f254
tree3e4a4fc24c3cb2a64063741375d269006162f511tree | snapshot
parentc487af185e2592449e33c228a3e4ef9a3875dea5commit | diff
Stupid bug of mine fixed: sometimes (Some ~-1) was used in place of None.
Moreover the userGoal was retrieved before setting it.
helm/matita/matita.ml diff | blob | history
helm/matita/matitaMathView.ml diff | blob | history
helm/matita/matitaScript.ml diff | blob | history
helm/matita/matitaScript.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.