From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 28 Jul 2005 14:42:41 +0000 (+0000)
Subject: Bug fixed: locate_term_in_conjecture used to raise TermNotFound as soon as
X-Git-Tag: V_0_7_2~15
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=250f53b2bddee6abaab7d586cfecccdc3fc61467;p=helm.git

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.
---

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