added @raise in comment (and source)

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 22b6c8487a8348d74a80f896c501a26f3263aba1..284098f3bae4fba29446eb66388b56b641380f2f 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -227,6 +227,12 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
   let add_ctx context name entry =
       (Some (name, entry)) :: context
   in
+  let map2 error_msg f l1 l2 = 
+    try 
+      List.map2 f l1 l2 
+    with
+    | Invalid_argument _ -> raise (Bad_pattern error_msg)
+  in
   let rec aux context where term =
     match (where, term) with
     | Cic.Implicit (Some `Hole), t -> [context,t]
@@ -234,7 +240,7 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
     | Cic.Implicit None,_ -> []
     | Cic.Meta (_, ctxt1), Cic.Meta (_, ctxt2) ->
         List.concat
-          (List.map2
+          (map2 "wrong number of argument in explicit substitution"
             (fun t1 t2 ->
               (match (t1, t2) with
                   Some t1, Some t2 -> aux context t1 t2
@@ -271,7 +277,7 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
         List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2
        in
         List.concat
-          (List.map2
+          (map2 "wrong number of mutually recursive functions"
             (fun (_, _, ty1, bo1) (_, _, ty2, bo2) -> 
               aux context ty1 ty2 @ aux (tys @ context) bo1 bo2)
             funs1 funs2)
@@ -280,7 +286,7 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
         List.map (fun (n,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) funs2
        in
         List.concat
-          (List.map2
+          (map2 "wrong number of mutually co-recursive functions"
             (fun (_, ty1, bo1) (_, ty2, bo2) ->
               aux context ty1 ty2 @ aux (tys @ context) bo1 bo2)
             funs1 funs2)
@@ -290,7 +296,8 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
                   (CicPp.ppterm x)
                   (CicPp.ppterm y)))
   and auxs context terms1 terms2 =  (* as aux for list of terms *)
-    List.concat (List.map2 (fun t1 t2 -> aux context t1 t2) terms1 terms2)
+    List.concat (map2 "wrong number of arguments in application"
+      (fun t1 t2 -> aux context t1 t2) terms1 terms2)
   in
    let context_len = List.length context in
    let roots = aux context where term in
@@ -462,7 +469,10 @@ exception Fail of string
   * with their context conclusion. Note: in the result the list of hypothesis
   * has an entry for each entry in the context and in the same order.
   * Of course the list of terms (with their context) associated to the
-  * hypothesis name may be empty. *)
+  * hypothesis name may be empty. 
+  *
+  * @raise Bad_pattern
+  * *)
   let select ~metasenv ~ugraph ~conjecture:(_,context,ty)
        ~pattern:(what,hyp_patterns,goal_pattern)
   =

diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli
index 859f1f4bac35096d0844f15c7718fef3577be179..4dad92917cb1b43204fefae62bdbb3ea130f6464 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.mli
+++ b/helm/ocaml/tactics/proofEngineHelpers.mli
@@ -68,7 +68,10 @@ val pattern_of:
 * subterms of the conclusion with their context. Note: in the result the list
 * of hypotheses * has an entry for each entry in the context and in the same
 * order. Of course the list of terms (with their context) associated to one
-* hypothesis may be empty. *)
+* hypothesis may be empty. 
+*
+* @raise Bad_pattern
+* *)
 val select:
  metasenv:Cic.metasenv ->
  ugraph:CicUniv.universe_graph ->