aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/Makefile.rt
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-02 15:03:28 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-02 16:17:30 +0200
commit6a736c77dee9315afd6d5f50375bf92c1da5d20c (patch)
tree1047b1578024ad227679d025714620bd611120d4 /doc/Makefile.rt
parent351adedc4d154f9f60a3a01b2e906ce2063e323f (diff)
Completing fixing order of parameters when translating from
glob_constr to constr_pattern. Was partially fixed to solve #3088 (8e88b7adab) in but the order of lambdas was still incorrect as the fix of the order of lambdas in second-order pattern-matching for #3136 showed (83159124ce22).
Diffstat (limited to 'doc/Makefile.rt')
0 files changed, 0 insertions, 0 deletions