diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d6c24e9cc..6f7e61f6b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1579,11 +1579,11 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in let indmv = destMeta sigma (nth_arg sigma i elimclause.templval.rebus) in let hypmv = - try match List.remove Int.equal indmv (clenv_independent elimclause) with - | [a] -> a - | _ -> failwith "" - with Failure _ -> user_err ~hdr:"elimination_clause" - (str "The type of elimination clause is not well-formed.") in + match List.remove Int.equal indmv (clenv_independent elimclause) with + | [a] -> a + | _ -> user_err ~hdr:"elimination_clause" + (str "The type of elimination clause is not well-formed.") + in let elimclause' = clenv_fchain ~flags indmv elimclause indclause in let hyp = mkVar id in let hyp_typ = Retyping.get_type_of env sigma hyp in |