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 c9dc6c2c611194760e24bc42b17f0039904da959..b9ee8bb8fc8d72eb00e231ad0b9f531d6b6cd9ad 100644 (file)
--- 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