diff options
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 0ed754f6f..0144fbb34 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -134,10 +134,10 @@ let general_elim_clause with_evars cls rew elim = an extra condition *) tclNOTSAMEGOAL (rewrite_elim with_evars rew elim ~allow_K:false) | Some id -> rewrite_elim_in with_evars id rew elim) - with Pretype_errors.PretypeError (env, - (Pretype_errors.NoOccurrenceFound (c', _))) -> + with Pretype_errors.PretypeError (env,evd, + Pretype_errors.NoOccurrenceFound (c', _)) -> raise (Pretype_errors.PretypeError - (env, (Pretype_errors.NoOccurrenceFound (c', cls)))) + (env,evd,Pretype_errors.NoOccurrenceFound (c', cls))) let general_elim_clause with_evars tac cls sigma c t l l2r elim gl = let all, firstonly, tac = |