Bug fixed in bottom-up conversion.

[helm.git] / helm / software / components / tactics / proofEngineHelpers.mli

diff --git a/helm/software/components/tactics/proofEngineHelpers.mli b/helm/software/components/tactics/proofEngineHelpers.mli
index 0a053ece7dcd212f1e37aef499ee6e6977529705..1eeb0aca3b3356a9168673d20750a35d8d05720e 100644 (file)
--- a/helm/software/components/tactics/proofEngineHelpers.mli
+++ b/helm/software/components/tactics/proofEngineHelpers.mli
@@ -35,7 +35,7 @@ val subst_meta_in_proof :
   ProofEngineTypes.proof * Cic.metasenv
 val subst_meta_and_metasenv_in_proof :
   ProofEngineTypes.proof ->
-  int -> (Cic.term -> Cic.term) -> Cic.metasenv ->
+  int -> Cic.substitution -> Cic.metasenv ->
   ProofEngineTypes.proof * Cic.metasenv
 
 (* returns the list of goals that are in newmetasenv and were not in