From d46ed1de8e9c928eed1121ae77bd308ecb88205b Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 7 Nov 2010 23:35:56 +0000 Subject: Delayed the evar normalization in error messages to the last minute before the message is delivered to the user. Should avoid useless computation in heavily backtracking tactics (auto, try, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13628 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/unification.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'pretyping/unification.ml') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 38cf59bc0..6c17567c3 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -844,7 +844,7 @@ let w_unify_to_subterm env ?(flags=default_unify_flags) (op,cl) evd = in try matchrec cl with ex when precatchable_exception ex -> - raise (PretypeError (env,NoOccurrenceFound (op, None))) + raise (PretypeError (env,evd,NoOccurrenceFound (op, None))) (* Tries to find all instances of term [cl] in term [op]. Unifies [cl] to every subterm of [op] and return all the matches. @@ -906,7 +906,7 @@ let w_unify_to_subterm_all env ?(flags=default_unify_flags) (op,cl) evd = in let res = matchrec cl [] in if res = [] then - raise (PretypeError (env,NoOccurrenceFound (op, None))) + raise (PretypeError (env,evd,NoOccurrenceFound (op, None))) else res @@ -922,7 +922,7 @@ let w_unify_to_subterm_list env flags allow_K hdmeta oplist t evd = try (* This is up to delta for subterms w/o metas ... *) w_unify_to_subterm env ~flags (strip_outer_cast op,t) evd - with PretypeError (env,NoOccurrenceFound _) when allow_K -> (evd,op) + with PretypeError (env,_,NoOccurrenceFound _) when allow_K -> (evd,op) in if not allow_K && (* ensure we found a different instance *) List.exists (fun op -> eq_constr op cl) l @@ -932,7 +932,7 @@ let w_unify_to_subterm_list env flags allow_K hdmeta oplist t evd = (evd,op::l) else (* This is not up to delta ... *) - raise (PretypeError (env,NoOccurrenceFound (op, None)))) + raise (PretypeError (env,evd,NoOccurrenceFound (op, None)))) oplist (evd,[]) @@ -996,13 +996,13 @@ let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd = with ex when precatchable_exception ex -> try w_unify2 env flags allow_K cv_pb ty1 ty2 evd - with PretypeError (env,NoOccurrenceFound _) as e -> raise e) + with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e) (* Second order case *) | (Meta _, true, _, _ | _, _, Meta _, true) -> (try w_unify2 env flags allow_K cv_pb ty1 ty2 evd - with PretypeError (env,NoOccurrenceFound _) as e -> raise e + with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e | ex when precatchable_exception ex -> try w_typed_unify env cv_pb flags ty1 ty2 evd -- cgit v1.2.3