diff options
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index bfaa7e5e4..d8d7661be 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -385,7 +385,7 @@ let rec get_names allow_conj = function | IntroOrAndPattern [l] -> if allow_conj then if l = [] then (None,[]) else - let l = List.map (fun id -> out_some (fst (get_names false id))) l in + let l = List.map (fun id -> Option.get (fst (get_names false id))) l in (Some (List.hd l), l) else error "Nested conjunctive patterns not allowed for inversion equations" |