]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bbe7741) | patch
Incredible bug of simpl fixed: the stack (in the terminology used for the
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 29 Jun 2005 15:17:19 +0000 (15:17 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 29 Jun 2005 15:17:19 +0000 (15:17 +0000)
commitd774aa49f50598f725ded815b87949110a6acdcf
tree557acdd83aae5ac6bcbf332f29d4956fffe7d396tree | snapshot
parentbbe7741f3bbaacb93f2876c018dace82f5e929b8commit | diff
Incredible bug of simpl fixed: the stack (in the terminology used for the
Krivine's machine) was processed in the wrong context. As a result List.nth
(to get a Rel in the context) used to raise Failure in several cases. The
Failure, however, was catched somewhere in the code of matita and the
failure of simpl was hidden in most of the cases.
helm/ocaml/tactics/proofEngineReduction.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.