diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 6 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
4 files changed, 7 insertions, 7 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 0ed754f6f8..0144fbb34c 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 = diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 0490f1bc89..f9c8e47fd7 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -578,7 +578,7 @@ let hResolve id c occ t gl = try Pretyping.Default.understand sigma env t_hole with - | Loc.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) -> + | Loc.Exc_located (loc,Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _)) -> resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole) in let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 99cbfe4980..860f162dbc 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1532,7 +1532,7 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl = with RewriteFailure -> let {l2r=l2r; c1=x; c2=y} = hypinfo in raise (Pretype_errors.PretypeError - (pf_env gl, + (pf_env gl,project gl, Pretype_errors.NoOccurrenceFound ((if l2r then x else y), cl))) let general_s_rewrite_clause x = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d18b540de7..2c4201f99f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -787,9 +787,9 @@ let simplest_elim c = default_elim false (c,NoBindings) let clenv_fchain_in id elim_flags mv elimclause hypclause = try clenv_fchain ~allow_K:false ~flags:elim_flags mv elimclause hypclause - with PretypeError (env,NoOccurrenceFound (op,_)) -> + with PretypeError (env,evd,NoOccurrenceFound (op,_)) -> (* Set the hypothesis name in the message *) - raise (PretypeError (env,NoOccurrenceFound (op,Some id))) + raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id))) let elimination_in_clause_scheme with_evars id i elimclause indclause gl = let indmv = destMeta (nth_arg i elimclause.templval.rebus) in |