* ElimSimplIntros replace by ElimIntrosSimpl. Simplification is performed

[helm.git] / helm / gTopLevel / primitiveTactics.mli

diff --git a/helm/gTopLevel/primitiveTactics.mli b/helm/gTopLevel/primitiveTactics.mli
index 59a714c78c938e3144f963a12390b54d332451f0..dad385339b876bbe4da402bf4d9068c62d9b3923 100644 (file)
--- a/helm/gTopLevel/primitiveTactics.mli
+++ b/helm/gTopLevel/primitiveTactics.mli
@@ -34,7 +34,7 @@ val cut_tac:
 val letin_tac:
   term: Cic.term -> ProofEngineTypes.tactic 
 
-val elim_simpl_intros_tac:
+val elim_intros_simpl_tac:
   term: Cic.term -> ProofEngineTypes.tactic 
 
 val change_tac: