diff --git a/src/ecParser.mly b/src/ecParser.mly index 93af2b5dd5..8762fbce6d 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -3267,7 +3267,7 @@ smt_info: smt_info1: | t=word - { `MAXLEMMAS (Some t) } + { `MAXLEMMAS (Some t) } | TIMEOUT EQ t=word { `TIMEOUT t } diff --git a/src/ecUtils.ml b/src/ecUtils.ml index 7528a02879..bba47f8ad7 100644 --- a/src/ecUtils.ml +++ b/src/ecUtils.ml @@ -642,18 +642,16 @@ module String = struct then List.map fst matched else aux matched (i+1) end - in aux matched 0 let last_matching tomatch s = - first_matching (List.map rev tomatch) (rev s) + List.map rev (first_matching (List.map rev tomatch) (rev s)) end let option_matching tomatch s = match OptionMatching.all_matching tomatch s with - | [s] -> [s] | matched -> - match OptionMatching.first_matching matched s with - | [s] -> [s] | matched -> OptionMatching.last_matching matched s + | [s] -> [s] + | matched -> OptionMatching.first_matching matched s end (* -------------------------------------------------------------------- *)