]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2e7aca4) | patch
catch the right exception, avoid uncaught Subst_not_found
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 13 Apr 2010 19:53:31 +0000 (19:53 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 13 Apr 2010 19:53:31 +0000 (19:53 +0000)
commit4edcf284d13d4f0f945234482fda852e7b7180c4
treefe37929b332a8d5c39c315df2af2ed8f9eee43fctree | snapshot
parent2e7aca462b7556a3a7369de030bbac8d8205aa92commit | diff
catch the right exception, avoid uncaught Subst_not_found

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>
helm/software/components/ng_refiner/nCicUnification.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.