diff options
| author | Arnaud Spiwack | 2014-02-27 14:07:43 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-02-27 14:46:37 +0100 |
| commit | d98fdf1ef5789f6d5420e52c34a33debf08584e9 (patch) | |
| tree | b61a0b679df7b56ff6180924395fa5671d4c9b8f /tactics | |
| parent | 4d6b938e90ecd9dbfb29a0af28a7d8b6a657ae17 (diff) | |
Code refactoring thanks to the new Monad module.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 098e45a4aa..d6139f5297 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1196,7 +1196,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = Proofview.tclZERO (Errors.UserError ("Equality.inj" , str "Failed to decompose the equality.")) else Proofview.tclBIND - (Proofview.list_map + (Proofview.Monad.List.map (fun (pf,ty) -> Tacticals.New.tclTHENS (cut ty) [Proofview.tclUNIT (); Proofview.V82.tactic (refine pf)]) (if l2r then List.rev injectors else injectors)) (fun _ -> tac (List.length injectors)) |