All the reduction tactics have been modified to reduce several (sub)terms

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

diff --git a/helm/ocaml/tactics/proofEngineReduction.mli b/helm/ocaml/tactics/proofEngineReduction.mli
index 91bce1a39d3d10b10031c667aae35e43f9e542aa..2c210b677c3e02c8861a43ca058018cf81d5e426 100644 (file)
--- a/helm/ocaml/tactics/proofEngineReduction.mli
+++ b/helm/ocaml/tactics/proofEngineReduction.mli
@@ -32,11 +32,12 @@ exception WrongUriToInductiveDefinition
 exception RelToHiddenHypothesis
 exception WrongShape
 exception AlreadySimplified
+exception WhatAndWithWhatDoNotHaveTheSameLength;;
 
 val alpha_equivalence: Cic.term -> Cic.term -> bool
 val replace :
   equality:(Cic.term -> 'a -> bool) ->
-  what:'a -> with_what:Cic.term -> where:Cic.term -> Cic.term
+  what:'a list -> with_what:Cic.term list -> where:Cic.term -> Cic.term
 val replace_lifting :
   equality:(Cic.term -> Cic.term -> bool) ->
   what:Cic.term -> with_what:Cic.term -> where:Cic.term -> Cic.term