From 250f53b2bddee6abaab7d586cfecccdc3fc61467 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 28 Jul 2005 14:42:41 +0000 Subject: [PATCH] Bug fixed: locate_term_in_conjecture used to raise TermNotFound as soon as the term was not found in one of the hypotheses or in the conclusion. --- helm/ocaml/tactics/proofEngineHelpers.ml | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index c9dc6c2c6..b9ee8bb8f 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -623,28 +623,36 @@ let locate_in_term ?(equality=(==))what ~where context = * It may raise TermNotFound or TermFoundMultipleTimes *) let locate_in_conjecture ?(equality=(==)) what (_,context,ty) = - let (@@) (l1,l2) (l1',t) = l1 @ l1', l2 @ [t] in + let (@@) (l1,l2) = + function + None -> l1,l2 + | Some (l1',t) -> l1 @ l1', l2 @ [t] in + let locate_in_term what ~where context = + try + Some (locate_in_term ~equality what ~where context) + with + TermNotFound -> None in let context,res = List.fold_right (fun entry (context,res) -> match entry with None -> entry::context, res | Some (_, Cic.Decl ty) -> - let res = res @@ locate_in_term ~equality what ~where:ty context in + let res = res @@ locate_in_term what ~where:ty context in let context' = entry::context in context',res | Some (_, Cic.Def (bo,ty)) -> - let res = res @@ locate_in_term ~equality what ~where:bo context in + let res = res @@ locate_in_term what ~where:bo context in let res = match ty with None -> res | Some ty -> - res @@ locate_in_term ~equality what ~where:ty context in + res @@ locate_in_term what ~where:ty context in let context' = entry::context in context',res ) context ([],([],[])) in - let res = res @@ locate_in_term ~equality what ~where:ty context in + let res = res @@ locate_in_term what ~where:ty context in match res with context,[] -> raise TermNotFound | context,[_] -> context -- 2.39.2