Huge reorganization of matita and ocaml.

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

diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli
index a7603d3a528bd54d978768892725aa1178ad279b..a7c0e5b543cb6fe23f51dd9be8b1f81c39779cab 100644 (file)
--- 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