]> matita.cs.unibo.it Git - fireball-separation.git/commit
projects / fireball-separation.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d3e73f8) | patch
subst does not replace anymore in branches of maches
authoracondolu <andrea.condoluci@unibo.it>
Sun, 16 Jul 2017 14:01:21 +0000 (16:01 +0200)
committeracondolu <andrea.condoluci@unibo.it>
Mon, 28 May 2018 09:10:57 +0000 (11:10 +0200)
commitaee2672094ae2dc02d7bbafd566b279e3c1c53f5
tree00378046075645153b70178cad824aef0baa77b4tree | snapshot
parentd3e73f866de30503a4c44d67cdd9e8ff77c15fc3commit | diff
subst does not replace anymore in branches of maches

It was unnecessary: a match cannot expand to a previous branch

(cherry picked from commit 8a90160900bb95133b8e204a4fcadaa2db2f11dd)
ocaml/num.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.