added applyS

[helm.git] / helm / software / components / tactics / paramodulation / indexing.mli

diff --git a/helm/software/components/tactics/paramodulation/indexing.mli b/helm/software/components/tactics/paramodulation/indexing.mli
index fe8582e92dc21788252f83ec2c678e18db9cf409..a446747e5c53ff3a10c3940103c5173e84dc46a0 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.mli
+++ b/helm/software/components/tactics/paramodulation/indexing.mli
@@ -45,12 +45,12 @@ val unification :
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
   Equality.equality ->
-  (Subst.substitution * Equality.equality) option
+  (Subst.substitution * Equality.equality * bool) option
 val subsumption :
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
   Equality.equality ->
-  (Subst.substitution * Equality.equality) option
+  (Subst.substitution * Equality.equality * bool) option
 val superposition_left :
   Cic.conjecture list * Cic.context * CicUniv.universe_graph ->
   Index.t ->