X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineHelpers.mli;h=a7c0e5b543cb6fe23f51dd9be8b1f81c39779cab;hb=ac595177011c8fd73c39fb9b5aaf8b130fb03ef3;hp=a7603d3a528bd54d978768892725aa1178ad279b;hpb=9e3eb63a93acaca0b4ad59c213e9ea430524d3ae;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli
index a7603d3a5..a7c0e5b54 100644
--- a/helm/ocaml/tactics/proofEngineHelpers.mli
+++ b/helm/ocaml/tactics/proofEngineHelpers.mli
@@ -23,7 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception Bad_pattern of string
+exception Bad_pattern of string Lazy.t
 
 (* Returns the first meta whose number is above the *)
 (* number of the higher meta.                       *)
@@ -76,7 +76,7 @@ val select:
  metasenv:Cic.metasenv ->
  ugraph:CicUniv.universe_graph ->
  conjecture:Cic.conjecture ->
- pattern:ProofEngineTypes.pattern ->
+ pattern:ProofEngineTypes.lazy_pattern ->
   Cic.substitution * Cic.metasenv * CicUniv.universe_graph *
   [ `Decl of (Cic.context * Cic.term) list
   | `Def of (Cic.context * Cic.term) list * (Cic.context * Cic.term) list option