experimental version

[helm.git] / helm / ocaml / tactics / proofEngineHelpers.ml

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 23aa20bfb50cb30d4483e5fd2c04400281ce7934..9f7fb42f4945a547d839878f158a3b8d3e8f8ca8 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -23,7 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception Bad_pattern of string
+exception Bad_pattern of string Lazy.t
 
 let new_meta_of_proof ~proof:(_, metasenv, _, _) =
   CicMkImplicit.new_meta metasenv []
@@ -231,7 +231,7 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
     try 
       List.map2 f l1 l2 
     with
-    | Invalid_argument _ -> raise (Bad_pattern error_msg)
+    | Invalid_argument _ -> raise (Bad_pattern (lazy error_msg))
   in
   let rec aux context where term =
     match (where, term) with
@@ -292,9 +292,9 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) =
             funs1 funs2)
     | x,y -> 
         raise (Bad_pattern 
-                (Printf.sprintf "Pattern %s versus term %s" 
+                (lazy (Printf.sprintf "Pattern %s versus term %s" 
                   (CicPp.ppterm x)
-                  (CicPp.ppterm y)))
+                  (CicPp.ppterm y))))
   and auxs context terms1 terms2 =  (* as aux for list of terms *)
     List.concat (map2 "wrong number of arguments in application"
       (fun t1 t2 -> aux context t1 t2) terms1 terms2)
@@ -455,7 +455,7 @@ let pattern_of ?(equality=(==)) ~term terms =
   in
    snd (aux term)
 
-exception Fail of string
+exception Fail of string Lazy.t
 
   (** select metasenv conjecture pattern
   * select all subterms of [conjecture] matching [pattern].
@@ -649,7 +649,7 @@ let saturate_term newmeta metasenv context ty goal_arity =
          in
           if prod_no + 1 = goal_arity then
            let head = CicReduction.normalize ~delta:false context ty in
-            head,[],[],newmeta,goal_arity + 1
+            head,[],[],lastmeta,goal_arity + 1
           else
            (** NORMALIZE RATIONALE 
             * we normalize the target only NOW since we may be in this case:
@@ -678,6 +678,6 @@ let lookup_type metasenv context hyp =
       | Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp ->
          p, fst (CicTypeChecker.type_of_aux' metasenv tail u CicUniv.empty_ugraph)
       | _ :: tail -> aux (succ p) tail
-      | [] -> raise (ProofEngineTypes.Fail "lookup_type: not premise in the current goal")
+      | [] -> raise (ProofEngineTypes.Fail (lazy "lookup_type: not premise in the current goal"))
    in
    aux 1 context