changed pattern datatype:

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

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